# [isabelle] Measure definition on streams

Dear probability experts,

`I have a possibly infinite nesting of discrete probability distributions, i.e., a
``codatatype of the form
`
codatatype foo = Foo "(nat * foo) pmf"

`where pmf is the type of discrete probability distributions (probability mass functions,
``PMF). Now, I would like to measure unrollings of some "foo :: foo", which are infinite
``streams of naturals. The streams are generated by picking a element (n, foo') from the
``support of foo's PMF, use n as the head of the stream and continue corecursively with
``foo'. The probability of a single stream should intuitively be the product of all the
``probabilities of the random choices according to the PMFs. This is only the intuition, as
``the stream is infinite and the resulting distribution is continuous, so the density given
``by the product does not exist.
`

`I now want to construct the measure space with the associated measure on the sigma algebra
``generated by the usual cylinders on streams. I tried to define the measure on the
``cylinders (which can be indexed all finite lists of naturals) and found the function
``extend_measure for that. Unfortunately, I have not found many usable theorems about
``extend_measure. In the theorem emeasure_extend_measure, e.g., I have to provide a positive
``and countably-additive function mu' on the sigma algebra of the cylinders, which is just
``what I want to construct. Am I overlooking the obvious? Are there better ways to construct
``the measure function I want? The sigma algebra is isomorphic to the infinite indexed
``product. My problem is just assigning the right probability to the sets of streams.
`
Thanks in advance for any pointers and suggestions,
Andreas

`PS: I am hooked in a recent snapshot of the development version, so I am happy to use all
``the new stuff that will be only available in Isabelle2015. I still post on isabelle-users
``as this is a general question about measures in Isabelle which will still be relevant
``after the next release.
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*