# Theory Preliminary_Results

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

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"
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
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"

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)"

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)}"
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)"
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"
then obtain y where y_def: "⋀j. j ∈ J ⟹ x j = {y j}"

have "⋂ (A  J) ⊆ set_pmf p" using b a(2) by blast
hence "R.prob (⋂ (A  J)) = prob (⋂ j ∈ J. A j)"
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)
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"

hence "R.indep_vars (λ_. discrete) X I"
unfolding  R.indep_vars_def2

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"

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 ω)})"
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

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"
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"