Re: [isabelle] Measure definition on streams

Hi Andreas,

I think you can use the formalization of Markov chains in the locale
MC_syntax in \$AFP/Markov_Models/Discrete_Time_Markov_Chain. Here a
Markov chain K is given as the Markov kernel (i.e. transition system)
K :: 's => 's pmf.

In your case the state space is nat * foo, so MC_syntax can be
instantiated with
K == un_Foo o snd
then you get a trace space "T s :: (nat * foo) stream measure". With
T' s == distr (T s) (stream_space (count_space UNIV)) (smap fst)
you construct a "nat stream space". But be aware: you lost some
information, so T' is not the trace space of a Markov chain anymore!

- Johannes

PS: If you want to construct the trace space yourself you want to use
Caratheodories extension theorem in the form of
extend_measure_caratheodory.
But generally I would suggest to avoid this and use the product measure
or the trace space of Markov chains.

Am Dienstag, den 24.02.2015, 17:19 +0100 schrieb Andreas Lochbihler:
> 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. 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.