*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Measure definition on streams*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 24 Feb 2015 23:21:44 +0100*In-reply-to*: <54ECA47B.5050707@inf.ethz.ch>*Organization*: TU München*References*: <54ECA47B.5050707@inf.ethz.ch>

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! Does this answer your question? - 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 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. >

**Follow-Ups**:**Re: [isabelle] Measure definition on streams***From:*Andreas Lochbihler

**References**:**[isabelle] Measure definition on streams***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
- Next by Date: [isabelle] Typo in Tutorial?
- Previous by Thread: [isabelle] Measure definition on streams
- Next by Thread: Re: [isabelle] Measure definition on streams
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list