Theory HOL-Probability.Probability_Measure
section ‹Probability measure›
theory Probability_Measure
imports "HOL-Analysis.Analysis"
begin
locale prob_space = finite_measure +
assumes emeasure_space_1: "emeasure M (space M) = 1"
lemma prob_spaceI[Pure.intro!]:
assumes *: "emeasure M (space M) = 1"
shows "prob_space M"
by (simp add: assms finite_measureI prob_space_axioms.intro prob_space_def)
lemma prob_space_imp_sigma_finite: "prob_space M ⟹ sigma_finite_measure M"
unfolding prob_space_def finite_measure_def by simp
abbreviation (in prob_space) "events ≡ sets M"
abbreviation (in prob_space) "prob ≡ measure M"
abbreviation (in prob_space) "random_variable M' X ≡ X ∈ measurable M M'"
abbreviation (in prob_space) "expectation ≡ integral⇧L M"
abbreviation (in prob_space) "variance X ≡ integral⇧L M (λx. (X x - expectation X)⇧2)"
lemma (in prob_space) finite_measure [simp]: "finite_measure M"
by unfold_locales
lemma (in prob_space) prob_space_distr:
assumes f: "f ∈ measurable M M'" shows "prob_space (distr M M' f)"
proof (rule prob_spaceI)
have "f -` space M' ∩ space M = space M" using f by (auto dest: measurable_space)
with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
by (auto simp: emeasure_distr emeasure_space_1)
qed
lemma prob_space_distrD:
assumes f: "f ∈ measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
proof
interpret M: prob_space "distr M N f" by fact
have "f -` space N ∩ space M = space M"
using f[THEN measurable_space] by auto
then show "emeasure M (space M) = 1"
using M.emeasure_space_1 by (simp add: emeasure_distr[OF f])
qed
lemma (in prob_space) prob_space: "prob (space M) = 1"
by (simp add: emeasure_space_1 measure_eq_emeasure_eq_ennreal)
lemma (in prob_space) prob_le_1[simp, intro]: "prob A ≤ 1"
using bounded_measure[of A] by (simp add: prob_space)
lemma (in prob_space) not_empty: "space M ≠ {}"
using prob_space by auto
lemma (in prob_space) emeasure_eq_1_AE:
"S ∈ sets M ⟹ AE x in M. x ∈ S ⟹ emeasure M S = 1"
by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1)
lemma (in prob_space) emeasure_le_1: "emeasure M S ≤ 1"
unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto
lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A ≥ 1 ⟷ emeasure M A = 1"
by (rule iffI, intro antisym emeasure_le_1) simp_all
lemma (in prob_space) AE_iff_emeasure_eq_1:
assumes [measurable]: "Measurable.pred M P"
shows "(AE x in M. P x) ⟷ emeasure M {x∈space M. P x} = 1"
proof -
have *: "{x ∈ space M. ¬ P x} = space M - {x∈space M. P x}"
by auto
show ?thesis
by (auto simp add: ennreal_minus_eq_0 * emeasure_compl emeasure_space_1 AE_iff_measurable[OF _ refl]
intro: antisym emeasure_le_1)
qed
lemma (in prob_space) measure_le_1: "emeasure M X ≤ 1"
using emeasure_space[of M X] by (simp add: emeasure_space_1)
lemma (in prob_space) measure_ge_1_iff: "measure M A ≥ 1 ⟷ measure M A = 1"
by (auto intro!: antisym)
lemma (in prob_space) AE_I_eq_1:
assumes "emeasure M {x∈space M. P x} = 1" "{x∈space M. P x} ∈ sets M"
shows "AE x in M. P x"
proof (rule AE_I)
show "emeasure M (space M - {x ∈ space M. P x}) = 0"
using assms emeasure_space_1 by (simp add: emeasure_compl)
qed (insert assms, auto)
lemma prob_space_restrict_space:
"S ∈ sets M ⟹ emeasure M S = 1 ⟹ prob_space (restrict_space M S)"
by (intro prob_spaceI)
(simp add: emeasure_restrict_space space_restrict_space)
lemma (in prob_space) prob_compl:
assumes A: "A ∈ events"
shows "prob (space M - A) = 1 - prob A"
using finite_measure_compl[OF A] by (simp add: prob_space)
lemma (in prob_space) AE_in_set_eq_1:
assumes A[measurable]: "A ∈ events" shows "(AE x in M. x ∈ A) ⟷ prob A = 1"
proof -
have *: "{x∈space M. x ∈ A} = A"
using A[THEN sets.sets_into_space] by auto
show ?thesis
by (subst AE_iff_emeasure_eq_1) (auto simp: emeasure_eq_measure *)
qed
lemma (in prob_space) AE_False: "(AE x in M. False) ⟷ False"
proof
assume "AE x in M. False"
then have "AE x in M. x ∈ {}" by simp
then show False
by (subst (asm) AE_in_set_eq_1) auto
qed simp
lemma (in prob_space) AE_prob_1:
assumes "prob A = 1" shows "AE x in M. x ∈ A"
proof -
from ‹prob A = 1› have "A ∈ events"
by (metis measure_notin_sets zero_neq_one)
with AE_in_set_eq_1 assms show ?thesis by simp
qed
lemma (in prob_space) AE_const[simp]: "(AE x in M. P) ⟷ P"
by (cases P) (auto simp: AE_False)
lemma (in prob_space) ae_filter_bot: "ae_filter M ≠ bot"
by (simp add: trivial_limit_def)
lemma (in prob_space) AE_contr:
assumes ae: "AE ω in M. P ω" "AE ω in M. ¬ P ω"
shows False
proof -
from ae have "AE ω in M. False" by eventually_elim auto
then show False by auto
qed
lemma (in prob_space) integral_ge_const:
fixes c :: real
shows "integrable M f ⟹ (AE x in M. c ≤ f x) ⟹ c ≤ (∫x. f x ∂M)"
using integral_mono_AE[of M "λx. c" f] prob_space by simp
lemma (in prob_space) integral_le_const:
fixes c :: real
shows "integrable M f ⟹ (AE x in M. f x ≤ c) ⟹ (∫x. f x ∂M) ≤ c"
using integral_mono_AE[of M f "λx. c"] prob_space by simp
lemma (in prob_space) nn_integral_ge_const:
"(AE x in M. c ≤ f x) ⟹ c ≤ (∫⇧+x. f x ∂M)"
using nn_integral_mono_AE[of "λx. c" f M] emeasure_space_1
by (simp split: if_split_asm)
lemma (in prob_space) expectation_less:
fixes X :: "_ ⇒ real"
assumes [simp]: "integrable M X"
assumes gt: "AE x in M. X x < b"
shows "expectation X < b"
proof -
have "expectation X < expectation (λx. b)"
using gt emeasure_space_1
by (intro integral_less_AE_space) auto
then show ?thesis using prob_space by simp
qed
lemma (in prob_space) expectation_greater:
fixes X :: "_ ⇒ real"
assumes [simp]: "integrable M X"
assumes gt: "AE x in M. a < X x"
shows "a < expectation X"
proof -
have "expectation (λx. a) < expectation X"
using gt emeasure_space_1
by (intro integral_less_AE_space) auto
then show ?thesis using prob_space by simp
qed
lemma (in prob_space) jensens_inequality:
fixes q :: "real ⇒ real"
assumes X: "integrable M X" "AE x in M. X x ∈ I"
assumes I: "I = {a <..< b} ∨ I = {a <..} ∨ I = {..< b} ∨ I = UNIV"
assumes q: "integrable M (λx. q (X x))" "convex_on I q"
shows "q (expectation X) ≤ expectation (λx. q (X x))"
proof -
let ?F = "λx. Inf ((λt. (q x - q t) / (x - t)) ` ({x<..} ∩ I))"
from X(2) AE_False have "I ≠ {}" by auto
from I have "open I" by auto
note I
moreover
{ assume "I ⊆ {a <..}"
with X have "a < expectation X"
by (intro expectation_greater) auto }
moreover
{ assume "I ⊆ {..< b}"
with X have "expectation X < b"
by (intro expectation_less) auto }
ultimately have "expectation X ∈ I"
by (elim disjE) (auto simp: subset_eq)
moreover
{ fix y assume y: "y ∈ I"
with q(2) ‹open I› have "Sup ((λx. q x + ?F x * (y - x)) ` I) = q y"
by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
ultimately have "q (expectation X) = Sup ((λx. q x + ?F x * (expectation X - x)) ` I)"
by simp
also have "… ≤ expectation (λw. q (X w))"
proof (rule cSup_least)
show "(λx. q x + ?F x * (expectation X - x)) ` I ≠ {}"
using ‹I ≠ {}› by auto
next
fix k assume "k ∈ (λx. q x + ?F x * (expectation X - x)) ` I"
then obtain x
where x: "k = q x + (INF t∈{x<..} ∩ I. (q x - q t) / (x - t)) * (expectation X - x)" "x ∈ I" ..
have "q x + ?F x * (expectation X - x) = expectation (λw. q x + ?F x * (X w - x))"
using prob_space by (simp add: X)
also have "… ≤ expectation (λw. q (X w))"
using ‹x ∈ I› ‹open I› X(2)
apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff
integrable_const X q)
apply (elim eventually_mono)
apply (intro convex_le_Inf_differential)
apply (auto simp: interior_open q)
done
finally show "k ≤ expectation (λw. q (X w))" using x by auto
qed
finally show "q (expectation X) ≤ expectation (λx. q (X x))" .
qed
lemma (in prob_space) finite_borel_measurable_integrable:
assumes "f∈ borel_measurable M"
and "finite (f`(space M))"
shows "integrable M f"
proof -
have "simple_function M f" using assms by (simp add: simple_function_borel_measurable)
moreover have "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞" by simp
ultimately have "Bochner_Integration.simple_bochner_integrable M f"
using Bochner_Integration.simple_bochner_integrable.simps by blast
hence "has_bochner_integral M f (Bochner_Integration.simple_bochner_integral M f)"
using has_bochner_integral_simple_bochner_integrable by auto
thus ?thesis using integrable.simps by auto
qed
subsection ‹Introduce binder for probability›
syntax
"_prob" :: "pttrn ⇒ logic ⇒ logic ⇒ logic" (‹('𝒫'((/_ in _./ _)'))›)
translations
"𝒫(x in M. P)" => "CONST measure M {x ∈ CONST space M. P}"
print_translation ‹
let
fun to_pattern (Const (\<^const_syntax>‹Pair›, _) $ l $ r) =
Syntax.const \<^const_syntax>‹Pair› :: to_pattern l @ to_pattern r
| to_pattern (t as (Const (\<^syntax_const>‹_bound›, _)) $ _) = [t]
fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t
and mk_patterns 0 xs = ([], xs)
| mk_patterns n xs =
let
val (t, xs') = mk_pattern xs
val (ts, xs'') = mk_patterns (n - 1) xs'
in
(t :: ts, xs'')
end
fun unnest_tuples
(Const (\<^syntax_const>‹_pattern›, _) $
t1 $
(t as (Const (\<^syntax_const>‹_pattern›, _) $ _ $ _)))
= let
val (_ $ t2 $ t3) = unnest_tuples t
in
Syntax.const \<^syntax_const>‹_pattern› $
unnest_tuples t1 $
(Syntax.const \<^syntax_const>‹_patterns› $ t2 $ t3)
end
| unnest_tuples pat = pat
fun tr' [sig_alg, Const (\<^const_syntax>‹Collect›, _) $ t] =
let
val bound_dummyT = Const (\<^syntax_const>‹_bound›, dummyT)
fun go pattern elem
(Const (\<^const_syntax>‹conj›, _) $
(Const (\<^const_syntax>‹Set.member›, _) $ elem' $ (Const (\<^const_syntax>‹space›, _) $ sig_alg')) $
u)
= let
val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match;
val (pat, rest) = mk_pattern (rev pattern);
val _ = case rest of [] => () | _ => raise Match
in
Syntax.const \<^syntax_const>‹_prob› $ unnest_tuples pat $ sig_alg $ u
end
| go pattern elem (Abs abs) =
let
val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs
in
go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
end
| go pattern elem (Const (\<^const_syntax>‹case_prod›, _) $ t) =
go
((Syntax.const \<^syntax_const>‹_pattern›, 2) :: pattern)
(Syntax.const \<^const_syntax>‹Pair› :: elem)
t
in
go [] [] t
end
in
[(\<^const_syntax>‹Sigma_Algebra.measure›, K tr')]
end
›
definition
"cond_prob M P Q = 𝒫(ω in M. P ω ∧ Q ω) / 𝒫(ω in M. Q ω)"
syntax
"_conditional_prob" :: "pttrn ⇒ logic ⇒ logic ⇒ logic ⇒ logic" (‹('𝒫'(_ in _. _ ¦/ _'))›)
translations
"𝒫(x in M. P ¦ Q)" => "CONST cond_prob M (λx. P) (λx. Q)"
lemma (in prob_space) AE_E_prob:
assumes ae: "AE x in M. P x"
obtains S where "S ⊆ {x ∈ space M. P x}" "S ∈ events" "prob S = 1"
proof -
from ae[THEN AE_E] obtain N
where "{x ∈ space M. ¬ P x} ⊆ N" "emeasure M N = 0" "N ∈ events" by auto
then show thesis
by (intro that[of "space M - N"])
(auto simp: prob_compl prob_space emeasure_eq_measure measure_nonneg)
qed
lemma (in prob_space) prob_neg: "{x∈space M. P x} ∈ events ⟹ 𝒫(x in M. ¬ P x) = 1 - 𝒫(x in M. P x)"
by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])
lemma (in prob_space) prob_eq_AE:
"(AE x in M. P x ⟷ Q x) ⟹ {x∈space M. P x} ∈ events ⟹ {x∈space M. Q x} ∈ events ⟹ 𝒫(x in M. P x) = 𝒫(x in M. Q x)"
by (rule finite_measure_eq_AE) auto
lemma (in prob_space) prob_eq_0_AE:
assumes not: "AE x in M. ¬ P x" shows "𝒫(x in M. P x) = 0"
proof cases
assume "{x∈space M. P x} ∈ events"
with not have "𝒫(x in M. P x) = 𝒫(x in M. False)"
by (intro prob_eq_AE) auto
then show ?thesis by simp
qed (simp add: measure_notin_sets)
lemma (in prob_space) prob_Collect_eq_0:
"{x ∈ space M. P x} ∈ sets M ⟹ 𝒫(x in M. P x) = 0 ⟷ (AE x in M. ¬ P x)"
using AE_iff_measurable[OF _ refl, of M "λx. ¬ P x"] by (simp add: emeasure_eq_measure measure_nonneg)
lemma (in prob_space) prob_Collect_eq_1:
"{x ∈ space M. P x} ∈ sets M ⟹ 𝒫(x in M. P x) = 1 ⟷ (AE x in M. P x)"
using AE_in_set_eq_1[of "{x∈space M. P x}"] by simp
lemma (in prob_space) prob_eq_0:
"A ∈ sets M ⟹ prob A = 0 ⟷ (AE x in M. x ∉ A)"
using AE_iff_measurable[OF _ refl, of M "λx. x ∉ A"]
by (auto simp add: emeasure_eq_measure Int_def[symmetric] measure_nonneg)
lemma (in prob_space) prob_eq_1:
"A ∈ sets M ⟹ prob A = 1 ⟷ (AE x in M. x ∈ A)"
using AE_in_set_eq_1[of A] by simp
lemma (in prob_space) prob_sums:
assumes P: "⋀n. {x∈space M. P n x} ∈ events"
assumes Q: "{x∈space M. Q x} ∈ events"
assumes ae: "AE x in M. (∀n. P n x ⟶ Q x) ∧ (Q x ⟶ (∃!n. P n x))"
shows "(λn. 𝒫(x in M. P n x)) sums 𝒫(x in M. Q x)"
proof -
from ae[THEN AE_E_prob] obtain S
where S:
"S ⊆ {x ∈ space M. (∀n. P n x ⟶ Q x) ∧ (Q x ⟶ (∃!n. P n x))}"
"S ∈ events"
"prob S = 1"
by auto
then have disj: "disjoint_family (λn. {x∈space M. P n x} ∩ S)"
by (auto simp: disjoint_family_on_def)
from S have ae_S:
"AE x in M. x ∈ {x∈space M. Q x} ⟷ x ∈ (⋃n. {x∈space M. P n x} ∩ S)"
"⋀n. AE x in M. x ∈ {x∈space M. P n x} ⟷ x ∈ {x∈space M. P n x} ∩ S"
using ae by (auto dest!: AE_prob_1)
from ae_S have *:
"𝒫(x in M. Q x) = prob (⋃n. {x∈space M. P n x} ∩ S)"
using P Q S by (intro finite_measure_eq_AE) auto
from ae_S have **:
"⋀n. 𝒫(x in M. P n x) = prob ({x∈space M. P n x} ∩ S)"
using P Q S by (intro finite_measure_eq_AE) auto
show ?thesis
unfolding * ** using S P disj
by (intro finite_measure_UNION) auto
qed
lemma (in prob_space) prob_sum:
assumes [simp, intro]: "finite I"
assumes P: "⋀n. n ∈ I ⟹ {x∈space M. P n x} ∈ events"
assumes Q: "{x∈space M. Q x} ∈ events"
assumes ae: "AE x in M. (∀n∈I. P n x ⟶ Q x) ∧ (Q x ⟶ (∃!n∈I. P n x))"
shows "𝒫(x in M. Q x) = (∑n∈I. 𝒫(x in M. P n x))"
proof -
from ae[THEN AE_E_prob] obtain S
where S:
"S ⊆ {x ∈ space M. (∀n∈I. P n x ⟶ Q x) ∧ (Q x ⟶ (∃!n. n ∈ I ∧ P n x))}"
"S ∈ events"
"prob S = 1"
by auto
then have disj: "disjoint_family_on (λn. {x∈space M. P n x} ∩ S) I"
by (auto simp: disjoint_family_on_def)
from S have ae_S:
"AE x in M. x ∈ {x∈space M. Q x} ⟷ x ∈ (⋃n∈I. {x∈space M. P n x} ∩ S)"
"⋀n. n ∈ I ⟹ AE x in M. x ∈ {x∈space M. P n x} ⟷ x ∈ {x∈space M. P n x} ∩ S"
using ae by (auto dest!: AE_prob_1)
from ae_S have *:
"𝒫(x in M. Q x) = prob (⋃n∈I. {x∈space M. P n x} ∩ S)"
using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int)
from ae_S have **:
"⋀n. n ∈ I ⟹ 𝒫(x in M. P n x) = prob ({x∈space M. P n x} ∩ S)"
using P Q S by (intro finite_measure_eq_AE) auto
show ?thesis
using S P disj
by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union)
qed
lemma (in prob_space) prob_EX_countable:
assumes sets: "⋀i. i ∈ I ⟹ {x∈space M. P i x} ∈ sets M" and I: "countable I"
assumes disj: "AE x in M. ∀i∈I. ∀j∈I. P i x ⟶ P j x ⟶ i = j"
shows "𝒫(x in M. ∃i∈I. P i x) = (∫⇧+i. 𝒫(x in M. P i x) ∂count_space I)"
proof -
let ?N= "λx. ∃!i∈I. P i x"
have "ennreal (𝒫(x in M. ∃i∈I. P i x)) = 𝒫(x in M. (∃i∈I. P i x ∧ ?N x))"
unfolding ennreal_inj[OF measure_nonneg measure_nonneg]
proof (rule prob_eq_AE)
show "AE x in M. (∃i∈I. P i x) = (∃i∈I. P i x ∧ ?N x)"
using disj by eventually_elim blast
qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
also have "𝒫(x in M. (∃i∈I. P i x ∧ ?N x)) = emeasure M (⋃i∈I. {x∈space M. P i x ∧ ?N x})"
unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob] simp: measure_nonneg)
also have "… = (∫⇧+i. emeasure M {x∈space M. P i x ∧ ?N x} ∂count_space I)"
by (rule emeasure_UN_countable)
(auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets
simp: disjoint_family_on_def)
also have "… = (∫⇧+i. 𝒫(x in M. P i x) ∂count_space I)"
unfolding emeasure_eq_measure using disj
by (intro nn_integral_cong ennreal_inj[THEN iffD2] prob_eq_AE)
(auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets measure_nonneg)+
finally show ?thesis .
qed
lemma (in prob_space) cond_prob_eq_AE:
assumes P: "AE x in M. Q x ⟶ P x ⟷ P' x" "{x∈space M. P x} ∈ events" "{x∈space M. P' x} ∈ events"
assumes Q: "AE x in M. Q x ⟷ Q' x" "{x∈space M. Q x} ∈ events" "{x∈space M. Q' x} ∈ events"
shows "cond_prob M P Q = cond_prob M P' Q'"
using P Q
by (auto simp: cond_prob_def intro!: arg_cong2[where f="(/)"] prob_eq_AE sets.sets_Collect_conj)
lemma (in prob_space) joint_distribution_Times_le_fst:
"random_variable MX X ⟹ random_variable MY Y ⟹ A ∈ sets MX ⟹ B ∈ sets MY
⟹ emeasure (distr M (MX ⨂⇩M MY) (λx. (X x, Y x))) (A × B) ≤ emeasure (distr M MX X) A"
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
lemma (in prob_space) joint_distribution_Times_le_snd:
"random_variable MX X ⟹ random_variable MY Y ⟹ A ∈ sets MX ⟹ B ∈ sets MY
⟹ emeasure (distr M (MX ⨂⇩M MY) (λx. (X x, Y x))) (A × B) ≤ emeasure (distr M MY Y) B"
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
lemma (in prob_space) variance_eq:
fixes X :: "'a ⇒ real"
assumes [simp]: "integrable M X"
assumes [simp]: "integrable M (λx. (X x)⇧2)"
shows "variance X = expectation (λx. (X x)⇧2) - (expectation X)⇧2"
by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])
lemma (in prob_space) variance_positive: "0 ≤ variance (X::'a ⇒ real)"
by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
lemma (in prob_space) variance_mean_zero:
"expectation X = 0 ⟹ variance X = expectation (λx. (X x)^2)"
by simp
theorem%important (in prob_space) Chebyshev_inequality:
assumes [measurable]: "random_variable borel f"
assumes "integrable M (λx. f x ^ 2)"
defines "μ ≡ expectation f"
assumes "a > 0"
shows "prob {x∈space M. ¦f x - μ¦ ≥ a} ≤ variance f / a⇧2"
unfolding μ_def
proof (rule second_moment_method)
have integrable: "integrable M f"
using assms by (blast dest: square_integrable_imp_integrable)
show "integrable M (λx. (f x - expectation f)⇧2)"
using assms integrable unfolding power2_eq_square ring_distribs
by (intro Bochner_Integration.integrable_diff) auto
qed (use assms in auto)
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
sublocale pair_prob_space ⊆ P?: prob_space "M1 ⨂⇩M M2"
proof
show "emeasure (M1 ⨂⇩M M2) (space (M1 ⨂⇩M M2)) = 1"
by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
qed
locale product_prob_space = product_sigma_finite M for M :: "'i ⇒ 'a measure" +
fixes I :: "'i set"
assumes prob_space: "⋀i. prob_space (M i)"
sublocale product_prob_space ⊆ M?: prob_space "M i" for i
by (rule prob_space)
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
sublocale finite_product_prob_space ⊆ prob_space "Π⇩M i∈I. M i"
proof
show "emeasure (Π⇩M i∈I. M i) (space (Π⇩M i∈I. M i)) = 1"
by (simp add: measure_times M.emeasure_space_1 prod.neutral_const space_PiM)
qed
lemma (in finite_product_prob_space) prob_times:
assumes X: "⋀i. i ∈ I ⟹ X i ∈ sets (M i)"
shows "prob (Π⇩E i∈I. X i) = (∏i∈I. M.prob i (X i))"
proof -
have "ennreal (measure (Π⇩M i∈I. M i) (Π⇩E i∈I. X i)) = emeasure (Π⇩M i∈I. M i) (Π⇩E i∈I. X i)"
using X by (simp add: emeasure_eq_measure)
also have "… = (∏i∈I. emeasure (M i) (X i))"
using measure_times X by simp
also have "… = ennreal (∏i∈I. measure (M i) (X i))"
using X by (simp add: M.emeasure_eq_measure prod_ennreal measure_nonneg)
finally show ?thesis by (simp add: measure_nonneg prod_nonneg)
qed
lemma product_prob_spaceI:
assumes "⋀i. prob_space (M i)"
shows "product_prob_space M"
unfolding product_prob_space_def product_prob_space_axioms_def product_sigma_finite_def
proof safe
fix i
interpret prob_space "M i"
by (rule assms)
show "sigma_finite_measure (M i)" "prob_space (M i)"
by unfold_locales
qed
subsection ‹Distributions›
definition distributed :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ ennreal) ⇒ bool"
where
"distributed M N X f ⟷
distr M N X = density N f ∧ f ∈ borel_measurable N ∧ X ∈ measurable M N"
lemma
assumes "distributed M N X f"
shows distributed_distr_eq_density: "distr M N X = density N f"
and distributed_measurable: "X ∈ measurable M N"
and distributed_borel_measurable: "f ∈ borel_measurable N"
using assms by (simp_all add: distributed_def)
lemma
assumes D: "distributed M N X f"
shows distributed_measurable'[measurable_dest]:
"g ∈ measurable L M ⟹ (λx. X (g x)) ∈ measurable L N"
and distributed_borel_measurable'[measurable_dest]:
"h ∈ measurable L N ⟹ (λx. f (h x)) ∈ borel_measurable L"
using distributed_measurable[OF D] distributed_borel_measurable[OF D]
by simp_all
lemma distributed_real_measurable:
"(⋀x. x ∈ space N ⟹ 0 ≤ f x) ⟹ distributed M N X (λx. ennreal (f x)) ⟹ f ∈ borel_measurable N"
by (simp_all add: distributed_def)
lemma distributed_real_measurable':
"(⋀x. x ∈ space N ⟹ 0 ≤ f x) ⟹ distributed M N X (λx. ennreal (f x)) ⟹
h ∈ measurable L N ⟹ (λx. f (h x)) ∈ borel_measurable L"
using distributed_real_measurable[measurable] by simp
lemma joint_distributed_measurable1:
"distributed M (S ⨂⇩M T) (λx. (X x, Y x)) f ⟹ h1 ∈ measurable N M ⟹ (λx. X (h1 x)) ∈ measurable N S"
by simp
lemma joint_distributed_measurable2:
"distributed M (S ⨂⇩M T) (λx. (X x, Y x)) f ⟹ h2 ∈ measurable N M ⟹ (λx. Y (h2 x)) ∈ measurable N T"
by simp
lemma distributed_count_space:
assumes X: "distributed M (count_space A) X P" and a: "a ∈ A" and A: "finite A"
shows "P a = emeasure M (X -` {a} ∩ space M)"
proof -
have "emeasure M (X -` {a} ∩ space M) = emeasure (distr M (count_space A) X) {a}"
using X a A by (simp add: emeasure_distr)
also have "… = emeasure (density (count_space A) P) {a}"
using X by (simp add: distributed_distr_eq_density)
also have "… = (∫⇧+x. P a * indicator {a} x ∂count_space A)"
using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
also have "… = P a"
using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ennreal_def[symmetric] AE_count_space)
finally show ?thesis ..
qed
lemma distributed_cong_density:
"(AE x in N. f x = g x) ⟹ g ∈ borel_measurable N ⟹ f ∈ borel_measurable N ⟹
distributed M N X f ⟷ distributed M N X g"
by (auto simp: distributed_def intro!: density_cong)
lemma (in prob_space) distributed_imp_emeasure_nonzero:
assumes X: "distributed M MX X Px"
shows "emeasure MX {x ∈ space MX. Px x ≠ 0} ≠ 0"
proof
note Px = distributed_borel_measurable[OF X]
interpret X: prob_space "distr M MX X"
using distributed_measurable[OF X] by (rule prob_space_distr)
assume "emeasure MX {x ∈ space MX. Px x ≠ 0} = 0"
with Px have "AE x in MX. Px x = 0"
by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ennreal_iff)
moreover
from X.emeasure_space_1 have "(∫⇧+x. Px x ∂MX) = 1"
unfolding distributed_distr_eq_density[OF X] using Px
by (subst (asm) emeasure_density)
(auto simp: borel_measurable_ennreal_iff intro!: integral_cong cong: nn_integral_cong)
ultimately show False
by (simp add: nn_integral_cong_AE)
qed
lemma subdensity:
assumes T: "T ∈ measurable P Q"
assumes f: "distributed M P X f"
assumes g: "distributed M Q Y g"
assumes Y: "Y = T ∘ X"
shows "AE x in P. g (T x) = 0 ⟶ f x = 0"
proof -
have "{x∈space Q. g x = 0} ∈ null_sets (distr M Q (T ∘ X))"
using g Y by (auto simp: null_sets_density_iff distributed_def)
also have "distr M Q (T ∘ X) = distr (distr M P X) Q T"
using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
finally have "T -` {x∈space Q. g x = 0} ∩ space P ∈ null_sets (distr M P X)"
using T by (subst (asm) null_sets_distr_iff) auto
also have "T -` {x∈space Q. g x = 0} ∩ space P = {x∈space P. g (T x) = 0}"
using T by (auto dest: measurable_space)
finally show ?thesis
using f g by (auto simp add: null_sets_density_iff distributed_def)
qed
lemma subdensity_real:
fixes g :: "'a ⇒ real" and f :: "'b ⇒ real"
assumes T: "T ∈ measurable P Q"
assumes f: "distributed M P X f"
assumes g: "distributed M Q Y g"
assumes Y: "Y = T ∘ X"
shows "(AE x in P. 0 ≤ g (T x)) ⟹ (AE x in P. 0 ≤ f x) ⟹ AE x in P. g (T x) = 0 ⟶ f x = 0"
using subdensity[OF T, of M X "λx. ennreal (f x)" Y "λx. ennreal (g x)"] assms
by auto
lemma distributed_emeasure:
"distributed M N X f ⟹ A ∈ sets N ⟹ emeasure M (X -` A ∩ space M) = (∫⇧+x. f x * indicator A x ∂N)"
by (auto simp: distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
lemma distributed_nn_integral:
"distributed M N X f ⟹ g ∈ borel_measurable N ⟹ (∫⇧+x. f x * g x ∂N) = (∫⇧+x. g (X x) ∂M)"
by (auto simp: distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)
lemma distributed_integral:
"distributed M N X f ⟹ g ∈ borel_measurable N ⟹ (⋀x. x ∈ space N ⟹ 0 ≤ f x) ⟹
(∫x. f x * g x ∂N) = (∫x. g (X x) ∂M)"
supply distributed_real_measurable[measurable]
by (auto simp: distributed_distr_eq_density[symmetric] integral_real_density[symmetric] integral_distr)
lemma distributed_transform_integral:
assumes Px: "distributed M N X Px" "⋀x. x ∈ space N ⟹ 0 ≤ Px x"
assumes "distributed M P Y Py" "⋀x. x ∈ space P ⟹ 0 ≤ Py x"
assumes Y: "Y = T ∘ X" and T: "T ∈ measurable N P" and f: "f ∈ borel_measurable P"
shows "(∫x. Py x * f x ∂P) = (∫x. Px x * f (T x) ∂N)"
proof -
have "(∫x. Py x * f x ∂P) = (∫x. f (Y x) ∂M)"
by (rule distributed_integral) fact+
also have "… = (∫x. f (T (X x)) ∂M)"
using Y by simp
also have "… = (∫x. Px x * f (T x) ∂N)"
using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)
finally show ?thesis .
qed
lemma (in prob_space) distributed_unique:
assumes Px: "distributed M S X Px"
assumes Py: "distributed M S X Py"
shows "AE x in S. Px x = Py x"
proof -
interpret X: prob_space "distr M S X"
using Px by (intro prob_space_distr) simp
have "sigma_finite_measure (distr M S X)" ..
with sigma_finite_density_unique[of Px S Py ] Px Py
show ?thesis
by (auto simp: distributed_def)
qed
lemma (in prob_space) distributed_jointI:
assumes "sigma_finite_measure S" "sigma_finite_measure T"
assumes X[measurable]: "X ∈ measurable M S" and Y[measurable]: "Y ∈ measurable M T"
assumes [measurable]: "f ∈ borel_measurable (S ⨂⇩M T)" and f: "AE x in S ⨂⇩M T. 0 ≤ f x"
assumes eq: "⋀A B. A ∈ sets S ⟹ B ∈ sets T ⟹
emeasure M {x ∈ space M. X x ∈ A ∧ Y x ∈ B} = (∫⇧+x. (∫⇧+y. f (x, y) * indicator B y ∂T) * indicator A x ∂S)"
shows "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) f"
unfolding distributed_def
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
interpret ST: pair_sigma_finite S T ..
from ST.sigma_finite_up_in_pair_measure_generator
obtain F :: "nat ⇒ ('b × 'c) set"
where F: "range F ⊆ {A × B |A B. A ∈ sets S ∧ B ∈ sets T} ∧ incseq F ∧
⋃ (range F) = space S × space T ∧ (∀i. emeasure (S ⨂⇩M T) (F i) ≠ ∞)" ..
let ?E = "{a × b |a b. a ∈ sets S ∧ b ∈ sets T}"
let ?P = "S ⨂⇩M T"
show "distr M ?P (λx. (X x, Y x)) = density ?P f" (is "?L = ?R")
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
show "?E ⊆ Pow (space ?P)"
using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
show "sets ?L = sigma_sets (space ?P) ?E"
by (simp add: sets_pair_measure space_pair_measure)
then show "sets ?R = sigma_sets (space ?P) ?E"
by simp
next
interpret L: prob_space ?L
by (rule prob_space_distr) (auto intro!: measurable_Pair)
show "range F ⊆ ?E" "(⋃i. F i) = space ?P" "⋀i. emeasure ?L (F i) ≠ ∞"
using F by (auto simp: space_pair_measure)
next
fix E assume "E ∈ ?E"
then obtain A B where E[simp]: "E = A × B"
and A[measurable]: "A ∈ sets S" and B[measurable]: "B ∈ sets T" by auto
have "emeasure ?L E = emeasure M {x ∈ space M. X x ∈ A ∧ Y x ∈ B}"
by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
also have "… = (∫⇧+x. (∫⇧+y. (f (x, y) * indicator B y) * indicator A x ∂T) ∂S)"
using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
also have "… = emeasure ?R E"
by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
intro!: nn_integral_cong split: split_indicator)
finally show "emeasure ?L E = emeasure ?R E" .
qed
qed (auto simp: f)
lemma (in prob_space) distributed_swap:
assumes "sigma_finite_measure S" "sigma_finite_measure T"
assumes Pxy: "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) Pxy"
shows "distributed M (T ⨂⇩M S) (λx. (Y x, X x)) (λ(x, y). Pxy (y, x))"
proof -
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
interpret ST: pair_sigma_finite S T ..
interpret TS: pair_sigma_finite T S ..
note Pxy[measurable]
show ?thesis
apply (subst TS.distr_pair_swap)
unfolding distributed_def
proof safe
let ?D = "distr (S ⨂⇩M T) (T ⨂⇩M S) (λ(x, y). (y, x))"
show 1: "(λ(x, y). Pxy (y, x)) ∈ borel_measurable ?D"
by auto
show 2: "random_variable (distr (S ⨂⇩M T) (T ⨂⇩M S) (λ(x, y). (y, x))) (λx. (Y x, X x))"
using Pxy by auto
{ fix A assume A: "A ∈ sets (T ⨂⇩M S)"
let ?B = "(λ(x, y). (y, x)) -` A ∩ space (S ⨂⇩M T)"
from sets.sets_into_space[OF A]
have "emeasure M ((λx. (Y x, X x)) -` A ∩ space M) =
emeasure M ((λx. (X x, Y x)) -` ?B ∩ space M)"
by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
also have "… = (∫⇧+ x. Pxy x * indicator ?B x ∂(S ⨂⇩M T))"
using Pxy A by (intro distributed_emeasure) auto
finally have "emeasure M ((λx. (Y x, X x)) -` A ∩ space M) =
(∫⇧+ x. Pxy x * indicator A (snd x, fst x) ∂(S ⨂⇩M T))"
by (auto intro!: nn_integral_cong split: split_indicator) }
note * = this
show "distr M ?D (λx. (Y x, X x)) = density ?D (λ(x, y). Pxy (y, x))"
apply (intro measure_eqI)
apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
apply (subst nn_integral_distr)
apply (auto intro!: * simp: comp_def split_beta)
done
qed
qed
lemma (in prob_space) distr_marginal1:
assumes "sigma_finite_measure S" "sigma_finite_measure T"
assumes Pxy: "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) Pxy"
defines "Px ≡ λx. (∫⇧+z. Pxy (x, z) ∂T)"
shows "distributed M S X Px"
unfolding distributed_def
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
interpret ST: pair_sigma_finite S T ..
note Pxy[measurable]
show X: "X ∈ measurable M S" by simp
show borel: "Px ∈ borel_measurable S"
by (auto intro!: T.nn_integral_fst simp: Px_def)
interpret Pxy: prob_space "distr M (S ⨂⇩M T) (λx. (X x, Y x))"
by (intro prob_space_distr) simp
show "distr M S X = density S Px"
proof (rule measure_eqI)
fix A assume A: "A ∈ sets (distr M S X)"
with X measurable_space[of Y M T]
have "emeasure (distr M S X) A = emeasure (distr M (S ⨂⇩M T) (λx. (X x, Y x))) (A × space T)"
by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
also have "… = emeasure (density (S ⨂⇩M T) Pxy) (A × space T)"
using Pxy by (simp add: distributed_def)
also have "… = ∫⇧+ x. ∫⇧+ y. Pxy (x, y) * indicator (A × space T) (x, y) ∂T ∂S"
using A borel Pxy
by (simp add: emeasure_density T.nn_integral_fst[symmetric])
also have "… = ∫⇧+ x. Px x * indicator A x ∂S"
proof (rule nn_integral_cong)
fix x assume "x ∈ space S"
moreover have eq: "⋀y. y ∈ space T ⟹ indicator (A × space T) (x, y) = indicator A x"
by (auto simp: indicator_def)
ultimately have "(∫⇧+ y. Pxy (x, y) * indicator (A × space T) (x, y) ∂T) = (∫⇧+ y. Pxy (x, y) ∂T) * indicator A x"
by (simp add: eq nn_integral_multc cong: nn_integral_cong)
also have "(∫⇧+ y. Pxy (x, y) ∂T) = Px x"
by (simp add: Px_def)
finally show "(∫⇧+ y. Pxy (x, y) * indicator (A × space T) (x, y) ∂T) = Px x * indicator A x" .
qed
finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
using A borel Pxy by (simp add: emeasure_density)
qed simp
qed
lemma (in prob_space) distr_marginal2:
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
assumes Pxy: "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) Pxy"
shows "distributed M T Y (λy. (∫⇧+x. Pxy (x, y) ∂S))"
using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp
lemma (in prob_space) distributed_marginal_eq_joint1:
assumes T: "sigma_finite_measure T"
assumes S: "sigma_finite_measure S"
assumes Px: "distributed M S X Px"
assumes Pxy: "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) Pxy"
shows "AE x in S. Px x = (∫⇧+y. Pxy (x, y) ∂T)"
using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)
lemma (in prob_space) distributed_marginal_eq_joint2:
assumes T: "sigma_finite_measure T"
assumes S: "sigma_finite_measure S"
assumes Py: "distributed M T Y Py"
assumes Pxy: "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) Pxy"
shows "AE y in T. Py y = (∫⇧+x. Pxy (x, y) ∂S)"
using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
lemma (in prob_space) distributed_joint_indep':
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
assumes indep: "distr M S X ⨂⇩M distr M T Y = distr M (S ⨂⇩M T) (λx. (X x, Y x))"
shows "distributed M (S ⨂⇩M T) (λx. (X x, Y x)) (λ(x, y). Px x * Py y)"
unfolding distributed_def
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
interpret ST: pair_sigma_finite S T ..
interpret X: prob_space "density S Px"
unfolding distributed_distr_eq_density[OF X, symmetric]
by (rule prob_space_distr) simp
have sf_X: "sigma_finite_measure (density S Px)" ..
interpret Y: prob_space "density T Py"
unfolding distributed_distr_eq_density[OF Y, symmetric]
by (rule prob_space_distr) simp
have sf_Y: "sigma_finite_measure (density T Py)" ..
show "distr M (S ⨂⇩M T) (λx. (X x, Y x)) = density (S ⨂⇩M T) (λ(x, y). Px x * Py y)"
unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
using distributed_borel_measurable[OF X]
using distributed_borel_measurable[OF Y]
by (rule pair_measure_density[OF _ _ T sf_Y])
show "random_variable (S ⨂⇩M T) (λx. (X x, Y x))" by auto
show Pxy: "(λ(x, y). Px x * Py y) ∈ borel_measurable (S ⨂⇩M T)" by auto
qed
lemma distributed_integrable:
"distributed M N X f ⟹ g ∈ borel_measurable N ⟹ (⋀x. x ∈ space N ⟹ 0 ≤ f x) ⟹
integrable N (λx. f x * g x) ⟷ integrable M (λx. g (X x))"
supply distributed_real_measurable[measurable]
by (auto simp: distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
lemma distributed_transform_integrable:
assumes Px: "distributed M N X Px" "⋀x. x ∈ space N ⟹ 0 ≤ Px x"
assumes "distributed M P Y Py" "⋀x. x ∈ space P ⟹ 0 ≤ Py x"
assumes Y: "Y = (λx. T (X x))" and T: "T ∈ measurable N P" and f: "f ∈ borel_measurable P"
shows "integrable P (λx. Py x * f x) ⟷ integrable N (λx. Px x * f (T x))"
proof -
have "integrable P (λx. Py x * f x) ⟷ integrable M (λx. f (Y x))"
by (rule distributed_integrable) fact+
also have "… ⟷ integrable M (λx. f (T (X x)))"
using Y by simp
also have "… ⟷ integrable N (λx. Px x * f (T x))"
using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
finally show ?thesis .
qed
lemma distributed_integrable_var:
fixes X :: "'a ⇒ real"
shows "distributed M lborel X (λx. ennreal (f x)) ⟹ (⋀x. 0 ≤ f x) ⟹
integrable lborel (λx. f x * x) ⟹ integrable M X"
using distributed_integrable[of M lborel X f "λx. x"] by simp
lemma (in prob_space) distributed_variance:
fixes f::"real ⇒ real"
assumes D: "distributed M lborel X f" and [simp]: "⋀x. 0 ≤ f x"
shows "variance X = (∫x. x⇧2 * f (x + expectation X) ∂lborel)"
proof (subst distributed_integral[OF D, symmetric])
show "(∫ x. f x * (x - expectation X)⇧2 ∂lborel) = (∫ x. x⇧2 * f (x + expectation X) ∂lborel)"
by (subst lborel_integral_real_affine[where c=1 and t="expectation X"]) (auto simp: ac_simps)
qed simp_all
lemma (in prob_space) variance_affine:
fixes f::"real ⇒ real"
assumes [arith]: "b ≠ 0"
assumes D[intro]: "distributed M lborel X f"
assumes [simp]: "prob_space (density lborel f)"
assumes I[simp]: "integrable M X"
assumes I2[simp]: "integrable M (λx. (X x)⇧2)"
shows "variance (λx. a + b * X x) = b⇧2 * variance X"
by (subst variance_eq)
(auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib)
definition
"simple_distributed M X f ⟷
(∀x. 0 ≤ f x) ∧
distributed M (count_space (X`space M)) X (λx. ennreal (f x)) ∧
finite (X`space M)"
lemma simple_distributed_nonneg[dest]: "simple_distributed M X f ⟹ 0 ≤ f x"
by (auto simp: simple_distributed_def)
lemma simple_distributed:
"simple_distributed M X Px ⟹ distributed M (count_space (X`space M)) X Px"
unfolding simple_distributed_def by auto
lemma simple_distributed_finite[dest]: "simple_distributed M X P ⟹ finite (X`space M)"
by (simp add: simple_distributed_def)
lemma (in prob_space) distributed_simple_function_superset:
assumes X: "simple_function M X" "⋀x. x ∈ X ` space M ⟹ P x = measure M (X -` {x} ∩ space M)"
assumes A: "X`space M ⊆ A" "finite A"
defines "S ≡ count_space A" and "P' ≡ (λx. if x ∈ X`space M then P x else 0)"
shows "distributed M S X P'"
unfolding distributed_def
proof safe
show "(λx. ennreal (P' x)) ∈ borel_measurable S" unfolding S_def by simp
show "distr M S X = density S P'"
proof (rule measure_eqI_finite)
show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
using A unfolding S_def by auto
show "finite A" by fact
fix a assume a: "a ∈ A"
then have "a ∉ X`space M ⟹ X -` {a} ∩ space M = {}" by auto
with A a X have "emeasure (distr M S X) {a} = P' a"
by (subst emeasure_distr)
(auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
intro!: arg_cong[where f=prob])
also have "… = (∫⇧+x. ennreal (P' a) * indicator {a} x ∂S)"
using A X a
by (subst nn_integral_cmult_indicator)
(auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
also have "… = (∫⇧+x. ennreal (P' x) * indicator {a} x ∂S)"
by (auto simp: indicator_def intro!: nn_integral_cong)
also have "… = emeasure (density S P') {a}"
using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
qed
show "random_variable S X"
using X(1) A by (auto simp: measurable_def simple_functionD S_def)
qed
lemma (in prob_space) simple_distributedI:
assumes X: "simple_function M X"
"⋀x. 0 ≤ P x"
"⋀x. x ∈ X ` space M ⟹ P x = measure M (X -` {x} ∩ space M)"
shows "simple_distributed M X P"
unfolding simple_distributed_def
proof (safe intro!: X)
have "distributed M (count_space (X ` space M)) X (λx. ennreal (if x ∈ X`space M then P x else 0))"
(is "?A")
using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X(1,3)]) auto
also have "?A ⟷ distributed M (count_space (X ` space M)) X (λx. ennreal (P x))"
by (rule distributed_cong_density) auto
finally show "…" .
qed (rule simple_functionD[OF X(1)])
lemma simple_distributed_joint_finite:
assumes X: "simple_distributed M (λx. (X x, Y x)) Px"
shows "finite (X ` space M)" "finite (Y ` space M)"
proof -
have "finite ((λx. (X x, Y x)) ` space M)"
using X by (auto simp: simple_distributed_def simple_functionD)
then have "finite (fst ` (λx. (X x, Y x)) ` space M)" "finite (snd ` (λx. (X x, Y x)) ` space M)"
by auto
then show fin: "finite (X ` space M)" "finite (Y ` space M)"
by (auto simp: image_image)
qed
lemma simple_distributed_joint2_finite:
assumes X: "simple_distributed M (λx. (X x, Y x, Z x)) Px"
shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
proof -
have "finite ((λx. (X x, Y x, Z x)) ` space M)"
using X by (auto simp: simple_distributed_def simple_functionD)
then have "finite (fst ` (λx. (X x, Y x, Z x)) ` space M)"
"finite ((fst ∘ snd) ` (λx. (X x, Y x, Z x)) ` space M)"
"finite ((snd ∘ snd) ` (λx. (X x, Y x, Z x)) ` space M)"
by auto
then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
by (auto simp: image_image)
qed
lemma simple_distributed_simple_function:
"simple_distributed M X Px ⟹ simple_function M X"
unfolding simple_distributed_def distributed_def
by (auto simp: simple_function_def measurable_count_space_eq2)
lemma simple_distributed_measure:
"simple_distributed M X P ⟹ a ∈ X`space M ⟹ P a = measure M (X -` {a} ∩ space M)"
using distributed_count_space[of M "X`space M" X P a, symmetric]
by (auto simp: simple_distributed_def measure_def)
lemma (in prob_space) simple_distributed_joint:
assumes X: "simple_distributed M (λx. (X x, Y x)) Px"
defines "S ≡ count_space (X`space M) ⨂⇩M count_space (Y`space M)"
defines "P ≡ (λx. if x ∈ (λx. (X x, Y x))`space M then Px x else 0)"
shows "distributed M S (λx. (X x, Y x)) P"
proof -
from simple_distributed_joint_finite[OF X, simp]
have S_eq: "S = count_space (X`space M × Y`space M)"
by (simp add: S_def pair_measure_count_space)
show ?thesis
unfolding S_eq P_def
proof (rule distributed_simple_function_superset)
show "simple_function M (λx. (X x, Y x))"
using X by (rule simple_distributed_simple_function)
fix x assume "x ∈ (λx. (X x, Y x)) ` space M"
from simple_distributed_measure[OF X this]
show "Px x = prob ((λx. (X x, Y x)) -` {x} ∩ space M)" .
qed auto
qed
lemma (in prob_space) simple_distributed_joint2:
assumes X: "simple_distributed M (λx. (X x, Y x, Z x)) Px"
defines "S ≡ count_space (X`space M) ⨂⇩M count_space (Y`space M) ⨂⇩M count_space (Z`space M)"
defines "P ≡ (λx. if x ∈ (λx. (X x, Y x, Z x))`space M then Px x else 0)"
shows "distributed M S (λx. (X x, Y x, Z x)) P"
proof -
from simple_distributed_joint2_finite[OF X, simp]
have S_eq: "S = count_space (X`space M × Y`space M × Z`space M)"
by (simp add: S_def pair_measure_count_space)
show ?thesis
unfolding S_eq P_def
proof (rule distributed_simple_function_superset)
show "simple_function M (λx. (X x, Y x, Z x))"
using X by (rule simple_distributed_simple_function)
fix x assume "x ∈ (λx. (X x, Y x, Z x)) ` space M"
from simple_distributed_measure[OF X this]
show "Px x = prob ((λx. (X x, Y x, Z x)) -` {x} ∩ space M)" .
qed auto
qed
lemma (in prob_space) simple_distributed_sum_space:
assumes X: "simple_distributed M X f"
shows "sum f (X`space M) = 1"
proof -
from X have "sum f (X`space M) = prob (⋃i∈X`space M. X -` {i} ∩ space M)"
by (subst finite_measure_finite_Union)
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD
intro!: sum.cong arg_cong[where f="prob"])
also have "… = prob (space M)"
by (auto intro!: arg_cong[where f=prob])
finally show ?thesis
using emeasure_space_1 by (simp add: emeasure_eq_measure)
qed
lemma (in prob_space) distributed_marginal_eq_joint_simple:
assumes Px: "simple_function M X"
assumes Py: "simple_distributed M Y Py"
assumes Pxy: "simple_distributed M (λx. (X x, Y x)) Pxy"
assumes y: "y ∈ Y`space M"
shows "Py y = (∑x∈X`space M. if (x, y) ∈ (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0)"
proof -
note Px = simple_distributedI[OF Px measure_nonneg refl]
have "AE y in count_space (Y ` space M). ennreal (Py y) =
∫⇧+ x. ennreal (if (x, y) ∈ (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0) ∂count_space (X ` space M)"
using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite
simple_distributed[OF Py] simple_distributed_joint[OF Pxy]
by (rule distributed_marginal_eq_joint2)
(auto intro: Py Px simple_distributed_finite)
then have "ennreal (Py y) =
(∑x∈X`space M. ennreal (if (x, y) ∈ (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0))"
using y Px[THEN simple_distributed_finite]
by (auto simp: AE_count_space nn_integral_count_space_finite)
also have "… = (∑x∈X`space M. if (x, y) ∈ (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0)"
using Pxy by (intro sum_ennreal) auto
finally show ?thesis
using simple_distributed_nonneg[OF Py] simple_distributed_nonneg[OF Pxy]
by (subst (asm) ennreal_inj) (auto intro!: sum_nonneg)
qed
lemma distributedI_real:
fixes f :: "'a ⇒ real"
assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E"
and A: "range A ⊆ E" "(⋃i::nat. A i) = space M1" "⋀i. emeasure (distr M M1 X) (A i) ≠ ∞"
and X: "X ∈ measurable M M1"
and f: "f ∈ borel_measurable M1" "AE x in M1. 0 ≤ f x"
and eq: "⋀A. A ∈ E ⟹ emeasure M (X -` A ∩ space M) = (∫⇧+ x. f x * indicator A x ∂M1)"
shows "distributed M M1 X f"
unfolding distributed_def
proof (intro conjI)
show "distr M M1 X = density M1 f"
proof (rule measure_eqI_generator_eq[where A=A])
{ fix A assume A: "A ∈ E"
then have "A ∈ sigma_sets (space M1) E" by auto
then have "A ∈ sets M1"
using gen by simp
with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A"
by (auto simp add: emeasure_distr emeasure_density ennreal_indicator
intro!: nn_integral_cong split: split_indicator) }
note eq_E = this
show "Int_stable E" by fact
{ fix e assume "e ∈ E"
then have "e ∈ sigma_sets (space M1) E" by auto
then have "e ∈ sets M1" unfolding gen .
then have "e ⊆ space M1" by (rule sets.sets_into_space) }
then show "E ⊆ Pow (space M1)" by auto
show "sets (distr M M1 X) = sigma_sets (space M1) E"
"sets (density M1 (λx. ennreal (f x))) = sigma_sets (space M1) E"
unfolding gen[symmetric] by auto
qed fact+
qed (insert X f, auto)
lemma distributedI_borel_atMost:
fixes f :: "real ⇒ real"
assumes [measurable]: "X ∈ borel_measurable M"
and [measurable]: "f ∈ borel_measurable borel" and f[simp]: "AE x in lborel. 0 ≤ f x"
and g_eq: "⋀a. (∫⇧+x. f x * indicator {..a} x ∂lborel) = ennreal (g a)"
and M_eq: "⋀a. emeasure M {x∈space M. X x ≤ a} = ennreal (g a)"
shows "distributed M lborel X f"
proof (rule distributedI_real)
show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)"
by (simp add: borel_eq_atMost)
show "Int_stable (range atMost :: real set set)"
by (auto simp: Int_stable_def)
have vimage_eq: "⋀a. (X -` {..a} ∩ space M) = {x∈space M. X x ≤ a}" by auto
define A where "A i = {.. real i}" for i :: nat
then show "range A ⊆ range atMost" "(⋃i. A i) = space lborel"
"⋀i. emeasure (distr M lborel X) (A i) ≠ ∞"
by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq)
fix A :: "real set" assume "A ∈ range atMost"
then obtain a where A: "A = {..a}" by auto
show "emeasure M (X -` A ∩ space M) = (∫⇧+x. f x * indicator A x ∂lborel)"
unfolding vimage_eq A M_eq g_eq ..
qed auto
lemma (in prob_space) uniform_distributed_params:
assumes X: "distributed M MX X (λx. indicator A x / measure MX A)"
shows "A ∈ sets MX" "measure MX A ≠ 0"
proof -
interpret X: prob_space "distr M MX X"
using distributed_measurable[OF X] by (rule prob_space_distr)
show "measure MX A ≠ 0"
proof
assume "measure MX A = 0"
with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
show False
by (simp add: emeasure_density zero_ennreal_def[symmetric])
qed
with measure_notin_sets[of A MX] show "A ∈ sets MX"
by blast
qed
lemma prob_space_uniform_measure:
assumes A: "emeasure M A ≠ 0" "emeasure M A ≠ ∞"
shows "prob_space (uniform_measure M A)"
proof
show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
by (simp add: Int_absorb2 less_top)
qed
lemma prob_space_uniform_count_measure: "finite A ⟹ A ≠ {} ⟹ prob_space (uniform_count_measure A)"
by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ennreal_def)
lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
shows "𝒫(x in uniform_measure M {x∈space M. Q x}. P x) = 𝒫(x in M. P x ¦ Q x)"
proof cases
assume Q: "measure M {x∈space M. Q x} = 0"
then have *: "AE x in M. ¬ Q x"
by (simp add: prob_eq_0)
then have "density M (λx. indicator {x ∈ space M. Q x} x / emeasure M {x ∈ space M. Q x}) = density M (λx. 0)"
by (intro density_cong) auto
with * show ?thesis
unfolding uniform_measure_def
by (simp add: emeasure_density measure_def cond_prob_def emeasure_eq_0_AE)
next
assume Q: "measure M {x∈space M. Q x} ≠ 0"
then show "𝒫(x in uniform_measure M {x ∈ space M. Q x}. P x) = cond_prob M P Q"
by (subst measure_uniform_measure)
(auto simp: emeasure_eq_measure cond_prob_def measure_nonneg intro!: arg_cong[where f=prob])
qed
lemma prob_space_point_measure:
"finite S ⟹ (⋀s. s ∈ S ⟹ 0 ≤ p s) ⟹ (∑s∈S. p s) = 1 ⟹ prob_space (point_measure S p)"
by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)
lemma (in prob_space) distr_pair_fst: "distr (N ⨂⇩M M) N fst = N"
proof (intro measure_eqI)
fix A assume A: "A ∈ sets (distr (N ⨂⇩M M) N fst)"
from A have "emeasure (distr (N ⨂⇩M M) N fst) A = emeasure (N ⨂⇩M M) (A × space M)"
by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure])
with A show "emeasure (distr (N ⨂⇩M M) N fst) A = emeasure N A"
by (simp add: emeasure_pair_measure_Times emeasure_space_1)
qed simp
lemma (in product_prob_space) distr_reorder:
assumes "inj_on t J" "t ∈ J → K" "finite K"
shows "distr (PiM K M) (Pi⇩M J (λx. M (t x))) (λω. λn∈J. ω (t n)) = PiM J (λx. M (t x))"
proof (rule product_sigma_finite.PiM_eqI)
show "product_sigma_finite (λx. M (t x))" ..
have "t`J ⊆ K" using assms by auto
then show [simp]: "finite J"
by (rule finite_imageD[OF finite_subset]) fact+
fix A assume A: "⋀i. i ∈ J ⟹ A i ∈ sets (M (t i))"
moreover have "((λω. λn∈J. ω (t n)) -` Pi⇩E J A ∩ space (Pi⇩M K M)) =
(Π⇩E i∈K. if i ∈ t`J then A (the_inv_into J t i) else space (M i))"
using A A[THEN sets.sets_into_space] ‹t ∈ J → K› ‹inj_on t J›
by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def)
ultimately show "distr (Pi⇩M K M) (Pi⇩M J (λx. M (t x))) (λω. λn∈J. ω (t n)) (Pi⇩E J A) = (∏i∈J. M (t i) (A i))"
using assms
apply (subst emeasure_distr)
apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
apply (subst emeasure_PiM)
apply (auto simp: the_inv_into_f_f ‹inj_on t J› prod.reindex[OF ‹inj_on t J›]
if_distrib[where f="emeasure (M _)"] prod.If_cases emeasure_space_1 Int_absorb1 ‹t`J ⊆ K›)
done
qed simp
lemma (in product_prob_space) distr_restrict:
"J ⊆ K ⟹ finite K ⟹ (Π⇩M i∈J. M i) = distr (Π⇩M i∈K. M i) (Π⇩M i∈J. M i) (λf. restrict f J)"
using distr_reorder[of "λx. x" J K] by (simp add: Pi_iff subset_eq)
lemma (in product_prob_space) emeasure_prod_emb[simp]:
assumes L: "J ⊆ L" "finite L" and X: "X ∈ sets (Pi⇩M J M)"
shows "emeasure (Pi⇩M L M) (prod_emb L M J X) = emeasure (Pi⇩M J M) X"
by (subst distr_restrict[OF L])
(simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
lemma emeasure_distr_restrict:
assumes "I ⊆ K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A ∈ sets (PiM I M)"
shows "emeasure (distr Q (PiM I M) (λω. restrict ω I)) A = emeasure Q (prod_emb K M I A)"
using ‹I⊆K› sets_eq_imp_space_eq[OF Q]
by (subst emeasure_distr)
(auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict)
lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
by (rule prob_spaceI) (simp add: emeasure_space_1)
lemma distr_PiM_finite_prob_space:
assumes fin: "finite I"
assumes "product_prob_space M"
assumes "product_prob_space M'"
assumes [measurable]: "⋀i. i ∈ I ⟹ f ∈ measurable (M i) (M' i)"
shows "distr (PiM I M) (PiM I M') (compose I f) = PiM I (λi. distr (M i) (M' i) f)"
proof -
interpret M: product_prob_space M by fact
interpret M': product_prob_space M' by fact
define N where "N = (λi. if i ∈ I then distr (M i) (M' i) f else M' i)"
have [intro]: "prob_space (N i)" for i
by (auto simp: N_def intro!: M.M.prob_space_distr M'.prob_space)
interpret N: product_prob_space N
by (intro product_prob_spaceI) (auto simp: N_def M'.prob_space intro: M.M.prob_space_distr)
have "distr (PiM I M) (PiM I M') (compose I f) = PiM I N"
proof (rule N.PiM_eqI)
have N_events_eq: "sets (Pi⇩M I N) = sets (Pi⇩M I M')"
unfolding N_def by (intro sets_PiM_cong) auto
also have "… = sets (distr (Pi⇩M I M) (Pi⇩M I M') (compose I f))"
by simp
finally show "sets (distr (Pi⇩M I M) (Pi⇩M I M') (compose I f)) = sets (Pi⇩M I N)" ..
fix A assume A: "⋀i. i ∈ I ⟹ A i ∈ N.M.events i"
have "emeasure (distr (Pi⇩M I M) (Pi⇩M I M') (compose I f)) (Pi⇩E I A) =
emeasure (Pi⇩M I M) (compose I f -` Pi⇩E I A ∩ space (Pi⇩M I M))"
proof (intro emeasure_distr)
show "compose I f ∈ Pi⇩M I M →⇩M Pi⇩M I M'"
unfolding compose_def by measurable
show "Pi⇩E I A ∈ sets (Pi⇩M I M')"
unfolding N_events_eq [symmetric] by (intro sets_PiM_I_finite fin A)
qed
also have "compose I f -` Pi⇩E I A ∩ space (Pi⇩M I M) = Pi⇩E I (λi. f -` A i ∩ space (M i))"
using A by (auto simp: space_PiM PiE_def Pi_def extensional_def N_def compose_def)
also have "emeasure (Pi⇩M I M) (Pi⇩E I (λi. f -` A i ∩ space (M i))) =
(∏i∈I. emeasure (M i) (f -` A i ∩ space (M i)))"
using A by (intro M.emeasure_PiM fin) (auto simp: N_def)
also have "… = (∏i∈I. emeasure (distr (M i) (M' i) f) (A i))"
using A by (intro prod.cong emeasure_distr [symmetric]) (auto simp: N_def)
also have "… = (∏i∈I. emeasure (N i) (A i))"
unfolding N_def by (intro prod.cong) (auto simp: N_def)
finally show "emeasure (distr (Pi⇩M I M) (Pi⇩M I M') (compose I f)) (Pi⇩E I A) = …" .
qed fact+
also have "PiM I N = PiM I (λi. distr (M i) (M' i) f)"
by (intro PiM_cong) (auto simp: N_def)
finally show ?thesis .
qed
end