(* File: Probability_Misc.thy Authors: Max Haslbeck, Manuel Eberl Miscellaneous facts about measures and probability that are missing from the library and should perhaps be moved there at some point. *) section ‹Auxiliary material› theory Probability_Misc imports "HOL-Probability.Probability" begin lemma measure_eqI_countable_AE': assumes [simp]: "sets M = Pow B" "sets N = Pow B" and subset: "Ω ⊆ B" assumes ae: "AE x in M. x ∈ Ω" "AE x in N. x ∈ Ω" and [simp]: "countable Ω" assumes eq: "⋀x. x ∈ Ω ⟹ emeasure M {x} = emeasure N {x}" shows "M = N" proof (rule measure_eqI) fix A assume A: "A ∈ sets M" have "emeasure N A = emeasure N {x∈Ω. x ∈ A}" using ae subset A by (intro emeasure_eq_AE) auto also have "… = (∫⇧^{+}x. emeasure N {x} ∂count_space {x∈Ω. x ∈ A})" using A subset by (intro emeasure_countable_singleton) auto also have "… = (∫⇧^{+}x. emeasure M {x} ∂count_space {x∈Ω. x ∈ A})" by (intro nn_integral_cong eq[symmetric]) auto also have "… = emeasure M {x∈Ω. x ∈ A}" using A subset by (intro emeasure_countable_singleton[symmetric]) auto also have "… = emeasure M A" using ae A subset by (intro emeasure_eq_AE) auto finally show "emeasure M A = emeasure N A" .. qed simp lemma measurable_le[measurable (raw)]: fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "Measurable.pred M (λx. f x ≤ g x)" unfolding pred_def by (intro borel_measurable_le assms) lemma measurable_eq[measurable (raw)]: fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "Measurable.pred M (λx. f x = g x)" unfolding pred_def by (intro borel_measurable_eq assms) context fixes M :: "'a measure" assumes singleton_null_set: "x ∈ space M ⟹ {x} ∈ null_sets M" begin lemma countable_null_set: assumes "countable A" "A ⊆ space M" shows "A ∈ null_sets M" proof - have "(⋃x∈A. {x}) ∈ null_sets M" using assms by (intro null_sets_UN' assms singleton_null_set) auto also have "(⋃x∈A. {x}) = A" by simp finally show ?thesis . qed lemma finite_null_set: assumes "finite A" "A ⊆ space M" shows "A ∈ null_sets M" using countable_finite[OF assms(1)] countable_null_set[OF _ assms(2)] by simp end lemma measurable_inj_on_finite: assumes fin [measurable]: "finite I" assumes [measurable]: "⋀i j. Measurable.pred (M i ⨂⇩_{M}M j) (λ(x,y). x = y)" shows "Measurable.pred (Pi⇩_{M}I M) (λx. inj_on x I)" unfolding inj_on_def by measurable lemma almost_everywhere_not_in_countable_set: assumes "countable A" assumes [measurable]: "Measurable.pred (M ⨂⇩_{M}M) (λ(x,y). x = y)" assumes null: "⋀x. x ∈ space M ⟹ {x} ∈ null_sets M" shows "AE x in M. x ∉ A" proof - have "A ∩ space M ∈ null_sets M" by (rule countable_null_set) (insert assms(1), auto intro: null) hence "AE x in M. ∀y∈A. x ≠ y" by (rule AE_I') auto also have "?this ⟷ ?thesis" by (intro AE_cong) auto finally show ?thesis . qed lemma almost_everywhere_inj_on_PiM: assumes fin: "finite I" and prob_space: "⋀i. i ∈ I ⟹ prob_space (M i)" assumes [measurable]: "⋀i j. Measurable.pred (M i ⨂⇩_{M}M j) (λ(x,y). x = y)" assumes null: "⋀i x. i ∈ I ⟹ x ∈ space (M i) ⟹ {x} ∈ null_sets (M i)" shows "AE f in (Π⇩_{M}i∈I. M i). inj_on f I" proof - note [measurable] = measurable_inj_on_finite define I' where "I' = I" hence "I ⊆ I'" by simp from fin and this show ?thesis proof (induction I rule: finite_induct) case (insert i I) interpret pair_sigma_finite "M i" "PiM I M" unfolding pair_sigma_finite_def using insert.prems by (auto intro!: prob_space_imp_sigma_finite prob_space prob_space_PiM simp: I'_def) from insert.hyps have [measurable]: "finite (insert i I)" by simp have "PiM (insert i I) M = distr (M i ⨂⇩_{M}Pi⇩_{M}I M) (Pi⇩_{M}(insert i I) M) (λ(x, X). X(i := x))" using insert.prems by (intro distr_pair_PiM_eq_PiM [symmetric] prob_space) (auto simp: I'_def) also have "(AE f in …. inj_on f (insert i I)) ⟷ (AE x in M i ⨂⇩_{M}Pi⇩_{M}I M. inj_on ((snd x)(i := fst x)) (insert i I))" by (subst AE_distr_iff; measurable) (simp add: case_prod_unfold)? also have "… = (AE x in M i. AE y in Pi⇩_{M}I M. inj_on (y(i := x)) (insert i I))" by (rule AE_pair_iff [symmetric]) measurable also have "… ⟷ (AE x in M i. AE y in Pi⇩_{M}I M. inj_on (y(i := x)) I) ∧ (AE x in M i. AE y in Pi⇩_{M}I M. x ∉ y(i := x) ` (I - {i}))" by simp also have … proof (rule conjI, goal_cases) case 1 from insert.prems have "AE f in Pi⇩_{M}I M. inj_on f I" by (intro insert.IH) auto hence "AE f in Pi⇩_{M}I M. inj_on (f(i := x)) I" for x by eventually_elim (insert insert.hyps, auto simp: inj_on_def) thus ?case by blast next note [measurable] = ‹finite I› { fix f have "f ` I ∩ space (M i) ∈ null_sets (M i)" by (rule finite_null_set) (insert insert.hyps insert.prems, auto intro!: null simp: I'_def) hence "AE x in M i. x ∉ f(i := x) ` I" by (rule AE_I') (insert insert.hyps, auto split: if_splits) also have "(AE x in M i. x ∉ f(i := x) ` I) ⟷ (AE x in M i. ∀y∈I. f y ≠ x)" using insert.hyps by (intro AE_cong) (auto split: if_splits) finally have "…" . } hence "AE f in Pi⇩_{M}I M. AE x in M i. ∀y∈I. f y ≠ x" by blast hence "AE x in M i. AE f in Pi⇩_{M}I M. ∀y∈I. f y ≠ x" by (subst AE_commute) simp_all also have "?this ⟷ (AE x in M i. AE y in Pi⇩_{M}I M. x ∉ y(i := x) ` (I - {i}))" using insert.hyps by (intro AE_cong) (auto split: if_splits) finally show … . qed finally show ?case . qed auto qed lemma null_sets_uniform_measure: assumes "A ∈ sets M" "emeasure M A ≠ ∞" shows "null_sets (uniform_measure M A) = (λB. A ∩ B) -` null_sets M ∩ sets M" using assms by (auto simp: null_sets_def) lemma almost_everywhere_avoid_finite: assumes fin: "finite I" shows "AE f in (Π⇩_{M}i∈I. uniform_measure lborel {(0::real)..1}). inj_on f I" proof (intro almost_everywhere_inj_on_PiM fin prob_space_uniform_measure) fix x :: real show "{x} ∈ null_sets (uniform_measure lborel {0..1})" by (cases "x ∈ {0..1}") (auto simp: null_sets_uniform_measure) qed auto lemma almost_everywhere_avoid_countable: assumes "countable A" shows "AE x in uniform_measure lborel {(0::real)..1}. x ∉ A" proof (intro almost_everywhere_not_in_countable_set assms prob_space_uniform_measure) fix x :: real show "{x} ∈ null_sets (uniform_measure lborel {0..1})" by (cases "x ∈ {0..1}") (auto simp: null_sets_uniform_measure) qed auto lemma measure_pmf_of_set: assumes "A ≠ {}" and "finite A" shows "measure_pmf (pmf_of_set A) = uniform_measure (count_space UNIV) A" using assms by (intro measure_eqI) (auto simp: emeasure_pmf_of_set divide_ennreal [symmetric] card_gt_0_iff ennreal_of_nat_eq_real_of_nat) lemma emeasure_distr_restrict: assumes "f ∈ M →⇩_{M}N" "f ∈ M' →⇩_{M}N'" "A ∈ sets N'" "sets M' ⊆ sets M" "sets N' ⊆ sets N" assumes "⋀X. X ∈ sets M' ⟹ emeasure M X = emeasure M' X" assumes "⋀X. X ∈ sets M ⟹ X ⊆ space M - space M' ⟹ emeasure M X = 0" shows "emeasure (distr M N f) A= emeasure (distr M' N' f) A" proof - have space_subset: "space M' ⊆ space M" using ‹sets M' ⊆ sets M› by (simp add: sets_le_imp_space_le) have "emeasure (distr M N f) A = emeasure M (f -` A ∩ space M)" using assms by (subst emeasure_distr) auto also have "f -` A ∩ space M = f -` A ∩ space M' ∪ f -` A ∩ (space M - space M')" using space_subset by blast also have "emeasure M … = emeasure M (f -` A ∩ space M')" proof (intro emeasure_Un_null_set) show "f -` A ∩ space M' ∈ sets M" using assms by auto have "f -` A ∩ (space M - space M') ∈ sets M" using assms by (metis Int_Diff measurable_sets sets.Diff sets.top subsetCE) moreover from this have "emeasure M (f -` A ∩ (space M - space M')) = 0" by (intro assms) auto ultimately show "f -` A ∩ (space M - space M') ∈ null_sets M" unfolding null_sets_def by blast qed also have "… = emeasure M' (f -` A ∩ space M')" using assms by (intro assms) auto also have "… = emeasure (distr M' N' f) A" using assms by (subst emeasure_distr) auto finally show ?thesis . qed lemma distr_uniform_measure_count_space_inj: assumes "inj_on f A'" "A' ⊆ A" "f ` A ⊆ B" "finite A'" shows "distr (uniform_measure (count_space A) A') (count_space B) f = uniform_measure (count_space B) (f ` A')" (is "?lhs = ?rhs") proof (rule measure_eqI, goal_cases) case (2 X) hence X_subset: "X ⊆ B" by simp from assms have eq: "f ` A' ∩ X = f ` (A' ∩ (f -` X ∩ A))" by auto from assms have [measurable]: "f ∈ count_space A →⇩_{M}count_space B" by (subst measurable_count_space_eq1) auto from X_subset have "emeasure ?lhs X = emeasure (uniform_measure (count_space A) A') (f -` X ∩ A)" by (subst emeasure_distr) auto also from assms X_subset have "… = emeasure (count_space A) (A' ∩ (f -` X ∩ A)) / emeasure (count_space A) A'" by (intro emeasure_uniform_measure) auto also from assms have "… = of_nat (card (A' ∩ (f -` X ∩ A))) / of_nat (card A')" by (subst (1 2) emeasure_count_space) auto also have "card (A' ∩ (f -` X ∩ A)) = card (f ` (A' ∩ (f -` X ∩ A)))" using assms by (intro card_image [symmetric]) (auto simp: inj_on_def) also have "f ` (A' ∩ (f -` X ∩ A)) = f ` A' ∩ X" using assms by auto also have "of_nat (card A') = of_nat (card (f ` A'))" using assms by (subst card_image) auto also have "of_nat (card (f ` A' ∩ X)) / … = emeasure (count_space B) (f ` A' ∩ X) / emeasure (count_space B) (f ` A')" using assms by (subst (1 2) emeasure_count_space) auto also from assms X_subset have "… = emeasure ?rhs X" by (intro emeasure_uniform_measure [symmetric]) auto finally show ?case . qed simp_all lemma (in pair_prob_space) pair_measure_bind: assumes [measurable]: "f ∈ M1 ⨂⇩_{M}M2 →⇩_{M}subprob_algebra N" shows "(M1 ⨂⇩_{M}M2) ⤜ f = do {x ← M1; y ← M2; f (x, y)}" proof - note M1 = M1.prob_space_axioms and M2 = M2.prob_space_axioms have [measurable]: "M1 ∈ space (subprob_algebra M1)" by (rule M1.M_in_subprob) have [measurable]: "M2 ∈ space (subprob_algebra M2)" by (rule M2.M_in_subprob) have "(M1 ⨂⇩_{M}M2) = M1 ⤜ (λx. M2 ⤜ (λy. return (M1 ⨂⇩_{M}M2) (x, y)))" by (subst pair_measure_eq_bind) simp_all also have "… ⤜ f = M1 ⤜ (λx. (M2 ⤜ (λy. return (M1 ⨂⇩_{M}M2) (x, y))) ⤜ f)" by (rule bind_assoc) measurable also have "… = M1 ⤜ (λx. M2 ⤜ (λxa. return (M1 ⨂⇩_{M}M2) (x, xa) ⤜ f))" by (intro bind_cong refl bind_assoc) measurable also have "… = do {x ← M1; y ← M2; f (x, y)}" by (intro bind_cong refl bind_return) (measurable, simp_all add: space_pair_measure) finally show ?thesis . qed lemma count_space_singleton_conv_return: "count_space {x} = return (count_space {x}) x" proof (rule measure_eqI) fix A assume "A ∈ sets (count_space {x})" hence "A ⊆ {x}" by auto hence "A = {} ∨ A = {x}" by (cases "x ∈ A") auto thus "emeasure (count_space {x}) A = emeasure (return (count_space {x}) x) A" by auto qed auto lemma distr_count_space_singleton [simp]: "f x ∈ space M ⟹ distr (count_space {x}) M f = return M (f x)" by (subst count_space_singleton_conv_return, subst distr_return) simp_all lemma uniform_measure_count_space_singleton [simp]: assumes "{x} ∈ sets M" "emeasure M {x} ≠ 0" "emeasure M {x} < ∞" shows "uniform_measure M {x} = return M x" proof (rule measure_eqI) fix A assume A: "A ∈ sets (uniform_measure M {x})" show "emeasure (uniform_measure M {x}) A = emeasure (return M x) A" by (cases "x ∈ A") (insert assms A, auto) qed simp_all lemma PiM_uniform_measure_permute: fixes a b :: real assumes "g permutes A" "a < b" shows "distr (PiM A (λ_. uniform_measure lborel {a..b})) (PiM A (λ_. lborel)) (λf. f ∘ g) = PiM A (λ_. uniform_measure lborel {a..b})" proof - have "distr (PiM A (λ_. uniform_measure lborel {a..b})) (PiM A (λ_. lborel)) (λf. f ∘ g) = distr (PiM A (λ_. uniform_measure lborel {a..b})) (PiM A (λ_. uniform_measure lborel {a..b})) (λf. λx∈A. f (g x))" using assms by (intro distr_cong sets_PiM_cong refl) (auto simp: fun_eq_iff space_PiM PiE_def extensional_def permutes_in_image[of g A]) also from assms have "… = Pi⇩_{M}A (λi. uniform_measure lborel {a..b})" by (intro distr_PiM_reindex) (auto simp: permutes_inj_on permutes_in_image[of g A] intro!: prob_space_uniform_measure) finally show ?thesis . qed lemma ennreal_fact [simp]: "ennreal (fact n) = fact n" by (induction n) (auto simp: algebra_simps ennreal_mult' ennreal_of_nat_eq_real_of_nat) lemma inverse_ennreal_unique: assumes "a * (b :: ennreal) = 1" shows "b = inverse a" using assms by (metis divide_ennreal_def ennreal_inverse_1 ennreal_top_eq_mult_iff mult.comm_neutral mult_divide_eq_ennreal mult_eq_0_iff semiring_normalization_rules(7)) end