Theory Prob_Events_Extras

(* Theory: Prob_Events_Extras
   Author: Chelsea Edmonds *)

section ‹General Event Lemmas›
text ‹General lemmas for reasoning on events in probability spaces after different operations ›

theory Prob_Events_Extras 
  imports 
    "HOL-Probability.Probability" 
    PiE_Rel_Extras
begin

context prob_space
begin

lemma prob_sum_Union:
  assumes measurable: "finite A" "A ⊆ events" "disjoint A"
  shows "prob (⋃A ) = (∑e∈A. prob (e))"
proof -
  obtain f where bb: "bij_betw f {0..<card A} A"
    using assms(1) ex_bij_betw_nat_finite by auto
  then have eq: "f ` {0..<card A} = A"
    by (simp add: bij_betw_imp_surj_on)
  moreover have "inj_on f {0..<card A}"
    using bb bij_betw_def by blast
  ultimately have "disjoint_family_on f {0..<card A}" 
    using disjoint_image_disjoint_family_on[of f "{0..<card A}"] assms by auto
  moreover have "(∑e∈A. prob (e)) = (∑i∈{0..<card A}. prob (f i))" using sum.reindex bb
    by (simp add: sum.reindex_bij_betw) 
  ultimately show ?thesis using finite_measure_finite_Union eq assms(1) assms(2)
    by (metis bb bij_betw_finite) 
qed

lemma events_inter: 
  assumes "finite S"
  assumes "S ≠ {}"
  shows "(⋀ A. A ∈ S ⟹ A ∈ events) ⟹ ⋂S ∈ events"
using assms proof (induct S rule: finite_ne_induct)
  case (singleton x)
  then show ?case by auto
next
  case (insert x F)
  then show ?case using sets.Int
    by (metis complete_lattice_class.Inf_insert insertCI) 
qed

lemma events_union: 
  assumes "finite S"
  shows "(⋀ A. A ∈ S ⟹ A ∈ events) ⟹ ⋃S ∈ events"
using assms(1) proof (induct S rule: finite_induct)
  case empty
  then show ?case by auto
next
  case (insert x F)
  then show ?case using sets.Un
    by (simp add: insertI1) 
qed

lemma prob_inter_set_lt_elem:  "A ∈ events ⟹ prob (A ∩ (⋂AS)) ≤ prob A"
  by (simp add: finite_measure_mono) 

lemma Inter_event_ss: "finite A ⟹ A ⊆ events ⟹ A ≠ {} ⟹ ⋂A ∈ events"
  by (simp add: events_inter subset_iff) 

lemma prob_inter_ss_lt: 
  assumes "finite A"
  assumes "A ⊆ events"
  assumes "B ≠ {}"
  assumes "B ⊆ A"
  shows "prob (⋂A) ≤ prob (⋂B)"
proof (cases "B = A")
  case True
  then show ?thesis by simp
next
  case False
  then obtain C where "C = A - B" and "C ≠ {}"
    using assms(4) by auto
  then have "⋂ A = ⋂C ∩ ⋂B"
    by (metis Inter_Un_distrib Un_Diff_cancel2 assms(4) sup.orderE) 
  moreover have "⋂B ∈ events" using assms(1) assms(3) assms(2) Inter_event_ss
    by (meson assms(2) assms(4) dual_order.trans finite_subset) 
  ultimately show ?thesis using prob_inter_set_lt_elem
    by (simp add: inf_commute) 
qed

lemma prob_inter_ss_lt_index: 
  assumes "finite A"
  assumes "F ` A ⊆ events"
  assumes "B ≠ {}"
  assumes "B ⊆ A"
  shows "prob (⋂(F ` A)) ≤ prob (⋂(F `B))"
using prob_inter_ss_lt[of "F ` A" "F ` B"] assms by auto

lemma space_compl_double: 
  assumes "S ⊆ events"
  shows "((-) (space M)) ` (((-) (space M)) ` S) = S"
proof (intro subset_antisym subsetI)
  fix x assume "x ∈ (-) (space M) ` (-) (space M) ` S"
  then obtain x' where xeq: "x = space M - x'" and "x' ∈ (-) (space M) ` S" by blast
  then obtain x'' where "x' = space M - x''" and xin: "x'' ∈ S" by blast
  then have "x'' = x" using xeq assms
    by (simp add: Diff_Diff_Int Set.basic_monos(7)) 
  then show "x ∈ S" using xin by simp
