Re: [isabelle] Probabilities: expectation as a sum
Currently, I have no _concrete_ plans to replace simple_distributed by
But I think in future development pmfs could replace simple_distributed,
as pmfs are much easier to handle.
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
> Do you intend on linking simple_distributed and the pmf type, or are
> they to remain independent definitions?
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and