Theory Lovasz_Local.Cond_Prob_Extensions

(* Theory: Cond_Prob_Extensions
   Author: Chelsea Edmonds *)

section ‹Conditional Probability Library Extensions ›

theory Cond_Prob_Extensions 
  imports 
    Prob_Events_Extras  
    Design_Theory.Multisets_Extras
begin

subsection ‹Miscellaneous Set and List Lemmas ›

lemma nth_image_tl: 
  assumes "xs ≠ []"
  shows "nth xs ` {1..<length xs} = set(tl xs)"
proof -
  have "set (tl xs) = {(tl xs)!i | i. i < length (tl xs)}"
    using set_conv_nth by metis 
  then have "set (tl xs) = {xs! (Suc i) | i. i  < length xs - 1}"
    using nth_tl by fastforce 
  then have "set (tl xs) = {xs ! j | j. j > 0 ∧ j < length xs}"
    by (smt (verit, best) Collect_cong Suc_diff_1 Suc_less_eq assms length_greater_0_conv zero_less_Suc)
  thus ?thesis by auto
qed

lemma exists_list_card: 
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S"
  by (metis assms distinct_card finite_distinct_list)

lemma bij_betw_inter_empty: (* this is the only lemma needing the Multisets_Extras theory *)
  assumes "bij_betw f A B"
  assumes "A' ⊆ A"
  assumes "A'' ⊆ A"
  assumes "A' ∩ A'' = {}"
  shows "f ` A' ∩ f ` A'' = {}"
  by (metis assms(1) assms(2) assms(3) assms(4) bij_betw_inter_subsets image_empty)


lemma bij_betw_image_comp_eq: 
  assumes "bij_betw g T S"
  shows "(F ∘ g) ` T = F ` S"
  using assms bij_betw_imp_surj_on by (metis image_comp) 

lemma prod_card_image_set_eq: 
  assumes "bij_betw f {0..<card S} S"
  assumes "finite S"
  shows "(∏i ∈ {n..<(card S)} . g (f i)) = (∏i ∈ f ` {n..<card S} . g i)"
proof (cases "n ≥ card S")
  case True
  then show ?thesis by simp
next
  case False
  then show ?thesis using assms 
  proof (induct "card S" arbitrary: S)
    case 0
    then show ?case by auto
  next
    case (Suc x)
    then have nlt: "n < Suc x" by simp
    then have split: "{n..<Suc x} = {n..<x} ∪ {x}" by auto
    then have "f ` {n..<Suc x} = f ` ({n..< x} ∪ {x})" by simp
    then have fsplit: "f ` {n..<Suc x} = f ` {n..< x} ∪ {f x}"
      by simp 
    have "{n..<x} ⊆ {0..<card S}"
      using Suc(2)  by auto 
    moreover have "{x} ⊆ {0..<card S}" using Suc(2) by auto
    moreover have "{n..< x} ∩ {x} = {}" by auto
    ultimately have finter: "f ` {n..< x} ∩ {f x} = {}" using Suc.prems(2) Suc.prems(1) 
       bij_betw_inter_empty[of f "{0..<card S}" S "{n..< x}" "{x}"] by auto
    have "(∏i = n..<Suc x. g (f i)) = (∏i = n..<x. g (f i)) * g (f( x))" using nlt by simp
    moreover have "(∏x∈f ` {n..<Suc x}. g x) = (∏i∈f ` {n..< x}. g i) * g (f x)" using finter fsplit
      by (simp add: Groups.mult_ac(2))
    moreover have "(∏i∈f ` {n..< x}. g i) = (∏i = n..<x. g (f i))"
    proof -
      let ?S' = "f ` {0..<x}"
      have "{0..<x} ⊆ {0..<card S}" using Suc(2) by auto
      then have bij: "bij_betw f {0..<x} ?S'" using Suc.prems(2)
        using bij_betw_subset by blast 
      moreover have "card ?S' = x" using bij_betw_same_card[of f "{0..<x}" ?S'] bij by auto
      moreover have "finite ?S'" using finite_subset by auto 
      ultimately show ?thesis
        by (metis bij_betw_subset ivl_subset less_eq_nat.simps(1) order_refl prod.reindex_bij_betw)  
    qed 
    ultimately show ?case using Suc(2) by auto
  qed
qed

lemma set_take_distinct_elem_not: 
  assumes "distinct xs"
  assumes "i < length xs"
  shows "xs ! i ∉ set (take i xs)"
  by (metis assms(1) assms(2) distinct_take id_take_nth_drop not_distinct_conv_prefix)

subsection ‹ Conditional Probability Basics ›
context prob_space
begin

text ‹Abbreviation to mirror mathematical notations ›

abbreviation cond_prob_ev :: "'a set ⇒ 'a set ⇒ real" (‹𝒫'(_ | _')›)  where 
"𝒫(B | A) ≡  𝒫(x in M. (x ∈ B) ¦ (x ∈ A))"

lemma cond_prob_inter: "𝒫(B | A) = 𝒫(ω in M. (ω ∈ B ∩ A)) / 𝒫(ω in M. (ω ∈ A))"
  using cond_prob_def by auto

lemma cond_prob_ev_def: 
  assumes "A ∈ events" "B ∈ events"
  shows "𝒫(B | A) = prob (A ∩ B) / prob A"
proof -
  have a: "𝒫(B | A) = 𝒫(ω in M. (ω ∈ B ∩ A)) / 𝒫(ω in M. (ω ∈ A))"
    using cond_prob_inter by auto
  also have "... = prob {w ∈ space M . w ∈ B ∩ A} / prob {w ∈ space M . w ∈ A}"
    by auto
  finally show ?thesis using assms
    by (simp add: Collect_conj_eq a inf_commute)
qed

lemma measurable_in_ev:
  assumes "A ∈ events"
  shows "Measurable.pred M (λ x . x ∈ A)"
  using assms by auto

lemma measure_uniform_measure_eq_cond_prob_ev:
  assumes "A ∈ events" "B ∈ events"
  shows "𝒫(A | B) =𝒫(x in uniform_measure M {x∈space M. x ∈ B}. x ∈ A)"
  using assms measurable_in_ev measure_uniform_measure_eq_cond_prob by auto

lemma measure_uniform_measure_eq_cond_prob_ev2:
  assumes "A ∈ events" "B ∈ events"
  shows "𝒫(A | B) = measure (uniform_measure M {x∈space M. x ∈ B}) A"
  using measure_uniform_measure_eq_cond_prob_ev assms
  by (metis Int_def sets.Int_space_eq1 space_uniform_measure) 

