(* Title: HOL/Probability/Probability_Measure.thy Author: Johannes Hölzl, TU München Author: Armin Heller, TU München *) 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" proof - interpret finite_measure M proof show "emeasure M (space M) ≠ ∞" using * by simp qed show "prob_space M" by standard fact qed 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" using emeasure_space_1 unfolding measure_def by (simp add: one_ennreal.rep_eq) 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 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!