# Re: [isabelle] Probabilities: expectation as a sum

```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]
> 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?
> >>
> >>
> >> 	Quentin
> >
> >
> >
> >
>

```

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