lemma measure_uniform_measure_eq_cond_prob_ev3:
  assumes "A ∈ events" "B ∈ events"
  shows "𝒫(A | B) = measure (uniform_measure M B) A"
  using measure_uniform_measure_eq_cond_prob_ev assms  Int_def sets.Int_space_eq1 space_uniform_measure
  by metis (* Slow *)

lemma prob_space_cond_prob_uniform:
  assumes "prob ({x∈space M. Q x}) > 0"
  shows "prob_space (uniform_measure M {x∈space M. Q x})"
  using assms by (intro prob_space_uniform_measure) (simp_all add: emeasure_eq_measure)

lemma prob_space_cond_prob_event:
  assumes "prob B > 0"
  shows "prob_space (uniform_measure M B)"
  using assms by (intro prob_space_uniform_measure) (simp_all add: emeasure_eq_measure)

text‹Note this case shouldn't be used. Conditional probability should have > 0 assumption›
lemma cond_prob_empty: "𝒫(B | {}) = 0" 
  using cond_prob_inter[of B "{}"] by auto

lemma cond_prob_space:  "𝒫(A | space M) = 𝒫(w in M . w ∈ A)"
proof -
  have p1: "prob {ω ∈ space M. ω ∈ space M} = 1"
    by (simp add: prob_space) 
  have "⋀ w. w ∈ space M ⟹ w ∈ A ∩ (space M) ⟷ w ∈ A" by auto
  then have "prob {ω ∈ space M. ω ∈ A ∩ space M} = 𝒫(w in M . w ∈ A)"
    by meson 
  then show ?thesis using cond_prob_inter[of  A "space M"] p1 by auto
qed

lemma cond_prob_space_ev: assumes "A ∈ events" shows "𝒫(A | space M) = prob A"
  using cond_prob_space assms
  by (metis Int_commute Int_def measure_space_inter sets.top) 

lemma cond_prob_UNIV: "𝒫(A | UNIV) = 𝒫(w in M . w ∈ A)"
proof -
  have p1: "prob {ω ∈ space M. ω ∈ UNIV} = 1"
    by (simp add: prob_space) 
  have "⋀ w. w ∈ space M ⟹ w ∈ A ∩ UNIV ⟷ w ∈ A" by auto
  then have "prob {ω ∈ space M. ω ∈ A ∩ UNIV} = 𝒫(w in M . w ∈ A)"
    by meson 
  then show ?thesis using cond_prob_inter[of A UNIV] p1 by auto
qed

lemma cond_prob_UNIV_ev: "A ∈ events ⟹ 𝒫(A | UNIV) = prob A"
  using cond_prob_UNIV 
  by (metis Int_commute Int_def measure_space_inter sets.top)

lemma cond_prob_neg: 
  assumes "A ∈ events" "B ∈ events"
  assumes "prob A >0"
  shows "𝒫((space M - B) | A) = 1 - 𝒫(B | A)"
proof -
  have negB: "space M - B ∈ events" using assms by auto 
  have "prob ((space M - B) ∩ A) = prob A - prob (B ∩ A)"
    by (simp add: Diff_Int_distrib2 assms(1) assms(2) finite_measure_Diff sets.Int)
  then have "𝒫((space M - B) | A) = (prob A - prob (B ∩ A))/prob A" 
    using cond_prob_ev_def[of A "space M - B"] assms negB by (simp add: Int_commute) 
  also have "... = ((prob A)/prob A) - ((prob (B ∩ A))/prob A)" by (simp add: field_simps)
  also have "... = 1 - ((prob (B ∩ A))/prob A)" using assms(3) by (simp add: field_simps)
  finally show "𝒫((space M - B) | A) = 1 - 𝒫(B | A)" using cond_prob_ev_def[of A B] assms
    by (simp add: inf_commute) 
qed

subsection ‹Bayes Theorem ›


lemma prob_intersect_A: 
  assumes "A ∈ events" "B ∈ events"
  shows "prob (A ∩ B) = prob A * 𝒫(B | A)"
  using cond_prob_ev_def assms apply simp
  by (metis Int_lower1 finite_measure_mono measure_le_0_iff)

lemma prob_intersect_B: 
  assumes "A ∈ events" "B ∈ events"
  shows "prob (A ∩ B) = prob B * 𝒫(A | B)"
  using cond_prob_ev_def assms 
  by (simp_all add: inf_commute)(metis Int_lower2 finite_measure_mono measure_le_0_iff)

theorem Bayes_theorem: 
  assumes "A ∈ events" "B ∈ events"
  shows "prob B * 𝒫(A | B) = prob A * 𝒫(B |A)" 
  using prob_intersect_A prob_intersect_B assms by simp

corollary Bayes_theorem_div: 
  assumes "A ∈ events" "B ∈ events"
  shows "𝒫(A | B) = (prob A * 𝒫(B |A))/(prob B)"
  using assms Bayes_theorem
  by (metis cond_prob_ev_def prob_intersect_A) 

lemma cond_prob_dual_intersect: 
  assumes "A ∈ events" "B ∈ events" "C ∈ events"
  assumes "prob C ≠ 0"
  shows "𝒫(A | (B ∩ C)) = 𝒫(A ∩ B | C)/ 𝒫(B | C)" (is "?LHS = ?RHS")
proof - 
  have "B ∩ C ∈ events" using assms by auto
  then have lhs: "?LHS = prob (A ∩ B ∩ C)/prob (B ∩ C)" 
    using assms cond_prob_ev_def[of "B ∩ C" "A"] inf_commute inf_left_commute  by (metis)
  have "A ∩ B ∈ events" using assms by auto
  then have "𝒫(A ∩ B | C) = prob (A ∩ B ∩ C) / prob C" 
    using assms cond_prob_ev_def[of "C" "A ∩ B"] inf_commute by (metis)
  moreover have "𝒫(B | C) = prob (B ∩ C)/prob C" using cond_prob_ev_def[of "C" "B"] assms inf_commute by metis
  ultimately have "?RHS = (prob (A ∩ B ∩ C) / prob C)/( prob (B ∩ C)/prob C)"
    by simp
  also have "... = (prob (A ∩ B ∩ C) / prob C)*( prob (C)/prob (B ∩ C))" by simp
  also have "... = prob (A ∩ B ∩ C)/prob (B∩ C)" using assms(4) by simp
  finally show ?thesis using lhs by simp
qed


lemma cond_prob_ev_double: 
  assumes "A ∈ events" "B ∈ events" "C ∈ events"
  assumes "prob C > 0"
  shows "𝒫(x in (uniform_measure M C). (x ∈ A) ¦ (x ∈ B)) =  𝒫(A | (B ∩ C))"