next
  fix x assume "x ∈ S"
  then obtain x' where xeq: "x' = space M - x" and "x' ∈ (-) (space M) ` S" by simp
  then have "space M - x' ∈(-) (space M) ` (-) (space M) ` S" by auto
  moreover have "space M - x' = x" using xeq assms
    by (simp add: Diff_Diff_Int ‹x ∈ S› subset_iff)
  ultimately show "x ∈ (-) (space M) ` (-) (space M) ` S" by simp
qed

lemma bij_betw_compl_sets:
  assumes "S ⊆ events"
  assumes "S' = ((-) (space M)) ` S"
  shows "bij_betw ((-) (space M)) S' S"
proof (intro bij_betwI')
  show "⋀x y. x ∈ S' ⟹ y ∈ S' ⟹ (space M - x = space M - y) = (x = y)"
    using assms(2) by blast
next
  show "⋀x. x ∈ S' ⟹ space M - x ∈ S" using space_compl_double assms by auto
next 
  show "⋀y. y ∈ S ⟹ ∃x∈S'. y = space M - x" using space_compl_double assms by auto
qed

lemma bij_betw_compl_sets_rev: 
  assumes "S ⊆ events"
  assumes "S' = ((-) (space M)) ` S"
  shows "bij_betw ((-) (space M)) S S'"
proof (intro bij_betwI')
  show "⋀x y. x ∈ S ⟹ y ∈ S ⟹ (space M - x = space M - y) = (x = y)"
    using assms by (metis Diff_Diff_Int sets.Int_space_eq1 subset_eq) 
next
  show "⋀x. x ∈ S ⟹ space M - x ∈ S'" using space_compl_double assms by auto
next 
  show "⋀y. y ∈ S' ⟹ ∃x∈S. y = space M - x" using space_compl_double assms by auto
qed

lemma prob0_basic_inter:  "A ∈ events ⟹ B ∈ events ⟹ prob A = 0 ⟹ prob (A ∩ B) = 0"
  by (metis Int_lower1 finite_measure_mono measure_le_0_iff) 

lemma prob0_basic_Inter: "A ∈ events ⟹ B ⊆ events ⟹ prob A = 0 ⟹ prob (A ∩ (⋂B)) = 0"
  by (metis Int_lower1 finite_measure_mono measure_le_0_iff) 

lemma prob1_basic_inter: "A ∈ events ⟹ B ∈ events ⟹ prob A = 1 ⟹ prob (A ∩ B) = prob B"
  by (metis inf_commute measure_space_inter prob_space) 

lemma prob1_basic_Inter:
  assumes "A ∈ events" "B ⊆ events"
  assumes "prob A = 1"
  assumes "B ≠ {}"
  assumes "finite B"
  shows "prob (A ∩ (⋂B)) = prob (⋂B)"
proof -
  have "⋂B ∈ events" using Inter_event_ss assms by auto 
  then show ?thesis  using assms prob1_basic_inter by auto
qed

lemma compl_identity:  "A ∈ events ⟹ space M - (space M - A) = A"
  by (simp add: double_diff sets.sets_into_space)

lemma prob_addition_rule: "A ∈ events ⟹ B ∈ events ⟹ 
    prob (A ∪ B) = prob A + prob B - prob (A ∩ B)"
  by (simp add: finite_measure_Diff' finite_measure_Union' inf_commute) 

lemma compl_subset_in_events: "S ⊆ events ⟹ (-) (space M) ` S ⊆ events" 
  by auto

lemma prob_compl_diff_inter:  "A ∈ events ⟹ B ∈ events ⟹ 
    prob (A ∩ (space M - B)) = prob A - prob (A ∩ B)"
  by (simp add: Diff_Int_distrib finite_measure_Diff sets.Int)

lemma bij_betw_prod_prob: "bij_betw f A B ⟹ (∏b∈B. prob b) = (∏a∈A. prob (f a))"
  by (simp add: prod.reindex_bij_betw) 

definition event_compl :: "'a set ⇒ 'a set" where
"event_compl A ≡ space M - A"

lemma compl_Union:  "A ≠ {} ⟹ space M - (⋃A) = (⋂a ∈ A . (space M - a))"
  by (simp)

lemma compl_Union_fn: "A ≠ {} ⟹ space M - (⋃(F ` A)) = (⋂a ∈ A . (space M - F a))"
  by (simp)

end

text ‹Reasoning on the probability of function sets ›

lemma card_PiE_val_ss_eq: 
  assumes "finite A"
  assumes "b ∈ B"
  assumes "d ⊆ A"
  assumes "B ≠ {}"
  assumes "finite B"
  shows "card {f ∈ (A →⇩E B) . (∀ v ∈ d .f v = b)}/card (A →⇩E B)  = 1/((card B) powi (card d))" 
    (is "card {f ∈ ?C . (∀ v ∈ d .f v = b)}/card ?C  = 1/((card B) powi (card d))")
proof - 
  have lt: "card d ≤ card A"
    by (simp add: card_mono assms(1) assms(3)) 
  then have scard: "card {f ∈ ?C . ∀ v ∈ d . f v = b} = (card B) powi ((card A) - card d)"
    using assms card_PiE_filter_range_set_const[of b B d A] assms
    by (simp flip: of_nat_diff)
  have Ccard: "card ?C = (card B) powi (card A)" using card_funcsetE assms(2) assms(1) by auto
  have bgt: "card B ≠ 0" using assms(5) assms(4) by auto
  have "card {f ∈ ?C . ∀ v ∈ d . f v = b}/ (card ?C) = 
      ((card B) powi ((card A) - card d))/((card B) powi (card A))" 
    using Ccard scard by simp
  also have "... = (card B) powi (int (card A - card d) - int (card A))" 
    using bgt by (simp add: power_int_diff)
  also have "... = inverse ((card B) powi (card d))" 
    using power_int_minus[of "card B" "(int (card d))"] by (simp add: lt)
  finally show ?thesis by (simp add: inverse_eq_divide)  
qed  

lemma card_PiE_val_indiv_eq: 
  assumes "finite A"
  assumes "b ∈ B"
  assumes "d ∈ A"
  assumes "B ≠ {}"
  assumes "finite B"
  shows "card {f ∈ (A →⇩E B) . f d = b}/card (A →⇩E B)  = 1/(card B)" 
    (is "card {f ∈ ?C .f d = b}/card ?C  = 1/(card B)")
proof - 
  have "{d} ⊆ A" using assms(3) by simp
  moreover have "⋀ f . f ∈ ?C ⟹ f d = b ⟷ (∀ d' ∈ {d}. f d' = b)" by auto
  ultimately have "card {f ∈ ?C .f d = b}/card ?C = 1/((card B) powi (card {d}))"
    using card_PiE_val_ss_eq[of A b B "{d}"] assms by auto
  also have "... = 1/((card B) powi 1)" by auto
  finally show ?thesis by simp
qed  

lemma prob_uniform_ex_fun_space: 
  assumes "finite A"
  assumes "b ∈ B"
  assumes "d ⊆ A"
  assumes "B ≠ {}"
  assumes "A ≠ {}"
  assumes "finite B"
  shows "prob_space.prob (uniform_count_measure (A →⇩E B)) {f ∈ (A →⇩E B) . (∀ v ∈ d .f v = b)} = 
    1/((card B) powi (card d))"
proof - 
  let ?C = "(A →⇩E B)"
  let ?M = "uniform_count_measure ?C"
  have finC: "finite ?C" using assms(2) assms(6) assms(1)
    by (simp add: finite_PiE) 
  moreover have "?C ≠ {}" using assms(4) assms(1)
    by (simp add: PiE_eq_empty_iff) 
  ultimately interpret P: prob_space ?M
    using assms(3)  by (simp add: prob_space_uniform_count_measure)
  have "P.prob {f ∈ ?C . ∀ v ∈ d . f v = b} = card {f ∈ ?C . ∀ v ∈ d . f v = b}/ (card ?C)"
    using measure_uniform_count_measure[of ?C "{f ∈ ?C . ∀ v ∈ d . f v = b} "] finC assms(3) 
    by fastforce  
  then show ?thesis using card_PiE_val_ss_eq assms by (simp)  
qed

proposition integrable_uniform_count_measure_finite:
  fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}"
  shows "finite A ⟹ integrable (uniform_count_measure A) g"
  unfolding uniform_count_measure_def
  using integrable_point_measure_finite by fastforce

end