Email Gateway (Aug 22 2022 at 09:45): Email Gateway (Aug 22 2022 at 09:45):From: Quentin Hibon <quentin.hibon@polytechnique.edu>
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
Email Gateway (Aug 22 2022 at 09:48):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 10:06):From: Quentin Hibon <quentin.hibon@polytechnique.edu>
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
Email Gateway (Aug 22 2022 at 10:07):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Last updated: Apr 25 2024 at 08:20 UTC