[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,

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.