[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