*To*: Quentin Hibon <quentin.hibon at polytechnique.edu>*Subject*: Re: [isabelle] Probabilities: expectation as a sum*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 12 May 2015 11:12:00 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <554CD468.6070900@polytechnique.edu>*Organization*: TU München*References*: <5548E30D.7030007@polytechnique.edu> <1430911953.12550.22.camel@lapnipkow5> <554CD468.6070900@polytechnique.edu>

Currently, I have no _concrete_ plans to replace simple_distributed by pmfs. But I think in future development pmfs could replace simple_distributed, as pmfs are much easier to handle. - Johannes Am Freitag, den 08.05.2015, 16:21 +0100 schrieb Quentin Hibon: > Hi Johannes, > > many thanks, that does the trick. I realized I actually needed the > expectation of f(X), but the proof is obvious using yours: > > lemma (in prob_space) simp_exp_composed: > assumes X: "simple_distributed M X Px" > shows "expectation (Îa. f (X a)) = (âx â X`space M. f x * Px x)" > using distributed_integral[OF simple_distributed[OF X], of f] > by (simp add: lebesgue_integral_count_space_finite[OF > simple_distributed_finite[OF X]] ac_simps) > > I don't think I need to reason on sets that are not finite, as I only > use random variables that output symbols taken from a finite set, so > simple_distributed should suffice. I have seen that the pmf type could > have helped me to manipulate such expressions, but I'm not sure that I > would be wise to try to rewrite all that I have done so far using > simple_distributed. > > Do you intend on linking simple_distributed and the pmf type, or are > they to remain independent definitions? > > Quentin > > On 05/06/2015 12:32 PM, Johannes HÃlzl wrote: > > > > Hi Quentin, > > > > thanks for using Probability theory :-) > > > > Your lemma can be proved by using distributed_integral, and with > > relating > > simple_distributed to finite and distributed: > > > > lemma (in prob_space) simp_exp: > > assumes X: "simple_distributed M X Px" > > shows "expectation X = (âx â X`space M. x * Px x)" > > using simple_distributed_finite[OF X] > > using distributed_integral[OF simple_distributed[OF X], of "Îx. x", > > symmetric] > > by (simp add: lebesgue_integral_count_space_finite ac_simps) > > > > Remember that simple_distributed is only finite, not countable. > > > > Another option is to use the new pmf type of discrete (countable) > > distributions, available in Isabelle2015. But which one is better suited > > depends on your exact use-case. > > > > - Johannes > > > > > > > > Am Dienstag, den 05.05.2015, 16:34 +0100 schrieb Quentin Hibon: > >> Dear Isabelle users, > >> > >> I am trying to use the probability theories provided with Isabelle 2014, > >> however I find it harder than I had thought to derive a basic formula > >> from the general ones. > >> > >> I would like to prove that the expectation of a discrete random variable > >> is the sum of the values taken times their respective probabilities: > >> > >> lemma simp_exp: > >> assumes X: "simple_distributed M X Px" > >> shows "expectation X = (âx â X`space M. x * Px x)" > >> > >> (in a sublocale of prob_space) > >> > >> I know that there is lebesgue_integral_count_space_finite (in > >> Bochner_Integration) that links an integral over a countable set to the > >> related sum, but I'm not sure how I can use it in this case. > >> I could also probably use the integral over simple_function[s] as it is > >> defined as a sum, but I would then have to prove it is the same as the > >> Lebesgue function. Is there any other more straightforward option? > >> > >> Thanks in advance, > >> > >> Quentin > > > > > > > > >

**References**:**[isabelle] Probabilities: expectation as a sum***From:*Quentin Hibon

**Re: [isabelle] Probabilities: expectation as a sum***From:*Johannes Hölzl

**Re: [isabelle] Probabilities: expectation as a sum***From:*Quentin Hibon

- Previous by Date: Re: [isabelle] simp warnings for cong rules
- Next by Date: [isabelle] Extracting Goal Information from Proof Terms
- Previous by Thread: Re: [isabelle] Probabilities: expectation as a sum
- Next by Thread: [isabelle] Rule ccontr
- Cl-isabelle-users May 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