Theory Probability_Misc

theory Probability_Misc
imports Probability
(*
  File:      Probability_Misc.thy
  Authors:   Max Haslbeck, Manuel Eberl

  Miscellaneous facts about measures and probability that are missing from the library and
  should perhaps be moved there at some point.
*)
section ‹Auxiliary material›
theory Probability_Misc
  imports "HOL-Probability.Probability"
begin

lemma measure_eqI_countable_AE':
  assumes [simp]: "sets M = Pow B" "sets N = Pow B" and subset: "Ω ⊆ B"
  assumes ae: "AE x in M. x ∈ Ω" "AE x in N. x ∈ Ω" and [simp]: "countable Ω"
  assumes eq: "⋀x. x ∈ Ω ⟹ emeasure M {x} = emeasure N {x}"
  shows "M = N"
proof (rule measure_eqI)
  fix A assume A: "A ∈ sets M"
  have "emeasure N A = emeasure N {x∈Ω. x ∈ A}"
    using ae subset A by (intro emeasure_eq_AE) auto
  also have "… = (∫+x. emeasure N {x} ∂count_space {x∈Ω. x ∈ A})"
    using A subset by (intro emeasure_countable_singleton) auto
  also have "… = (∫+x. emeasure M {x} ∂count_space {x∈Ω. x ∈ A})"
    by (intro nn_integral_cong eq[symmetric]) auto
  also have "… = emeasure M {x∈Ω. x ∈ A}"
    using A subset by (intro emeasure_countable_singleton[symmetric]) auto
  also have "… = emeasure M A"
    using ae A subset by (intro emeasure_eq_AE) auto
  finally show "emeasure M A = emeasure N A" ..
qed simp

lemma measurable_le[measurable (raw)]:
  fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
  assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "Measurable.pred M (λx. f x ≤ g x)"
  unfolding pred_def by (intro borel_measurable_le assms)

lemma measurable_eq[measurable (raw)]:
  fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
  assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "Measurable.pred M (λx. f x = g x)"
  unfolding pred_def by (intro borel_measurable_eq assms)

context
  fixes M :: "'a measure"
  assumes singleton_null_set: "x ∈ space M ⟹ {x} ∈ null_sets M"
begin

lemma countable_null_set:
  assumes "countable A" "A ⊆ space M"
  shows   "A ∈ null_sets M"
