Theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
section ‹Preliminary Results›
theory Universal_Hash_Families_More_Independent_Families
imports
Universal_Hash_Families
"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)
lemma (in prob_space) k_wise_indep_vars_triv:
assumes "indep_vars N T I"
shows "k_wise_indep_vars k N T I"
using assms indep_vars_subset unfolding k_wise_indep_vars_def by auto
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