section ‹Preliminary Results› theory Preliminary_Results imports "Definitions" "HOL-Probability.Stream_Space" "HOL-Probability.Probability_Mass_Function" begin lemma set_comp_image_cong: assumes "⋀x. P x ⟹ f x = h (g x)" shows "{f x| x. P x} = h ` {g x| x. P x}" using assms by (auto simp: setcompr_eq_image) lemma (in prob_space) k_wise_indep_vars_compose: assumes "k_wise_indep_vars k M' X I" assumes "⋀i. i ∈ I ⟹ Y i ∈ measurable (M' i) (N i)" shows "k_wise_indep_vars k N (λi x. Y i (X i x)) I" using indep_vars_compose2[where N="N" and X="X" and Y="Y" and M'="M'"] assms by (simp add: k_wise_indep_vars_def subsetD) text ‹The following two lemmas are of independent interest, they help infer independence of events and random variables on distributions. (Candidates for @{theory "HOL-Probability.Independent_Family"}).› lemma (in prob_space) indep_sets_distr: fixes A assumes "random_variable N f" defines "F ≡ (λi. (λa. f -` a ∩ space M) ` A i)" assumes indep_F: "indep_sets F I" assumes sets_A: "⋀i. i ∈ I ⟹ A i ⊆ sets N" shows "prob_space.indep_sets (distr M N f) A I" proof (rule prob_space.indep_setsI) show "⋀A' J. J ≠ {} ⟹ J ⊆ I ⟹ finite J ⟹ ∀j∈J. A' j ∈ A j ⟹ measure (distr M N f) (⋂ (A' ` J)) = (∏j∈J. measure (distr M N f) (A' j))" proof - fix A' J assume a:"J ⊆ I" "finite J" "J ≠ {}" "∀j ∈ J. A' j ∈ A j" define F' where "F' = (λi. f -` A' i ∩ space M)" have "⋂ (F' ` J) = f -` (⋂ (A' ` J)) ∩ space M" unfolding set_eq_iff F'_def using a(3) by simp moreover have "⋂ (A' ` J) ∈ sets N" by (metis a sets_A sets.finite_INT subset_iff) ultimately have b: "measure (distr M N f) (⋂ (A' ` J)) = measure M (⋂ (F' ` J))" by (metis assms(1) measure_distr) have "⋀j. j ∈ J ⟹ F' j ∈ F j" using a(4) F'_def F_def by blast hence c:"measure M (⋂ (F' ` J)) = (∏j∈ J. measure M (F' j))" by (metis indep_F indep_setsD a(1,2,3)) have "⋀j. j ∈ J ⟹ F' j = f -` A' j ∩ space M" by (simp add:F'_def) moreover have "⋀j. j ∈ J ⟹ A' j ∈ sets N" using a(1,4) sets_A by blast ultimately have d: "⋀j. j ∈ J ⟹ measure M (F' j) = measure (distr M N f) (A' j)" using assms(1) measure_distr by metis show "measure (distr M N f) (⋂ (A' ` J)) = (∏j∈J. measure (distr M N f) (A' j))" using b c d by auto qed show "prob_space (distr M N f)" using prob_space_distr assms by blast show "⋀i. i ∈ I ⟹ A i ⊆ sets (distr M N f)" using sets_A sets_distr by blast qed lemma (in prob_space) indep_vars_distr: assumes "f ∈ measurable M N" assumes "⋀i. i ∈ I ⟹ X' i ∈ measurable N (M' i)" assumes "indep_vars M' (λi. (X' i) ∘ f) I" shows "prob_space.indep_vars (distr M N f) M' X' I" proof - interpret D: prob_space "(distr M N f)" using prob_space_distr[OF assms(1)] by simp have a: "f ∈ space M → space N" using assms(1) by (simp add:measurable_def) have "D.indep_sets (λi. {X' i -` A ∩ space N |A. A ∈ sets (M' i)}) I" proof (rule indep_sets_distr[OF assms(1)]) have "⋀i. i ∈ I ⟹ {(X' i ∘ f) -` A ∩ space M |A. A ∈ sets (M' i)} = (λa. f -` a ∩ space M) ` {X' i -` A ∩ space N |A. A ∈ sets (M' i)}" by (rule set_comp_image_cong, simp add:set_eq_iff, use a in blast) thus "indep_sets (λi. (λa. f -` a ∩ space M) ` {X' i -` A ∩ space N |A. A ∈ sets (M' i)}) I" using assms(3) by (simp add:indep_vars_def2 cong:indep_sets_cong) next fix i assume "i ∈ I" thus "{X' i -` A ∩ space N |A. A ∈ sets (M' i)} ⊆ sets N" using assms(2) measurable_sets by blast qed thus ?thesis using assms by (simp add:D.indep_vars_def2) qed lemma range_inter: "range ((∩) F) = Pow F" unfolding image_def by auto text ‹The singletons and the empty set form an intersection stable generator of a countable discrete $\sigma$-algebra:› lemma sigma_sets_singletons_and_empty: assumes "countable M" shows "sigma_sets M (insert {} ((λk. {k}) ` M)) = Pow M" proof - have "sigma_sets M ((λk. {k}) ` M) = Pow M" using assms sigma_sets_singletons by auto hence "Pow M ⊆ sigma_sets M (insert {} ((λk. {k}) ` M))" by (metis sigma_sets_subseteq subset_insertI) moreover have "(insert {} ((λk. {k}) ` M)) ⊆ Pow M" by blast hence "sigma_sets M (insert {} ((λk. {k}) ` M)) ⊆ Pow M" by (meson sigma_algebra.sigma_sets_subset sigma_algebra_Pow) ultimately show ?thesis by force qed text ‹In some of the following theorems, the premise @{term "M = measure_pmf p"} is used. This allows stating theorems that hold for pmfs more concisely, for example, instead of @{term "measure_pmf.prob p A ≤ measure_pmf.prob p B"} we can just write @{term "M = measure_pmf p ⟹ prob A ≤ prob B"} in the locale @{locale "prob_space"}.› lemma prob_space_restrict_space: assumes [simp]:"M = measure_pmf p" shows "prob_space (restrict_space M (set_pmf p))" by (rule prob_spaceI, auto simp:emeasure_restrict_space emeasure_pmf) text ‹The abbreviation below is used to specify the discrete $\sigma$-algebra on @{term "UNIV"} as a measure space. It is used in places where the existing definitions, such as @{term "indep_vars"}, expect a measure space even though only a \emph{measurable} space is really needed, i.e., in cases where the property is invariant with respect to the actual measure.› hide_const (open) discrete abbreviation "discrete ≡ count_space UNIV" lemma (in prob_space) indep_vars_restrict_space: assumes [simp]:"M = measure_pmf p" assumes "prob_space.indep_vars (restrict_space M (set_pmf p)) (λ_. discrete) X I" shows "indep_vars (λ_. discrete) X I" proof - have a: "id ∈ restrict_space M (set_pmf p) →⇩_{M}M" by (simp add:measurable_def range_inter sets_restrict_space) have "prob_space.indep_vars (distr (restrict_space M (set_pmf p)) M id) (λ_. discrete) X I" using assms a prob_space_restrict_space by (auto intro!:prob_space.indep_vars_distr) moreover have "⋀A. emeasure (distr (restrict_space M (set_pmf p)) M id) A = emeasure M A" using emeasure_distr[OF a] by (auto simp add: emeasure_restrict_space emeasure_Int_set_pmf) hence "distr (restrict_space M p) M id = M" by (auto intro: measure_eqI) ultimately show ?thesis by simp qed lemma (in prob_space) measure_pmf_eq: assumes "M = measure_pmf p" assumes "⋀x. x ∈ set_pmf p ⟹ (x ∈ P) = (x ∈ Q)" shows "prob P = prob Q" unfolding assms(1) by (rule measure_eq_AE, rule AE_pmfI[OF assms(2)], auto) text ‹The following lemma is an intro rule for the independence of random variables defined on pmfs. In that case it is possible, to check the independence of random variables point-wise. The proof relies on the fact that the support of a pmf is countable and the $\sigma$-algebra of such a set can be generated by singletons.› lemma (in prob_space) indep_vars_pmf: assumes [simp]:"M = measure_pmf p" assumes "⋀a J. J ⊆ I ⟹ finite J ⟹ prob {ω. ∀i ∈ J. X i ω = a i} = (∏i ∈ J. prob {ω. X i ω = a i})" shows "indep_vars (λ_. discrete) X I" proof - interpret R:prob_space "(restrict_space M (set_pmf p))" using prob_space_restrict_space by auto have events_eq_pow: "R.events = Pow (set_pmf p)" by (simp add:sets_restrict_space range_inter) define G where "G = (λi. {{}} ∪ (λx. {x}) ` (X i ` set_pmf p))" define F where "F = (λi. {X i -` a ∩ set_pmf p|a. a ∈ G i})" have sigma_sets_pow: "⋀i. i ∈ I ⟹ sigma_sets (X i ` set_pmf p) (G i) = Pow (X i ` set_pmf p)" by (simp add:G_def, metis countable_image countable_set_pmf sigma_sets_singletons_and_empty) have F_in_events: "⋀i. i ∈ I ⟹ F i ⊆ Pow (set_pmf p)" unfolding F_def by blast have as_sigma_sets: "⋀i. i ∈ I ⟹ {u. ∃A. u = X i -` A ∩ set_pmf p} = sigma_sets (set_pmf p) (F i)" proof - fix i assume a:"i ∈ I" have "⋀A. X i -` A ∩ set_pmf p = X i -` (A ∩ X i ` set_pmf p) ∩ set_pmf p" by auto hence "{u. ∃A. u = X i -` A ∩ set_pmf p} = {X i -` A ∩ set_pmf p |A. A ⊆ X i ` set_pmf p}" by (metis (no_types, opaque_lifting) inf_le2) also have "... = {X i -` A ∩ set_pmf p |A. A ∈ sigma_sets (X i ` set_pmf p) (G i)}" using a by (simp add:sigma_sets_pow) also have "... = sigma_sets (set_pmf p) {X i -` a ∩ set_pmf p |a. a ∈ G i}" by (subst sigma_sets_vimage_commute[symmetric], auto) also have "... = sigma_sets (set_pmf p) (F i)" by (simp add:F_def) finally show "{u. ∃A. u = X i -` A ∩ set_pmf p} = sigma_sets (set_pmf p) (F i)" by simp qed have F_Int_stable: "⋀i. i ∈ I ⟹ Int_stable (F i)" proof (rule Int_stableI) fix i a b assume "i ∈ I" "a ∈ F i" "b ∈ F i" thus "a ∩ b ∈ (F i)" unfolding F_def G_def by (cases "a ∩ b = {}", auto) qed have F_indep_sets:"R.indep_sets F I" proof (rule R.indep_setsI) fix i assume "i ∈ I" show "F i ⊆ R.events" unfolding F_def events_eq_pow by blast next fix A fix J assume a:"J ⊆ I" "J ≠ {}" "finite J" "∀j∈J. A j ∈ F j" have b: "⋀j. j ∈ J ⟹ A j ⊆ set_pmf p" by (metis PowD a(1,4) subsetD F_in_events) obtain x where x_def:"⋀j. j ∈ J ⟹ A j = X j -` x j ∩ set_pmf p ∧ x j ∈ G j" using a by (simp add:Pi_def F_def, metis) show "R.prob (⋂ (A ` J)) = (∏j∈J. R.prob (A j))" proof (cases "∃j ∈ J. A j = {}") case True hence "⋂ (A ` J) = {}" by blast then show ?thesis using a True by (simp, metis measure_empty) next case False then have "⋀j. j ∈ J ⟹ x j ≠ {}" using x_def by auto hence "⋀j. j ∈ J ⟹ x j ∈ (λx. {x}) ` X j ` set_pmf p" using x_def by (simp add:G_def) then obtain y where y_def: "⋀j. j ∈ J ⟹ x j = {y j}" by (simp add:image_def, metis) have "⋂ (A ` J) ⊆ set_pmf p" using b a(2) by blast hence "R.prob (⋂ (A ` J)) = prob (⋂ j ∈ J. A j)" by (simp add: measure_restrict_space) also have "... = prob ({ω. ∀j ∈ J. X j ω = y j})" using a x_def y_def apply (simp add:vimage_def measure_Int_set_pmf) by (rule arg_cong2 [where f="measure"], auto) also have "... = (∏ j∈ J. prob (A j))" using x_def y_def a assms(2) by (simp add:vimage_def measure_Int_set_pmf) also have "... = (∏j∈J. R.prob (A j))" using b by (simp add: measure_restrict_space cong:prod.cong) finally show ?thesis by blast qed qed have "R.indep_sets (λi. sigma_sets (set_pmf p) (F i)) I" using R.indep_sets_sigma[simplified] F_Int_stable F_indep_sets by (auto simp:space_restrict_space) hence "R.indep_sets (λi. {u. ∃A. u = X i -` A ∩ set_pmf p}) I" by (simp add: as_sigma_sets cong:R.indep_sets_cong) hence "R.indep_vars (λ_. discrete) X I" unfolding R.indep_vars_def2 by (simp add:measurable_def sets_restrict_space range_inter) thus ?thesis using indep_vars_restrict_space[OF assms(1)] by simp qed lemma (in prob_space) split_indep_events: assumes "M = measure_pmf p" assumes "indep_vars (λi. discrete) X' I" assumes "K ⊆ I" "finite K" shows "prob {ω. ∀x ∈ K. P x (X' x ω)} = (∏x ∈ K. prob {ω. P x (X' x ω)})" proof - have [simp]: "space M = UNIV" "events = UNIV" "prob UNIV = 1" by (simp add:assms(1))+ have "indep_vars (λ_. discrete) X' K" using assms(2,3) indep_vars_subset by blast hence "indep_events (λx. {ω ∈ space M. P x (X' x ω)}) K" using indep_eventsI_indep_vars by force hence a:"indep_events (λx. {ω. P x (X' x ω)}) K" by simp have "prob {ω. ∀x ∈ K. P x (X' x ω)} = prob (⋂x ∈ K. {ω. P x (X' x ω)})" by (simp add: measure_pmf_eq[OF assms(1)]) also have "... = (∏ x ∈ K. prob {ω. P x (X' x ω)})" using a assms(4) by (cases "K = {}", auto simp: indep_events_def) finally show ?thesis by simp qed lemma pmf_of_set_eq_uniform: assumes "finite A" "A ≠ {}" shows "measure_pmf (pmf_of_set A) = uniform_measure discrete A" proof - have a:"real (card A) > 0" using assms by (simp add: card_gt_0_iff) have b: "⋀Y. emeasure (pmf_of_set A) Y = emeasure (uniform_measure discrete A) Y" using assms a by (simp add: emeasure_pmf_of_set divide_ennreal ennreal_of_nat_eq_real_of_nat) show ?thesis by (rule measure_eqI, auto simp add: b) qed lemma (in prob_space) uniform_onI: assumes "M = measure_pmf p" assumes "finite A" "A ≠ {}" assumes "⋀a. prob {ω. X ω = a} = indicator A a / card A" shows "uniform_on X A" proof - have a:"⋀a. measure_pmf.prob p {x. X x = a} = indicator A a / card A" using assms(1,4) by simp have b:"map_pmf X p = pmf_of_set A" by (rule pmf_eqI, simp add:assms pmf_map vimage_def a) have "distr M discrete X = map_pmf X p" by (simp add: map_pmf_rep_eq assms(1)) also have "... = measure_pmf (pmf_of_set A)" using b by simp also have "... = uniform_measure discrete A" by (rule pmf_of_set_eq_uniform[OF assms(2,3)]) finally have "distr M discrete X = uniform_measure discrete A" by simp moreover have "random_variable discrete X" by (simp add: assms(1)) ultimately show ?thesis using assms(2,3) by (simp add: uniform_on_def) qed end