proof - 
  let ?M = "uniform_measure M C"
  interpret cps: prob_space "?M" using assms(4) prob_space_cond_prob_event by auto
  have probne: "prob C ≠ 0" using assms(4) by auto
  have ev: "cps.events = events" using sets_uniform_measure by auto
  have iev: "A ∩ B ∈ events" using assms(1) assms(2) by simp
  have 0: "𝒫(x in (uniform_measure M C). (x ∈ A) ¦ (x ∈ B)) = cps.cond_prob_ev A B" by simp
  also have 1: "... = (measure ?M (A ∩ B))/(measure ?M B)" using cond_prob_ev_def assms(1) assms(2) ev
    by (metis Int_commute cps.cond_prob_ev_def)
  also have 2: "... = 𝒫((A ∩ B) | C)/(measure ?M B)" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "A ∩ B" "C"] assms(3) iev by auto
  also have 3: "... = 𝒫((A ∩ B) | C)/ 𝒫(B | C)" using measure_uniform_measure_eq_cond_prob_ev3[of "B" "C"] assms(3) assms(2) by auto
  also have 4: "... = 𝒫(A | (B ∩ C))" 
    using cond_prob_dual_intersect[of "A" "B" "C"] assms(1) assms(2) assms(3) probne by presburger 
  finally show ?thesis using 1 2 3 4 by presburger
qed

lemma cond_prob_inter_set_lt: 
  assumes "A ∈ events" "B ∈ events" "AS ⊆ events"
  assumes "finite AS"
  shows "𝒫((A ∩ (⋂AS)) | B) ≤ 𝒫(A|B)" (is "?LHS ≤ ?RHS")
using measure_uniform_measure_eq_cond_prob_ev finite_measure_mono 
proof (cases "AS = {}")
  case True
  then have "(A ∩ (⋂AS)) = A" by simp
  then show ?thesis by simp
next
  case False
  then have "(⋂AS) ∈ events" using assms(3) assms(4) Inter_event_ss by simp
  then have "(A ∩ (⋂AS)) ∈ events" using assms by simp
  then have "?LHS = prob (A ∩ (⋂AS) ∩ B)/prob B" 
    using assms cond_prob_ev_def[of "B" "(A ∩ (⋂AS))"] inf_commute by metis
  moreover have "prob (A ∩ (⋂AS) ∩ B) ≤ prob (A ∩ B)" using finite_measure_mono
    assms(1) inf_commute inf_left_commute by (metis assms(2) inf_sup_ord(1) sets.Int) 
  ultimately show ?thesis using cond_prob_ev_def[of "B" "A"]
    by (simp add: assms(1) assms(2) divide_right_mono inf_commute) 
qed

subsection ‹Conditional Probability Multiplication Rule ›
text ‹Many list and indexed variations of this lemma ›

lemma prob_cond_Inter_List:  
  assumes "xs ≠ []"
  assumes "⋀ A. A ∈ set xs ⟹ A ∈ events"
  shows "prob (⋂(set xs)) = prob (hd xs) * (∏i = 1..<(length xs) . 
    𝒫((xs ! i) | (⋂(set (take i xs )))))"
  using assms(1) assms(2) 
proof (induct xs rule: rev_nonempty_induct)
  case (single x)
  then show ?case by auto
next
  case (snoc x xs)
  have "xs ≠ []"
    by (simp add: snoc.hyps(1)) 
  then have inev: "(⋂(set xs)) ∈ events" using events_inter
    by (simp add: snoc.prems) 
  have len: "(length (xs @ [x])) = length xs + 1" by auto
  have last_p: "𝒫(x | (⋂(set xs))) = 
    𝒫((xs @ [x]) ! length xs | ⋂ (set (take (length xs) (xs @ [x]))))"
    by auto
  have "prob (⋂ (set (xs @ [x]))) = prob (x ∩ (⋂(set xs)))"
    by auto
  also have "... = prob (⋂(set xs)) * 𝒫(x | (⋂(set xs)))" 
    using prob_intersect_B snoc.prems inev by simp 
  also have "... = prob (hd xs) * (∏i = 1..<length xs. 𝒫(xs ! i | ⋂ (set (take i xs)))) * 
      𝒫(x | (⋂(set xs)))"
    using snoc.hyps snoc.prems by auto
  finally have "prob (⋂ (set (xs @ [x]))) = prob (hd (xs @[x])) * 
      (∏i = 1..<length xs. 𝒫((xs @ [x]) ! i | ⋂ (set (take i (xs @ [x]))))) *  𝒫(x | (⋂(set xs)))" 
    using nth_append[of xs "[x]"] nth_take by (simp add: snoc.hyps(1)) 
  then show ?case using last_p by auto
qed

