(* Title: HOL/Probability/Probability_Mass_Function.thy
Author: Johannes Hölzl, TU München
Author: Andreas Lochbihler, ETH Zurich
*)
section \ Probability mass function \
theory Probability_Mass_Function
imports
Giry_Monad
"~~/src/HOL/Library/Multiset"
begin
lemma AE_emeasure_singleton:
assumes x: "emeasure M {x} \ 0" and ae: "AE x in M. P x" shows "P x"
proof -
from x have x_M: "{x} \ sets M"
by (auto intro: emeasure_notin_sets)
from ae obtain N where N: "{x\space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M"
by (auto elim: AE_E)
{ assume "\ P x"
with x_M[THEN sets.sets_into_space] N have "emeasure M {x} \ emeasure M N"
by (intro emeasure_mono) auto
with x N have False
by (auto simp: emeasure_le_0_iff) }
then show "P x" by auto
qed
lemma AE_measure_singleton: "measure M {x} \ 0 \ AE x in M. P x \ P x"
by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty)
lemma ereal_divide': "b \ 0 \ ereal (a / b) = ereal a / ereal b"
using ereal_divide[of a b] by simp
lemma (in finite_measure) countable_support:
"countable {x. measure M {x} \ 0}"
proof cases
assume "measure M (space M) = 0"
with bounded_measure measure_le_0_iff have "{x. measure M {x} \ 0} = {}"
by auto
then show ?thesis
by simp
next
let ?M = "measure M (space M)" and ?m = "\x. measure M {x}"
assume "?M \ 0"
then have *: "{x. ?m x \ 0} = (\n. {x. ?M / Suc n < ?m x})"
using reals_Archimedean[of "?m x / ?M" for x]
by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
have **: "\n. finite {x. ?M / Suc n < ?m x}"
proof (rule ccontr)
fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
then obtain X where "finite X" "card X = Suc (Suc n)" "X \ ?X"
by (metis infinite_arbitrarily_large)
from this(3) have *: "\x. x \ X \ ?M / Suc n \ ?m x"
by auto
{ fix x assume "x \ X"
from `?M \ 0` *[OF this] have "?m x \ 0" by (auto simp: field_simps measure_le_0_iff)
then have "{x} \ sets M" by (auto dest: measure_notin_sets) }
note singleton_sets = this
have "?M < (\x\X. ?M / Suc n)"
using `?M \ 0`
by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
also have "\ \ (\x\X. ?m x)"
by (rule setsum_mono) fact
also have "\ = measure M (\x\X. {x})"
using singleton_sets `finite X`
by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
finally have "?M < measure M (\x\X. {x})" .
moreover have "measure M (\x\X. {x}) \ ?M"
using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
ultimately show False by simp
qed
show ?thesis
unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
qed
lemma (in finite_measure) AE_support_countable:
assumes [simp]: "sets M = UNIV"
shows "(AE x in M. measure M {x} \ 0) \ (\S. countable S \ (AE x in M. x \ S))"
proof
assume "\S. countable S \ (AE x in M. x \ S)"
then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \ S"
by auto
then have "emeasure M (\x\{x\S. emeasure M {x} \ 0}. {x}) =
(\\<^sup>+ x. emeasure M {x} * indicator {x\S. emeasure M {x} \ 0} x \count_space UNIV)"
by (subst emeasure_UN_countable)
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
also have "\ = (\\<^sup>+ x. emeasure M {x} * indicator S x \count_space UNIV)"
by (auto intro!: nn_integral_cong split: split_indicator)
also have "\ = emeasure M (\x\S. {x})"
by (subst emeasure_UN_countable)
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
also have "\ = emeasure M (space M)"
using ae by (intro emeasure_eq_AE) auto
finally have "emeasure M {x \ space M. x\S \ emeasure M {x} \ 0} = emeasure M (space M)"
by (simp add: emeasure_single_in_space cong: rev_conj_cong)
with finite_measure_compl[of "{x \ space M. x\S \ emeasure M {x} \ 0}"]
have "AE x in M. x \ S \ emeasure M {x} \ 0"
by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong)
then show "AE x in M. measure M {x} \ 0"
by (auto simp: emeasure_eq_measure)
qed (auto intro!: exI[of _ "{x. measure M {x} \ 0}"] countable_support)
subsection \ PMF as measure \
typedef 'a pmf = "{M :: 'a measure. prob_space M \ sets M = UNIV \ (AE x in M. measure M {x} \ 0)}"
morphisms measure_pmf Abs_pmf
by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
(auto intro!: prob_space_uniform_measure AE_uniform_measureI)
declare [[coercion measure_pmf]]
lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
using pmf.measure_pmf[of p] by auto
interpretation measure_pmf!: prob_space "measure_pmf M" for M
by (rule prob_space_measure_pmf)
interpretation measure_pmf!: subprob_space "measure_pmf M" for M
by (rule prob_space_imp_subprob_space) unfold_locales
lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
by unfold_locales
locale pmf_as_measure
begin
setup_lifting type_definition_pmf
end
context
begin
interpretation pmf_as_measure .
lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
by transfer blast
lemma sets_measure_pmf_count_space[measurable_cong]:
"sets (measure_pmf M) = sets (count_space UNIV)"
by simp
lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \ space (subprob_algebra (count_space UNIV))"
by (simp add: space_subprob_algebra subprob_space_measure_pmf)
lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \ space N"
by (auto simp: measurable_def)
lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)"
by (intro measurable_cong_sets) simp_all
lemma measurable_pair_restrict_pmf2:
assumes "countable A"
assumes [measurable]: "\y. y \ A \ (\x. f (x, y)) \ measurable M L"
shows "f \ measurable (M \\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \ measurable ?M _")
proof -
have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
by (simp add: restrict_count_space)
show ?thesis
by (intro measurable_compose_countable'[where f="\a b. f (fst b, a)" and g=snd and I=A,
unfolded pair_collapse] assms)
measurable
qed
lemma measurable_pair_restrict_pmf1:
assumes "countable A"
assumes [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N L"
shows "f \ measurable (restrict_space (measure_pmf M) A \\<^sub>M N) L"
proof -
have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
by (simp add: restrict_count_space)
show ?thesis
by (intro measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A,
unfolded pair_collapse] assms)
measurable
qed
lift_definition pmf :: "'a pmf \ 'a \ real" is "\M x. measure M {x}" .
lift_definition set_pmf :: "'a pmf \ 'a set" is "\M. {x. measure M {x} \ 0}" .
declare [[coercion set_pmf]]
lemma AE_measure_pmf: "AE x in (M::'a pmf). x \ M"
by transfer simp
lemma emeasure_pmf_single_eq_zero_iff:
fixes M :: "'a pmf"
shows "emeasure M {y} = 0 \ y \ M"
by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \ (\y\M. P y)"
using AE_measure_singleton[of M] AE_measure_pmf[of M]
by (auto simp: set_pmf.rep_eq)
lemma countable_set_pmf [simp]: "countable (set_pmf p)"
by transfer (metis prob_space.finite_measure finite_measure.countable_support)
lemma pmf_positive: "x \ set_pmf p \ 0 < pmf p x"
by transfer (simp add: less_le measure_nonneg)
lemma pmf_nonneg: "0 \ pmf p x"
by transfer (simp add: measure_nonneg)
lemma pmf_le_1: "pmf p x \ 1"
by (simp add: pmf.rep_eq)
lemma set_pmf_not_empty: "set_pmf M \ {}"
using AE_measure_pmf[of M] by (intro notI) simp
lemma set_pmf_iff: "x \ set_pmf M \ pmf M x \ 0"
by transfer simp
lemma set_pmf_eq: "set_pmf M = {x. pmf M x \ 0}"
by (auto simp: set_pmf_iff)
lemma emeasure_pmf_single:
fixes M :: "'a pmf"
shows "emeasure M {x} = pmf M x"
by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
lemma emeasure_measure_pmf_finite: "finite S \ emeasure (measure_pmf M) S = (\s\S. pmf M s)"
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
lemma measure_measure_pmf_finite: "finite S \ measure (measure_pmf M) S = setsum (pmf M) S"
using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
lemma nn_integral_measure_pmf_support:
fixes f :: "'a \ ereal"
assumes f: "finite A" and nn: "\x. x \ A \ 0 \ f x" "\x. x \ set_pmf M \ x \ A \ f x = 0"
shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\A. f x * pmf M x)"
proof -
have "(\\<^sup>+x. f x \M) = (\\<^sup>+x. f x * indicator A x \M)"
using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator)
also have "\ = (\x\A. f x * emeasure M {x})"
using assms by (intro nn_integral_indicator_finite) auto
finally show ?thesis
by (simp add: emeasure_measure_pmf_finite)
qed
lemma nn_integral_measure_pmf_finite:
fixes f :: "'a \ ereal"
assumes f: "finite (set_pmf M)" and nn: "\x. x \ set_pmf M \ 0 \ f x"
shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\set_pmf M. f x * pmf M x)"
using assms by (intro nn_integral_measure_pmf_support) auto
lemma integrable_measure_pmf_finite:
fixes f :: "'a \ 'b::{banach, second_countable_topology}"
shows "finite (set_pmf M) \ integrable M f"
by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite)
lemma integral_measure_pmf:
assumes [simp]: "finite A" and "\a. a \ set_pmf M \ f a \ 0 \ a \ A"
shows "(\x. f x \measure_pmf M) = (\a\A. f a * pmf M a)"
proof -
have "(\x. f x \measure_pmf M) = (\x. f x * indicator A x \measure_pmf M)"
using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff)
also have "\ = (\a\A. f a * pmf M a)"
by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite)
finally show ?thesis .
qed
lemma integrable_pmf: "integrable (count_space X) (pmf M)"
proof -
have " (\\<^sup>+ x. pmf M x \count_space X) = (\\<^sup>+ x. pmf M x \count_space (M \ X))"
by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator)
then have "integrable (count_space X) (pmf M) = integrable (count_space (M \ X)) (pmf M)"
by (simp add: integrable_iff_bounded pmf_nonneg)
then show ?thesis
by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def)
qed
lemma integral_pmf: "(\x. pmf M x \count_space X) = measure M X"
proof -
have "(\x. pmf M x \count_space X) = (\\<^sup>+x. pmf M x \count_space X)"
by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral)
also have "\ = (\\<^sup>+x. emeasure M {x} \count_space (X \ M))"
by (auto intro!: nn_integral_cong_AE split: split_indicator
simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator
AE_count_space set_pmf_iff)
also have "\ = emeasure M (X \ M)"
by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf)
also have "\ = emeasure M X"
by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff)
finally show ?thesis
by (simp add: measure_pmf.emeasure_eq_measure)
qed
lemma integral_pmf_restrict:
"(f::'a \ 'b::{banach, second_countable_topology}) \ borel_measurable (count_space UNIV) \
(\x. f x \measure_pmf M) = (\x. f x \restrict_space M M)"
by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff)
lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1"
proof -
have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)"
by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf)
then show ?thesis
using measure_pmf.emeasure_space_1 by simp
qed
lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
using measure_pmf.emeasure_space_1[of M] by simp
lemma in_null_sets_measure_pmfI:
"A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)"
using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"]
by(auto simp add: null_sets_def AE_measure_pmf_iff)
lemma measure_subprob: "measure_pmf M \ space (subprob_algebra (count_space UNIV))"
by (simp add: space_subprob_algebra subprob_space_measure_pmf)
subsection \ Monad Interpretation \
lemma measurable_measure_pmf[measurable]:
"(\x. measure_pmf (M x)) \ measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales
lemma bind_measure_pmf_cong:
assumes "\x. A x \ space (subprob_algebra N)" "\x. B x \ space (subprob_algebra N)"
assumes "\i. i \ set_pmf x \ A i = B i"
shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
proof (rule measure_eqI)
show "sets (measure_pmf x \= A) = sets (measure_pmf x \= B)"
using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
next
fix X assume "X \ sets (measure_pmf x \= A)"
then have X: "X \ sets N"
using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
show "emeasure (measure_pmf x \= A) X = emeasure (measure_pmf x \= B) X"
using assms
by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
(auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
qed
lift_definition bind_pmf :: "'a pmf \ ('a \ 'b pmf ) \ 'b pmf" is bind
proof (clarify, intro conjI)
fix f :: "'a measure" and g :: "'a \ 'b measure"
assume "prob_space f"
then interpret f: prob_space f .
assume "sets f = UNIV" and ae_f: "AE x in f. measure f {x} \ 0"
then have s_f[simp]: "sets f = sets (count_space UNIV)"
by simp
assume g: "\x. prob_space (g x) \ sets (g x) = UNIV \ (AE y in g x. measure (g x) {y} \ 0)"
then have g: "\x. prob_space (g x)" and s_g[simp]: "\x. sets (g x) = sets (count_space UNIV)"
and ae_g: "\x. AE y in g x. measure (g x) {y} \ 0"
by auto
have [measurable]: "g \ measurable f (subprob_algebra (count_space UNIV))"
by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
show "prob_space (f \= g)"
using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
then interpret fg: prob_space "f \= g" .
show [simp]: "sets (f \= g) = UNIV"
using sets_eq_imp_space_eq[OF s_f]
by (subst sets_bind[where N="count_space UNIV"]) auto
show "AE x in f \= g. measure (f \= g) {x} \ 0"
apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"])
using ae_f
apply eventually_elim
using ae_g
apply eventually_elim
apply (auto dest: AE_measure_singleton)
done
qed
lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)"
unfolding pmf.rep_eq bind_pmf.rep_eq
by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg
intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
lemma pmf_bind: "pmf (bind_pmf N f) i = (\x. pmf (f x) i \measure_pmf N)"
using ereal_pmf_bind[of N f i]
by (subst (asm) nn_integral_eq_integral)
(auto simp: pmf_nonneg pmf_le_1
intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
lemma bind_pmf_const[simp]: "bind_pmf M (\