proof -
  have "(⋃x∈A. {x}) ∈ null_sets M" using assms 
    by (intro null_sets_UN' assms singleton_null_set) auto
  also have "(⋃x∈A. {x}) = A" by simp
  finally show ?thesis .
qed

lemma finite_null_set:
  assumes "finite A" "A ⊆ space M"
  shows   "A ∈ null_sets M"
  using countable_finite[OF assms(1)] countable_null_set[OF _ assms(2)] by simp
    
end

lemma measurable_inj_on_finite:
  assumes fin [measurable]: "finite I"
  assumes [measurable]: "⋀i j. Measurable.pred (M i ⨂M M j) (λ(x,y). x = y)"
  shows   "Measurable.pred (PiM I M) (λx. inj_on x I)" unfolding inj_on_def
  by measurable
    
lemma almost_everywhere_not_in_countable_set:
  assumes "countable A"
  assumes [measurable]: "Measurable.pred (M ⨂M M) (λ(x,y). x = y)"
  assumes null: "⋀x. x ∈ space M ⟹ {x} ∈ null_sets M"
  shows   "AE x in M. x ∉ A"
proof -
  have "A ∩ space M ∈ null_sets M"
    by (rule countable_null_set) (insert assms(1), auto intro: null)
  hence "AE x in M. ∀y∈A. x ≠ y" by (rule AE_I') auto
  also have "?this ⟷ ?thesis" by (intro AE_cong) auto
  finally show ?thesis .
qed
    
lemma almost_everywhere_inj_on_PiM:
  assumes fin: "finite I" and prob_space: "⋀i. i ∈ I ⟹ prob_space (M i)"
  assumes [measurable]: "⋀i j. Measurable.pred (M i ⨂M M j) (λ(x,y). x = y)"
  assumes null: "⋀i x. i ∈ I ⟹ x ∈ space (M i) ⟹ {x} ∈ null_sets (M i)"
  shows   "AE f in (ΠM i∈I. M i). inj_on f I"
proof -
  note [measurable] = measurable_inj_on_finite
  define I' where "I' = I"
  hence "I ⊆ I'" by simp
  from fin and this show ?thesis
  proof (induction I rule: finite_induct)
    case (insert i I)
    interpret pair_sigma_finite "M i" "PiM I M"
      unfolding pair_sigma_finite_def using insert.prems
      by (auto intro!: prob_space_imp_sigma_finite prob_space prob_space_PiM simp: I'_def)
    from insert.hyps have [measurable]: "finite (insert i I)" by simp
    have "PiM (insert i I) M = distr (M i ⨂M PiM I M) (PiM (insert i I) M) (λ(x, X). X(i := x))"
      using insert.prems 
      by (intro distr_pair_PiM_eq_PiM [symmetric] prob_space) (auto simp: I'_def)
    also have "(AE f in …. inj_on f (insert i I)) ⟷ 
                 (AE x in M i ⨂M PiM I M. inj_on ((snd x)(i := fst x)) (insert i I))"
      by (subst AE_distr_iff; measurable) (simp add: case_prod_unfold)?
    also have "… = (AE x in M i. AE y in PiM I M. inj_on (y(i := x)) (insert i I))"
      by (rule AE_pair_iff [symmetric]) measurable
    also have "… ⟷ (AE x in M i. AE y in PiM I M. inj_on (y(i := x)) I) ∧
                      (AE x in M i. AE y in PiM I M. x ∉ y(i := x) ` (I - {i}))" by simp
    also have 
    proof (rule conjI, goal_cases)
      case 1
      from insert.prems have "AE f in PiM I M. inj_on f I" by (intro insert.IH) auto
      hence "AE f in PiM I M. inj_on (f(i := x)) I" for x
        by eventually_elim (insert insert.hyps, auto simp: inj_on_def)
      thus ?case by blast
    next
      note [measurable] = ‹finite I›
      {
        fix f
        have "f ` I ∩ space (M i) ∈ null_sets (M i)"
          by (rule finite_null_set) 
             (insert insert.hyps insert.prems, auto intro!: null simp: I'_def)
        hence "AE x in M i. x ∉ f(i := x) ` I"
          by (rule AE_I') (insert insert.hyps, auto split: if_splits)
        also have "(AE x in M i. x ∉ f(i := x) ` I) ⟷ (AE x in M i. ∀y∈I. f y ≠ x)"
          using insert.hyps by (intro AE_cong) (auto split: if_splits)
        finally have "…" .
      }
      hence "AE f in PiM I M. AE x in M i. ∀y∈I. f y ≠ x" by blast
      hence "AE x in M i. AE f in PiM I M. ∀y∈I. f y ≠ x"
        by (subst AE_commute) simp_all
      also have "?this ⟷ (AE x in M i. AE y in PiM I M. x ∉ y(i := x) ` (I - {i}))"
        using insert.hyps by (intro AE_cong) (auto split: if_splits)
      finally show  .
    qed
    finally show ?case .
  qed auto
qed
  

lemma null_sets_uniform_measure:
  assumes "A ∈ sets M" "emeasure M A ≠ ∞"
  shows   "null_sets (uniform_measure M A) = (λB. A ∩ B) -` null_sets M ∩ sets M"
  using assms by (auto simp: null_sets_def)

lemma almost_everywhere_avoid_finite:
  assumes fin: "finite I"
  shows   "AE f in (ΠM i∈I. uniform_measure lborel {(0::real)..1}). inj_on f I"
proof (intro almost_everywhere_inj_on_PiM fin prob_space_uniform_measure)
  fix x :: real
  show "{x} ∈ null_sets (uniform_measure lborel {0..1})"
    by (cases "x ∈ {0..1}") (auto simp: null_sets_uniform_measure)
qed auto
  
lemma almost_everywhere_avoid_countable:
  assumes "countable A"
  shows   "AE x in uniform_measure lborel {(0::real)..1}. x ∉ A"
proof (intro almost_everywhere_not_in_countable_set assms prob_space_uniform_measure)
  fix x :: real
  show "{x} ∈ null_sets (uniform_measure lborel {0..1})"
    by (cases "x ∈ {0..1}") (auto simp: null_sets_uniform_measure)
qed auto

lemma measure_pmf_of_set:
  assumes "A ≠ {}" and "finite A" 
  shows   "measure_pmf (pmf_of_set A) = uniform_measure (count_space UNIV) A"
    using assms
  by (intro measure_eqI)
     (auto simp: emeasure_pmf_of_set divide_ennreal [symmetric] card_gt_0_iff
                  ennreal_of_nat_eq_real_of_nat)

lemma emeasure_distr_restrict:
  assumes "f ∈ M →M N" "f ∈ M' →M N'" "A ∈ sets N'" "sets M' ⊆ sets M" "sets N' ⊆ sets N"
  assumes "⋀X. X ∈ sets M' ⟹ emeasure M X = emeasure M' X"
  assumes "⋀X. X ∈ sets M ⟹ X ⊆ space M - space M' ⟹ emeasure M X = 0"
  shows   "emeasure (distr M N f) A= emeasure (distr M' N' f) A"
proof -
  have space_subset: "space M' ⊆ space M"
    using ‹sets M' ⊆ sets M› by (simp add: sets_le_imp_space_le)
  have "emeasure (distr M N f) A = emeasure M (f -` A ∩ space M)"
    using assms by (subst emeasure_distr) auto
  also have "f -` A ∩ space M = f -` A ∩ space M' ∪ f -` A ∩ (space M - space M')"
    using space_subset by blast
  also have "emeasure M … = emeasure M (f -` A ∩ space M')"
  proof (intro emeasure_Un_null_set)
    show "f -` A ∩ space M' ∈ sets M"
      using assms by auto
    have "f -` A ∩ (space M - space M') ∈ sets M"
      using assms by (metis Int_Diff measurable_sets sets.Diff sets.top subsetCE)
    moreover from this have "emeasure M (f -` A ∩ (space M - space M')) = 0"
      by (intro assms) auto
    ultimately show "f -` A ∩ (space M - space M') ∈ null_sets M"
      unfolding null_sets_def by blast
  qed
  also have "… = emeasure M' (f -` A ∩ space M')"
    using assms by (intro assms) auto
  also have "… = emeasure (distr M' N' f) A"
    using assms by (subst emeasure_distr) auto
  finally show ?thesis .
qed

lemma distr_uniform_measure_count_space_inj:
  assumes "inj_on f A'" "A' ⊆ A" "f ` A ⊆ B" "finite A'"
  shows   "distr (uniform_measure (count_space A) A') (count_space B) f =
             uniform_measure (count_space B) (f ` A')" (is "?lhs = ?rhs")
proof (rule measure_eqI, goal_cases)
  case (2 X)
  hence X_subset: "X ⊆ B" by simp
  from assms have eq: "f ` A' ∩ X = f ` (A' ∩ (f -` X ∩ A))"
    by auto
  from assms have [measurable]: "f ∈ count_space A →M count_space B"
    by (subst measurable_count_space_eq1) auto
  from X_subset have "emeasure ?lhs X = 
                        emeasure (uniform_measure (count_space A) A') (f -` X ∩ A)"
    by (subst emeasure_distr) auto
  also from assms X_subset 
    have "… = emeasure (count_space A) (A' ∩ (f -` X ∩ A)) / emeasure (count_space A) A'"
    by (intro emeasure_uniform_measure) auto
  also from assms have "… = of_nat (card (A' ∩ (f -` X ∩ A))) / of_nat (card A')"
    by (subst (1 2) emeasure_count_space) auto
  also have "card (A' ∩ (f -` X ∩ A)) = card (f ` (A' ∩ (f -` X ∩ A)))"
    using assms by (intro card_image [symmetric]) (auto simp: inj_on_def)
  also have "f ` (A' ∩ (f -` X ∩ A)) = f ` A' ∩ X"
    using assms by auto
  also have "of_nat (card A') = of_nat (card (f ` A'))"
    using assms by (subst card_image) auto
  also have "of_nat (card (f ` A' ∩ X)) / … = 
               emeasure (count_space B) (f ` A' ∩ X) / emeasure (count_space B) (f ` A')"
    using assms by (subst (1 2) emeasure_count_space) auto
  also from assms X_subset have "… = emeasure ?rhs X" 
    by (intro emeasure_uniform_measure [symmetric]) auto
  finally show ?case .
qed simp_all

lemma (in pair_prob_space) pair_measure_bind:
  assumes [measurable]: "f ∈ M1 ⨂M M2 →M subprob_algebra N"
  shows "(M1 ⨂M M2) ⤜ f = do {x ← M1; y ← M2; f (x, y)}"
proof -
  note M1 = M1.prob_space_axioms and M2 = M2.prob_space_axioms
  have [measurable]: "M1 ∈ space (subprob_algebra M1)"
    by (rule M1.M_in_subprob)
  have [measurable]: "M2 ∈ space (subprob_algebra M2)"
    by (rule M2.M_in_subprob)
  have "(M1 ⨂M M2) = M1 ⤜ (λx. M2 ⤜ (λy. return (M1 ⨂M M2) (x, y)))"
    by (subst pair_measure_eq_bind) simp_all
  also have "… ⤜ f = M1 ⤜ (λx. (M2 ⤜ (λy. return (M1 ⨂M M2) (x, y))) ⤜ f)"
    by (rule bind_assoc) measurable
  also have "… = M1 ⤜ (λx. M2 ⤜ (λxa. return (M1 ⨂M M2) (x, xa) ⤜ f))"
    by (intro bind_cong refl bind_assoc) measurable
  also have "… = do {x ← M1; y ← M2; f (x, y)}"
    by (intro bind_cong refl bind_return)
       (measurable, simp_all add: space_pair_measure)
  finally show ?thesis .
qed

lemma count_space_singleton_conv_return: 
  "count_space {x} = return (count_space {x}) x"
proof (rule measure_eqI)
  fix A assume "A ∈ sets (count_space {x})"
  hence "A ⊆ {x}" by auto
  hence "A = {} ∨ A = {x}" by (cases "x ∈ A") auto
  thus "emeasure (count_space {x}) A = emeasure (return (count_space {x}) x) A"
    by auto
qed auto
  
lemma distr_count_space_singleton [simp]:
    "f x ∈ space M ⟹ distr (count_space {x}) M f = return M (f x)"
  by (subst count_space_singleton_conv_return, subst distr_return) simp_all

lemma uniform_measure_count_space_singleton [simp]:
  assumes "{x} ∈ sets M" "emeasure M {x} ≠ 0" "emeasure M {x} < ∞"
  shows   "uniform_measure M {x} = return M x"
proof (rule measure_eqI)
  fix A assume A: "A ∈ sets (uniform_measure M {x})"
  show "emeasure (uniform_measure M {x}) A = emeasure (return M x) A"
    by (cases "x ∈ A") (insert assms A, auto)
qed simp_all

lemma PiM_uniform_measure_permute:
  fixes a b :: real
  assumes "g permutes A" "a < b"
  shows   "distr (PiM A (λ_. uniform_measure lborel {a..b})) (PiM A (λ_. lborel)) (λf. f ∘ g) =
             PiM A (λ_. uniform_measure lborel {a..b})"
proof -
  have "distr (PiM A (λ_. uniform_measure lborel {a..b})) (PiM A (λ_. lborel)) (λf. f ∘ g) =
          distr (PiM A (λ_. uniform_measure lborel {a..b})) 
            (PiM A (λ_. uniform_measure lborel {a..b})) (λf. λx∈A. f (g x))" using assms
    by (intro distr_cong sets_PiM_cong refl) 
       (auto simp: fun_eq_iff space_PiM PiE_def extensional_def permutes_in_image[of g A])  
  also from assms have "… = PiM A (λi. uniform_measure lborel {a..b})"
    by (intro distr_PiM_reindex)
       (auto simp: permutes_inj_on permutes_in_image[of g A] intro!: prob_space_uniform_measure)
  finally show ?thesis .
qed

lemma ennreal_fact [simp]: "ennreal (fact n) = fact n"
  by (induction n) (auto simp: algebra_simps ennreal_mult' ennreal_of_nat_eq_real_of_nat)

lemma inverse_ennreal_unique:
  assumes "a * (b :: ennreal) = 1"
  shows   "b = inverse a"
  using assms
  by (metis divide_ennreal_def ennreal_inverse_1 ennreal_top_eq_mult_iff mult.comm_neutral 
        mult_divide_eq_ennreal mult_eq_0_iff semiring_normalization_rules(7))

end