lemma prob_cond_Inter_index:  
  fixes n :: nat
  assumes "n > 0"
  assumes "F ` {0..<n} ⊆ events"
  shows "prob (⋂ (F `{0..<n} )) = prob (F 0) * (∏i ∈ {1..<n} . 
    𝒫(F i | (⋂ (F`{0..<i}))))"
proof -
  define xs where "xs ≡ map F [0..<n]"
  have "prob (⋂(set xs)) = prob (hd xs) * (∏i = 1..<(length xs) . 
    𝒫((xs ! i) | (⋂(set (take i xs )))))" using xs_def assms prob_cond_Inter_List[of xs] by auto
  then have "prob (⋂(set xs)) = prob (hd xs) * (∏i ∈ {1..<n} . 𝒫((xs ! i) | (⋂(set (take i xs )))))" 
    using xs_def by auto
  moreover have "hd xs = F 0" 
    unfolding xs_def by (simp add: assms(1) hd_map) 
  moreover have "⋀ i. i ∈ {1..<n} ⟹ F ` {0..<i} = set (take i xs )"
    by (metis atLeastLessThan_iff atLeastLessThan_upt image_set less_or_eq_imp_le plus_nat.add_0 
        take_map take_upt xs_def)
  ultimately show ?thesis using xs_def by auto
qed

lemma prob_cond_Inter_index_compl: 
  fixes n :: nat
  assumes "n > 0"
  assumes "F ` {0..<n} ⊆ events"
  shows "prob (⋂ x ∈ {0..<n} . space M - F x) = prob (space M - F 0) * (∏i ∈ {1..<n} . 
    𝒫(space M - F i | (⋂ j∈ {0..<i}. space M - F j)))"
proof -
  define G where "G ≡ λ i. space M - F i"
  then have "G ` {0..<n} ⊆ events" using assms(2) by auto
  then show ?thesis using prob_cond_Inter_index[of n G] G_def
    using assms(1) by blast  
qed


lemma prob_cond_Inter_take_cond:
  assumes "xs ≠ []"
  assumes "set xs ⊆ events"
  assumes "S ⊆ events"
  assumes "S ≠ {}"
  assumes "finite S"
  assumes "prob (⋂S) > 0"
  shows "𝒫((⋂(set xs)) | (⋂ S)) = (∏i = 0..<(length xs) .  𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S))))"
proof -
  define M' where "M' = uniform_measure M (⋂S)"
  interpret cps: prob_space M' using prob_space_cond_prob_event M'_def assms(6) by auto
  have len: "length xs > 0" using assms(1) by simp
  have cps_ev: "cps.events = events" using sets_uniform_measure M'_def by auto
  have sevents: "⋂S ∈ events" using assms(3) assms(4) Inter_event_ss assms(5) by auto
  have fin: "finite (set xs)" by auto
  then have xevents: "⋂(set xs) ∈ events" using assms(1) assms(2) Inter_event_ss by blast
  then have peq: "𝒫((⋂(set xs)) | (⋂ S)) = cps.prob (⋂ (set xs))" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "⋂(set xs)" "⋂S"] sevents M'_def
    by blast
  then have "cps.prob (⋂ (set xs)) = cps.prob (hd xs) * (∏i = 1..<(length xs) . 
    cps.cond_prob_ev (xs ! i) (⋂(set (take i xs ))))" using assms cps.prob_cond_Inter_List cps_ev 
    by blast
  moreover have "cps.prob (hd xs) = 𝒫((xs ! 0) | (⋂(set (take 0 xs ) ∪ S)))"
  proof -
    have ev: "hd xs ∈ events" using assms(2) len by auto
    then have "cps.prob (hd xs) = 𝒫(hd xs | ⋂S)" 
      using ev sevents measure_uniform_measure_eq_cond_prob_ev3[of "hd xs" "⋂S"] M'_def by presburger
    then show ?thesis using len by (simp add: hd_conv_nth)
  qed
  moreover have "⋀i. i > 0 ⟹ i < length xs ⟹ 
    cps.cond_prob_ev (xs ! i) (⋂(set (take i xs ))) = 𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S)))"
  proof -
    fix i assume igt: "i > 0" and ilt: "i <length xs"
    then have "set (take i xs) ⊆ events" using assms(2)
      by (meson set_take_subset subset_trans) 
    moreover have "set (take i xs) ≠ {}" using len igt ilt by auto
    ultimately have "(⋂(set (take i xs ))) ∈ events"
      using Inter_event_ss fin by auto
    moreover have "xs ! i ∈ events" using assms(2)
      using nth_mem subset_iff igt ilt by blast
    moreover have "(⋂(set (take i xs ) ∪ S)) = (⋂(set (take i xs ))) ∩ (⋂S)"
      by (simp add: Inf_union_distrib) 
    ultimately show "cps.cond_prob_ev (xs ! i) (⋂(set (take i xs ))) = 𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S)))"
      using sevents cond_prob_ev_double[of "xs ! i" "(⋂(set (take i xs )))" "⋂S"] assms(6) M'_def by presburger 
  qed
  ultimately have eq: "cps.prob (⋂ (set xs)) = 𝒫((xs ! 0) | (⋂(set (take 0 xs ) ∪ S))) * (∏i ∈ {1..<(length xs)} . 
    𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S))))" by simp
  moreover have "{1..<length xs} = {0..<length xs} - {0}"
    by (simp add: atLeast1_lessThan_eq_remove0 lessThan_atLeast0)
  moreover have "finite {0..<length xs}" by auto
  moreover have "0 ∈ {0..<length xs}"by (simp add: assms(1)) 
  ultimately have "𝒫((xs ! 0) | (⋂(set (take 0 xs ) ∪ S))) * (∏i ∈ {1..<(length xs)} . 
    𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S)))) = (∏i ∈ {0..<(length xs)} . 
    𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S))))" using prod.remove[of "{0..<length xs}" "0" "λ i. 𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S)))"]
    by presburger
  then have "cps.prob (⋂ (set xs)) = (∏i ∈ {0..<(length xs)} . 
    𝒫((xs ! i) | (⋂(set (take i xs ) ∪ S))))" using eq by simp
  then show ?thesis using peq by auto
qed

