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!

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.
> 






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