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  jJ. A' j  A j 
      measure (distr M N f) ( (A' ` J)) = (jJ. 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)) = (jJ. 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" "jJ. 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)) = (jJ. 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 "... = (jJ. 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