lemma prob_cond_Inter_index_cond_set:
  fixes n :: nat
  assumes "n > 0"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` {0..<n} ⊆ events"
  assumes "prob (⋂E) > 0"
  shows "𝒫((⋂(F ` {0..<n})) | (⋂E)) = (∏i ∈ {0..<n}.  𝒫(F i | (⋂((F ` {0..<i}) ∪ E))))"
proof -
  define M' where "M' = uniform_measure M (⋂E)"
  interpret cps: prob_space M' using prob_space_cond_prob_event M'_def assms(6) by auto
  have cps_ev: "cps.events = events" using sets_uniform_measure M'_def by auto
  have sevents: "(⋂(E)) ∈ events" using assms(6) assms(2) assms(3) assms(4) Inter_event_ss by auto
  have fin: "finite (F ` {0..<n})" by auto
  then have xevents: "⋂(F ` {0..<n}) ∈ events" using assms Inter_event_ss by auto
  then have peq: "𝒫((⋂(F ` {0..<n})) | (⋂ E)) = cps.prob (⋂ (F ` {0..<n}))" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "⋂(F ` {0..<n})" "⋂E"] sevents M'_def
    by blast
  moreover have "F `{0..<n} ⊆ cps.events" using cps_ev assms(5) by force 
  ultimately have "cps.prob (⋂ (F ` {0..<n})) = cps.prob (F 0) * (∏i = 1..<n . 
    cps.cond_prob_ev (F i) (⋂(F ` {0..<i})))" 
    using assms(1) cps.prob_cond_Inter_index[of n F] by blast
  moreover have "cps.prob (F 0) = 𝒫((F 0) | (⋂E))"
  proof -
    have ev: "F 0 ∈ events" using assms(1) assms(5) by auto
    then show ?thesis 
      using ev sevents measure_uniform_measure_eq_cond_prob_ev3[of "F 0" "⋂E"] M'_def by presburger
  qed
  moreover have "⋀i. i > 0 ⟹ i < n ⟹ 
    cps.cond_prob_ev (F i) (⋂(F ` {0..<i})) = 𝒫((F i) | (⋂((F ` {0..<i}) ∪ E)))"
  proof -
    fix i assume igt: "i > 0" and ilt: "i <n"
    then have "(⋂(F ` {0..<i})) ∈ events"
      using assms subset_trans igt Inter_event_ss fin by auto
    moreover have "F i ∈ events" using assms 
      using subset_iff igt ilt by simp
    moreover have "(⋂((F ` {0..<i}) ∪ (E))) = (⋂((F ` {0..<i}))) ∩ (⋂(E))"
      by (simp add: Inf_union_distrib) 
    ultimately show "cps.cond_prob_ev (F i) (⋂(F ` {0..<i})) = 𝒫((F i) | (⋂((F ` {0..<i}) ∪ E)))"
      using sevents cond_prob_ev_double[of "F i" "(⋂((F ` {0..<i})))" "⋂E"] assms M'_def by presburger 
  qed
  ultimately have eq: "cps.prob (⋂ (F ` {0..<n})) = 𝒫((F 0) | (⋂E)) * (∏i ∈ {1..<n} . 
    𝒫((F i) | (⋂((F ` {0..<i}) ∪ E))))" by simp
  moreover have "{1..<n} = {0..<n} - {0}"
    by (simp add: atLeast1_lessThan_eq_remove0 lessThan_atLeast0)
  ultimately have "𝒫((F 0) | (⋂E)) * (∏i ∈ {1..<n} .  𝒫((F i) | (⋂((F ` {0..<i}) ∪ E)))) = 
      (∏i ∈ {0..<n} . 𝒫((F i) | (⋂((F ` {0..<i}) ∪ E))))" using assms(1) 
    prod.remove[of "{0..<n}" "0" "λ i. 𝒫((F i) | (⋂((F `{0..<i}) ∪ E)))"] by fastforce
  then show ?thesis using peq eq by auto
qed

lemma prob_cond_Inter_index_cond_compl_set:
  fixes n :: nat
  assumes "n > 0"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` {0..<n} ⊆ events"
  assumes "prob (⋂E) > 0"
  shows "𝒫((⋂((-) (space M) ` F ` {0..<n})) | (⋂E)) = 
    (∏i = 0..<n .  𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ E))))"
proof -
  define G where "G ≡ λ i. (space M - F i)"
  then have "G ` {0..<n} ⊆ events" using assms(5) by auto
  then have "𝒫((⋂(G ` {0..<n})) | (⋂E)) = (∏i ∈ {0..<n}.  𝒫(G i | (⋂((G ` {0..<i}) ∪ E))))"
    using prob_cond_Inter_index_cond_set[of n E G] assms by blast
  moreover have "((-) (space M) ` F ` {0..<n}) = (G ` {0..<n})"  unfolding G_def by auto
  moreover have "⋀ i. i ∈ {0..<n} ⟹ 𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ E))) = 
    𝒫(G i | (⋂((G ` {0..<i}) ∪ E)))" 
  proof -
    fix i assume iin: "i ∈ {0..<n}"
    have "(-) (space M) ` F ` {0..<i} =  G ` {0..<i}" unfolding G_def using iin by auto
    then show "𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ E))) = 
    𝒫(G i | (⋂((G ` {0..<i}) ∪ E)))" unfolding G_def by auto
  qed
  ultimately show ?thesis  by auto
qed

lemma prob_cond_Inter_index_cond:
  fixes n :: nat
  assumes "n > 0"
  assumes "n < m"
  assumes "F ` {0..<m} ⊆ events"
  assumes "prob (⋂j ∈ {n..<m}. F j) > 0"
  shows "𝒫((⋂(F ` {0..<n})) | (⋂j ∈{n..<m} . F j)) = (∏i ∈ {0..<n}.  𝒫(F i | (⋂((F ` {0..<i}) ∪ (F ` {n..<m})))))"
proof -
  let ?E = "F ` {n..<m}"
  have "F ` {0..<n} ⊆ events" using assms(2) assms(3) by auto
  moreover have "?E ⊆ events" using assms(2) assms(3) by auto
  moreover have "prob(⋂?E) > 0" using assms(4) by simp
  moreover have "?E ≠ {}" using assms(2) by simp
  ultimately show ?thesis using prob_cond_Inter_index_cond_set[of n "?E" F] assms(1) by blast
qed


lemma prob_cond_Inter_index_cond_compl:
  fixes n :: nat
  assumes "n > 0"
  assumes "n < m"
  assumes "F ` {0..<m} ⊆ events"
  assumes "prob (⋂j ∈ {n..<m}. F j) > 0"
  shows "𝒫((⋂((-) (space M) ` F ` {0..<n})) | (⋂( F ` {n..<m}))) = 
    (∏i = 0..<n .  𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ (F ` {n..<m})))))"
proof -
  define G where "G ≡ λ i. if (i < n) then (space M - F i) else F i"
  then have "G ` {0..<m} ⊆ events" using assms(3) by auto
  moreover have "prob (⋂j ∈ {n..<m}. G j) > 0" using G_def assms(4) by simp
  ultimately have "𝒫((⋂(G ` {0..<n})) | (⋂( G ` {n..<m}))) = (∏i ∈ {0..<n}.  𝒫(G i | (⋂((G ` {0..<i}) ∪ (G ` {n..<m})))))"
    using prob_cond_Inter_index_cond[of n m G] assms(1) assms(2) by blast
  moreover have "((-) (space M) ` F ` {0..<n}) = (G ` {0..<n})"  unfolding G_def by auto
  moreover have meq: "( F ` {n..<m}) = ( G ` {n..<m})" unfolding G_def by auto
  moreover have "⋀ i. i ∈ {0..<n} ⟹ 𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ (F ` {n..<m})))) = 
    𝒫(G i | (⋂((G ` {0..<i}) ∪ (G ` {n..<m}))))" 
  proof -
    fix i assume iin: "i ∈ {0..<n}"
    then have "(space M - F i) = G i" unfolding G_def by auto
    moreover have "(-) (space M) ` F ` {0..<i} =  G ` {0..<i}" unfolding G_def using iin by auto
    ultimately show "𝒫((space M - F i) | (⋂((-) (space M) ` F ` {0..<i} ∪ (F ` {n..<m})))) = 
    𝒫(G i | (⋂((G ` {0..<i}) ∪ (G ` {n..<m}))))" using meq by auto
  qed
  ultimately show ?thesis  by auto
qed

lemma prob_cond_Inter_take_cond_neg:
  assumes "xs ≠ []"
  assumes "set xs ⊆ events"
  assumes "S ⊆ events"
  assumes "S ≠ {}"
  assumes "finite S"
  assumes "prob (⋂S) > 0"
  shows "𝒫((⋂((-) (space M) ` (set xs))) | (⋂ S)) = 
    (∏i = 0..<(length xs) .  𝒫((space M - xs ! i) | (⋂((-) (space M) ` (set (take i xs )) ∪ S))))"
proof -
  define ys where "ys = map ((-) (space M)) xs"
  have set: "((-) (space M) ` (set xs)) = set (ys)"
    using ys_def by simp
  then have "set ys ⊆ events"
    by (metis assms(2) image_subset_iff sets.compl_sets subsetD)
  moreover have "ys ≠ []" using ys_def assms(1) by simp
  ultimately have "𝒫(⋂(set ys) | (⋂S)) = 
      (∏i = 0..<(length ys) .  𝒫((ys ! i) | (⋂(set (take i ys ) ∪ S))))"
    using prob_cond_Inter_take_cond assms by auto
  moreover have len: "length ys = length xs" using ys_def by auto
  moreover have "⋀i. i < length xs ⟹ ys ! i = space M - xs ! i" using ys_def nth_map len by auto
  moreover have "⋀i. i < length xs ⟹ set (take i ys) = (-) (space M) ` set (take i xs)" 
    using ys_def take_map len by (metis set_map) 
  ultimately show ?thesis using set by auto
qed

lemma prob_cond_Inter_List_Index:  
  assumes "xs ≠ []"
  assumes "set xs ⊆ events"
  shows "prob (⋂(set xs)) = prob (hd xs) * (∏i = 1..<(length xs) . 
    𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)))"
proof -
  have "⋀ i. i < length xs ⟹ set (take i xs) = ((!) xs ` {0..<i})"
    by (metis nat_less_le nth_image)
  thus ?thesis using prob_cond_Inter_List[of xs] assms by auto
qed

lemma obtains_prob_cond_Inter_index: (* added obtains *)
  assumes " S ≠ {}"
  assumes "S ⊆ events"
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S" and 
    "prob (⋂S) = prob (hd xs) * (∏i = 1..<(length xs) . 𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)))"
  using assms prob_cond_Inter_List_Index exists_list_card 
  by (metis (no_types, lifting) set_empty2) 

lemma obtain_list_index: 
  assumes "bij_betw g {0..<card S} S"
  assumes "finite S"
  obtains xs where "set xs = S" and "⋀ i . i ∈ {0..<card S} ⟹ g i = xs ! i" and "distinct xs"
proof -
  let ?xs = "map g [0..<card S]" 
  have seq: "g ` {0..<card S} = S" using assms(1)
    by (simp add: bij_betw_imp_surj_on) 
  then have set_eq: "set ?xs = S"
    by simp 
  moreover have "⋀ i . i ∈ {0..<card S} ⟹ g i = ?xs ! i" 
    by auto
  moreover have leneq: "length ?xs = card S" using seq by auto
  moreover have "distinct ?xs" using set_eq leneq
    by (simp add: card_distinct) 
  ultimately show ?thesis
    using that by blast 
qed

lemma prob_cond_inter_fn:  
  assumes "bij_betw g {0..<card S} S"
  assumes "finite S"
  assumes "S ≠ {}"
  assumes "S ⊆ events"
  shows "prob (⋂S) = prob (g 0) * (∏i ∈ {1..<(card S)} . 𝒫(g i | (⋂(g ` {0..<i}))))"
proof -
  obtain xs where seq: "set xs = S" and geq: "⋀ i . i ∈ {0..<card S} ⟹ g i = xs ! i" and "distinct xs"
    using obtain_list_index assms by auto
  then have len:  "length xs = card S" by (metis distinct_card) 
  then have "prob (⋂S) = prob (hd xs) * (∏i ∈ {1..<(length xs)} . 𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)))"
    using prob_cond_Inter_List_Index[of xs] assms(3) assms(4) seq by auto
  then have "prob (⋂S) = prob (hd xs) * (∏i ∈ {1..<card S} . 𝒫(g i | (⋂ j ∈ {0..<i} . g j)))"
    using geq len by auto
  moreover have "hd xs = g 0" 
  proof -
    have "length xs > 0" using seq assms(3) by auto 
    then have "hd xs = xs ! 0"
      by (simp add: hd_conv_nth) 
    then show ?thesis using geq len
      using ‹0 < length xs› by auto 
  qed
  ultimately show ?thesis by simp
qed

lemma prob_cond_inter_obtain_fn: 
  assumes " S ≠ {}"
  assumes "S ⊆ events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S"  and 
    "prob (⋂S) = prob (f 0) * (∏i ∈ {1..<(card S)} . 𝒫(f i | (⋂(f ` {0..<i}))))"
proof -
  obtain f where "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  then show ?thesis using that prob_cond_inter_fn assms by auto
qed 


lemma prob_cond_inter_obtain_fn_compl: 
  assumes " S ≠ {}"
  assumes "S ⊆ events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S" and "prob (⋂((-) (space M) ` S)) = 
     prob (space M - f 0) * (∏i ∈ {1..<(card S)} . 𝒫(space M - f i | (⋂((-) (space M) ` f ` {0..<i}))))"
proof -
  let ?c = "(-) (space M)"
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  moreover have bij: "bij_betw ?c S ((-) (space M) ` S)"
    using bij_betw_compl_sets_rev assms(2) by auto
  ultimately have "bij_betw (?c ∘ f) {0..<card S} (?c ` S)"
    using bij_betw_comp_iff by blast 
  moreover have "?c ` S ≠ {}" using assms(1) by auto
  moreover have "finite (?c ` S )" using assms(3) by auto
  moreover have "?c ` S ⊆ events" using assms(2) by auto
  moreover have "card S = card (?c ` S)" using bij
    by (simp add: bij_betw_same_card)  
  ultimately have "prob (⋂(?c ` S)) = prob ((?c ∘ f) 0) * 
    (∏i ∈ {1..<(card S)} . 𝒫((?c ∘ f) i | (⋂((?c ∘ f) ` {0..<i}))))"
    using prob_cond_inter_fn[of "(?c ∘ f)" "(?c ` S)"] by auto
  then have "prob (⋂(?c ` S)) = prob (space M - (f 0)) * 
    (∏i ∈ {1..<(card S)} . 𝒫(space M -  (f i) | (⋂((?c ∘ f) ` {0..<i}))))" by simp
  then show ?thesis using that bb by simp
qed 

lemma prob_cond_Inter_index_cond_fn:
  assumes "I ≠ {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` I ⊆ events"
  assumes "prob (⋂E) > 0"
  assumes bb: "bij_betw g {0..<card I} I"
  shows "𝒫((⋂(F ` g ` {0..<card I})) | (⋂E)) = 
    (∏i ∈ {0..<card I}.  𝒫(F (g i) | (⋂((F ` g` {0..<i}) ∪ E))))"
proof -
  let ?n = "card I"
  have eq: "F ` I = (F ∘ g) ` {0..<card I}" using bij_betw_image_comp_eq bb  by metis
  moreover have "0 < ?n" using assms(1) assms(2) by auto
  ultimately have "𝒫(⋂ ((F ∘ g) ` {0..<card I}) | ⋂ E) = 
      (∏i = 0..<?n. 𝒫(F (g i) | ⋂ ((F ∘ g) ` {0..<i} ∪ E)))"
    using prob_cond_Inter_index_cond_set[of ?n E "(F ∘ g)"] assms(3) assms(4) assms(5) assms(6) 
      assms(7) by auto
  moreover have "⋀ i. i ∈ {0..<?n} ⟹ (F ∘ g) ` {0..<i} = F ` g ` {0..<i}" using image_comp by auto
  ultimately have "𝒫(⋂ (F ` g ` {0..<card I}) | ⋂ E) = (∏i = 0..<?n. 𝒫(F (g i) | ⋂ (F ` g ` {0..<i} ∪ E)))" 
    using image_comp[of F g "{0..<card I}"] by auto
  then show ?thesis using eq bb assms by blast
qed

lemma prob_cond_Inter_index_cond_obtains:
  assumes "I ≠ {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` I ⊆ events"
  assumes "prob (⋂E) > 0"
  obtains g where "bij_betw g {0..<card I} I" and  "𝒫((⋂(F ` g ` {0..<card I})) | (⋂E)) = 
    (∏i ∈ {0..<card I}.  𝒫(F (g i) | (⋂((F ` g` {0..<i}) ∪ E))))"
proof -
  obtain g where bb: "bij_betw g {0..<card I} I" using assms(2) ex_bij_betw_nat_finite by auto
  then show thesis using assms prob_cond_Inter_index_cond_fn[of I E F g] that by blast
qed

lemma prob_cond_Inter_index_cond_compl_fn:
  assumes "I ≠ {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` I ⊆ events"
  assumes "prob (⋂E) > 0"
  assumes bb: "bij_betw g {0..<card I} I"
  shows "𝒫((⋂Aj ∈ I . space M - F Aj) | (⋂E)) = 
    (∏i ∈ {0..<card I}.  𝒫(space M - F (g i) | (⋂(((λAj. space M - F Aj) ` g ` {0..<i}) ∪ E))))"
proof -
  let ?n = "card I"
  let ?G = "λ i. space M - F i"
  have eq: "?G ` I = (?G ∘ g) ` {0..<card I}" using bij_betw_image_comp_eq bb by metis
  then have "(?G ∘ g) ` {0..<card I}  ⊆ events" using assms(5)
    by (metis assms(6) compl_subset_in_events image_image) 
  moreover have "0 < ?n" using assms(1) assms(2) by auto
  ultimately have "𝒫(⋂ ((?G ∘ g) ` {0..<card I}) | ⋂ E) = (∏i = 0..<?n. 𝒫(?G (g i) | ⋂ ((?G ∘ g) ` {0..<i} ∪ E)))"
    using prob_cond_Inter_index_cond_set[of ?n E "(?G ∘ g)"] assms(3) assms(4) assms(5) assms(6) 
      assms(7) by auto
  moreover have "⋀ i. i ∈ {0..<?n} ⟹ (?G ∘ g) ` {0..<i} = ?G ` g ` {0..<i}" using image_comp by auto
  ultimately have "𝒫(⋂ (?G ` I) | ⋂ E) = (∏i = 0..<?n. 𝒫(?G (g i) | ⋂ (?G ` g ` {0..<i} ∪ E)))" 
    using image_comp[of ?G g "{0..<card I}"] eq by auto
  then show ?thesis using bb by blast
qed

lemma prob_cond_Inter_index_cond_compl_obtains:
  assumes "I ≠ {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E ≠ {}"
  assumes "E ⊆ events"
  assumes "F ` I ⊆ events"
  assumes "prob (⋂E) > 0"
  obtains g where "bij_betw g {0..<card I} I" and "𝒫((⋂Aj ∈ I . space M - F Aj) | (⋂E)) = 
    (∏i ∈ {0..<card I}.  𝒫(space M - F (g i) | (⋂(((λAj. space M - F Aj) ` g ` {0..<i}) ∪ E))))"
proof -
  let ?n = "card I"
  let ?G = "λ i. space M - F i"
  obtain g where bb: "bij_betw g {0..<?n} I" using assms(2) ex_bij_betw_nat_finite by auto
  then show ?thesis using assms prob_cond_Inter_index_cond_compl_fn[of I E F g] that by blast
qed

lemma prob_cond_inter_index_fn2: 
  assumes "F ` S ⊆ events"
  assumes "finite S"
  assumes "card S > 0"
  assumes "bij_betw g {0..<card S} S"
  shows "prob (⋂(F `S)) = prob (F (g 0)) * (∏i ∈ {1..<(card S)} . 𝒫(F (g i) | (⋂(F ` g ` {0..<i}))))"
proof -
  have 1: "F ` S = (F ∘ g) ` {0..<card S}" using assms(4) bij_betw_image_comp_eq  by metis
  moreover have "prob (⋂((F ∘ g) ` {0..<card S})) = 
      prob (F (g 0)) * (∏i ∈ {1..<(card S)} . 𝒫(F (g i) | (⋂(F ` g ` {0..<i}))))"
    using 1 prob_cond_Inter_index[of "card S" "F ∘ g"] assms(3) assms(1) by auto
  ultimately show ?thesis using assms(4)
    by metis
qed 

lemma prob_cond_inter_index_fn: 
  assumes "F ` S ⊆ events"
  assumes "finite S"
  assumes "S ≠ {}"
  assumes "bij_betw g {0..<card S} S"
  shows "prob (⋂(F `S)) = prob (F (g 0)) * (∏i ∈ {1..<(card S)} . 𝒫(F (g i) | (⋂(F ` g ` {0..<i}))))"
proof -
  have "card S > 0" using assms(3) assms(2)
    by (simp add: card_gt_0_iff) 
  moreover have "(F ∘ g) ` {0..<card S} ⊆ events" using assms(1) assms(4)
    using  bij_betw_imp_surj_on by (metis image_comp) 
  ultimately have "prob (⋂((F ∘ g) ` {0..<card S})) = 
      prob (F (g 0)) * (∏i ∈ {1..<(card S)} . 𝒫(F (g i) | (⋂(F ` g ` {0..<i}))))"
    using prob_cond_Inter_index[of "card S" "F ∘ g"] by auto
  moreover have "F ` S = (F ∘ g) ` {0..<card S}" using assms(4) 
    using bij_betw_imp_surj_on image_comp by (metis) 
  ultimately show ?thesis using assms(4) by presburger 
qed 

lemma prob_cond_inter_index_obtain_fn: 
  assumes "F ` S ⊆ events"
  assumes "finite S"
  assumes "S ≠ {}"
  obtains g where "bij_betw g {0..<card S} S"  and 
    "prob (⋂(F `S)) = prob (F (g 0)) * (∏i ∈ {1..<(card S)} . 𝒫(F (g i) | (⋂(F ` g ` {0..<i}))))"
proof -
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(2) ex_bij_betw_nat_finite by blast 
  then show ?thesis using prob_cond_inter_index_fn that assms by blast 
qed 

lemma prob_cond_inter_index_fn_compl: 
  assumes " S ≠ {}"
  assumes "F ` S ⊆ events"
  assumes "finite S"
  assumes "bij_betw f {0..<card S} S"
  shows "prob (⋂((-) (space M) ` F ` S)) = prob (space M - F (f 0)) * 
    (∏i ∈ {1..<(card S)} . 𝒫(space M - F (f i) | (⋂((-) (space M) ` F ` f ` {0..<i}))))"
proof -
  define G where "G ≡ λ i. space M - F i"
  then have "G ` S ⊆ events" using G_def assms(2) by auto
  then have "prob (⋂ (G ` S)) = prob (G (f 0)) * (∏i = 1..<card S. 𝒫(G (f i) | ⋂ (G ` f ` {0..<i})))"
    using prob_cond_inter_index_fn[of G S] assms by auto
  moreover have "(⋂((-) (space M) ` F ` S)) = (⋂i∈S. space M - F i)" by auto
  ultimately show ?thesis unfolding G_def by auto
qed


lemma prob_cond_inter_index_obtain_fn_compl: 
  assumes " S ≠ {}"
  assumes "F ` S ⊆ events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S"  and 
    "prob (⋂((-) (space M) ` F ` S)) = prob (space M - F (f 0)) * 
      (∏i ∈ {1..<(card S)} . 𝒫(space M - F (f i) | (⋂((-) (space M) ` F ` f ` {0..<i}))))"
proof -
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  then show ?thesis using prob_cond_inter_index_fn_compl[of S F f] assms that by blast
qed

lemma prob_cond_Inter_take: 
  assumes " S ≠ {}"
  assumes "S ⊆ events"
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S" and 
    "prob (⋂S) = prob (hd xs) * (∏i = 1..<(length xs) . 𝒫((xs ! i) | (⋂(set (take i xs )))))"
  using assms prob_cond_Inter_List exists_list_card 
  by (metis (no_types, lifting) set_empty2 subset_code(1)) 


lemma prob_cond_Inter_set_bound: 
  assumes " A ≠ {}"
  assumes "A ⊆ events"
  assumes "finite A"
  assumes "⋀ Ai . f Ai ≥ 0 ∧ f Ai ≤ 1"
  assumes "⋀Ai S. Ai ∈ A ⟹ S ⊆ A - {Ai} ⟹ S ≠ {} ⟹ 𝒫(Ai | (⋂S)) ≥ f Ai"
  assumes "⋀ Ai. Ai ∈ A ⟹ prob Ai ≥ f Ai"
  shows "prob (⋂A) ≥ (∏a' ∈ A .  f a')"
proof - 
  obtain xs where eq: "set xs = A" and seq: "length xs = card A" and
    pA: "prob (⋂A) = prob (hd xs) * (∏i = 1..<(length xs) . 𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)))"
    using assms obtains_prob_cond_Inter_index[of A] by blast
  then have dis: "distinct xs" using card_distinct
    by metis 
  then have "hd xs ∈ A" using eq hd_in_set assms(1) by auto
  then have "prob (hd xs) ≥ (f (hd xs))" using assms(6) by blast
  have "⋀ i. i ∈ {1..<(length xs)} ⟹ 𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)) ≥ f (xs ! i)"
  proof -
    fix i assume "i ∈ {1..<length xs}"
    then have ilb: "i ≥ 1" and iub: "i < length xs" by auto
    then have xsin: "xs ! i ∈ A" using eq by auto
    define S where "S = (λ j. xs ! j) ` {0..<i}"
    then have "S = set (take i xs)"
      by (simp add: iub less_or_eq_imp_le nth_image)
    then have "xs ! i ∉ S" using dis set_take_distinct_elem_not iub by simp
    then have "S ⊆ A - {(xs ! i)}"
      using ‹S = set (take i xs)› eq set_take_subset by fastforce 
    moreover have "S ≠ {}" using S_def ilb by (simp) 
    moreover have "𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)) = 𝒫((xs ! i) | (⋂ Aj ∈ S . Aj))" 
      using S_def by auto
    ultimately show "𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j)) ≥ f (xs ! i)"
      using assms(5) xsin by auto
  qed
  then have "(∏i = 1..<(length xs) . 𝒫((xs ! i) | (⋂ j ∈ {0..<i} . xs ! j))) ≥ 
    (∏i = 1..<(length xs) . f (xs ! i))"
    by (meson assms(4) prod_mono)
  moreover have "(∏i = 1..<(length xs) . f (xs ! i)) = (∏a ∈ A - {hd xs} . f a)"
  proof -
    have ne: "xs ≠ []" using assms(1) eq by auto
    have "A = (λ j. xs ! j) ` {0..<length xs}" using eq
      by (simp add: nth_image) 
    have "A - {hd xs} = set (tl xs) " using dis
      by (metis Diff_insert_absorb distinct.simps(2) eq list.exhaust_sel list.set(2) ne)
    also have "... = (λ j. xs ! j) ` {1..<length xs}" using nth_image_tl ne by auto
    finally have Ahdeq: "A - {hd xs} = (λ j. xs ! j) ` {1..<length xs}" by simp
    have io: "inj_on (nth xs) {1..<length xs}" using inj_on_nth dis
      by (metis atLeastLessThan_iff) 
    have "(∏i = 1..<(length xs) . f (xs ! i)) = (∏i ∈ {1..<(length xs)} . f (xs ! i))" by simp
    also have "... = (∏i ∈ (λ j. xs ! j) ` {1..<length xs} . f i)" 
      using io by (simp add: prod.reindex_cong) 
    finally show ?thesis using Ahdeq
      using ‹(∏i = 1..<length xs. f (xs ! i)) = prod f ((!) xs ` {1..<length xs})› by presburger 
  qed
  ultimately have "prob (⋂A) ≥ f (hd xs) * (∏a ∈ A - {hd xs} . f a)"
    using pA ‹f (hd xs) ≤ prob (hd xs)› assms(4) ordered_comm_semiring_class.comm_mult_left_mono
    by (simp add: mult_mono' prod_nonneg)  
  then show ?thesis
    by (metis ‹hd xs ∈ A› assms(3) prod.remove) 
qed
end

end