Theory Lovasz_Local.Indep_Events

(* Theory: Indep_Events.thy
   Author: Chelsea Edmonds *)

section ‹ Independent Events ›
theory Indep_Events imports Cond_Prob_Extensions
begin

subsection ‹More bijection helpers›

lemma bij_betw_obtain_subsetr:
  assumes "bij_betw f A B"
  assumes "A' ⊆ A"
  obtains B' where "B' ⊆ B" and "B' = f ` A'"
  using assms by (metis bij_betw_def image_mono) 

lemma bij_betw_obtain_subsetl:
  assumes "bij_betw f A B"
  assumes "B' ⊆ B"
  obtains A' where "A' ⊆ A" and "B' = f ` A'"
  using assms
  by (metis bij_betw_imp_surj_on subset_imageE) 

lemma bij_betw_remove:  "bij_betw f A B ⟹ a ∈ A ⟹ bij_betw f (A - {a}) (B - {f a})"
  using  bij_betwE notIn_Un_bij_betw3
  by (metis Un_insert_right insert_Diff member_remove  remove_def sup_bot.right_neutral)
(* Slow *)

subsection ‹Independent Event Extensions ›
text ‹ Extensions on both the indep\_event definition and the indep\_events definition ›
context prob_space
begin

lemma indep_eventsD: "indep_events A I ⟹ (A`I ⊆ events) ⟹ J ⊆ I ⟹ J ≠ {} ⟹ finite J ⟹ 
    prob (⋂j∈J. A j) = (∏j∈J. prob (A j))"
  using indep_events_def[of A I] by auto 

lemma
  assumes indep: "indep_event A B"
  shows indep_eventD_ev1: "A ∈ events"
    and indep_eventD_ev2: "B ∈ events"
  using indep unfolding indep_event_def indep_events_def UNIV_bool by auto

lemma indep_eventD: 
  assumes ie: "indep_event A B"
  shows "prob (A ∩ B) = prob (A) * prob (B)"
  using assms indep_eventD_ev1 indep_eventD_ev2 ie[unfolded indep_event_def, THEN indep_eventsD,of UNIV] 
  by (simp add: ac_simps UNIV_bool)

lemma  indep_eventI[intro]:
  assumes ev: "A ∈ events" "B ∈ events"
    and indep: "prob (A ∩ B) = prob A * prob B"
  shows "indep_event A B"
  unfolding indep_event_def
proof (intro indep_eventsI)
  show "⋀i. i ∈ UNIV ⟹ (case i of True ⇒ A | False ⇒ B) ∈ events" 
    using assms by (auto split: bool.split)
next
  fix J :: "bool set" assume jss: "J ⊆ UNIV" and jne: "J ≠ {}"  and finJ: "finite J"
  have "J ∈ Pow UNIV" by auto
  then have c: "J = UNIV ∨ J = {True} ∨ J = {False}" using jne jss UNIV_bool
    by (metis (full_types) UNIV_eq_I insert_commute subset_insert subset_singletonD) 
  then show "prob (⋂i∈J. case i of True ⇒ A | False ⇒ B) = 
      (∏i∈J. prob (case i of True ⇒ A | False ⇒ B)) "
    unfolding UNIV_bool using indep by (auto simp: ac_simps)
qed

text ‹Alternate set definition - when no possibility of duplicate objects ›

definition indep_events_set :: "'a set set ⇒ bool" where
"indep_events_set E ≡ (E ⊆ events ∧ (∀J. J ⊆ E ⟶ finite J ⟶ J ≠ {} ⟶ prob (⋂J) = (∏i∈J. prob i)))"

lemma indep_events_setI[intro]: "E ⊆ events ⟹ (⋀J. J ⊆ E ⟹ finite J ⟹ J ≠ {} ⟹ 
    prob (⋂J) = (∏i∈J. prob i)) ⟹ indep_events_set E"
  using indep_events_set_def by simp

lemma indep_events_subset:
  "indep_events_set E ⟷ (∀J⊆E. indep_events_set J)"
  by (auto simp: indep_events_set_def)

lemma indep_events_subset2:
  "indep_events_set E ⟹ J ⊆ E ⟹ indep_events_set J"
  by (auto simp: indep_events_set_def)

lemma indep_events_set_events: "indep_events_set E ⟹ (⋀e. e ∈ E ⟹ e ∈ events)" 
  using indep_events_set_def by auto

lemma indep_events_set_events_ss: "indep_events_set E ⟹  E ⊆ events" 
  using indep_events_set_events by auto

lemma indep_events_set_probs: "indep_events_set E ⟹ J ⊆ E ⟹ finite J ⟹ J ≠ {} ⟹ 
    prob (⋂J) = (∏i∈J. prob i)"
  by (simp add: indep_events_set_def)

lemma indep_events_set_prod_all: "indep_events_set E ⟹ finite E ⟹ E ≠ {} ⟹
     prob (⋂E) = prod prob E" 
  using indep_events_set_probs by simp

lemma indep_events_not_contain_compl: 
  assumes "indep_events_set E"
  assumes "A ∈ E"
  assumes "prob A > 0" "prob A < 1"
  shows "(space M - A) ∉ E" (is "?A' ∉ E")
proof (rule ccontr)
  assume "¬ (?A') ∉ E" 
  then have "?A' ∈ E" by auto
  then have "{A, ?A'} ⊆ E" using assms(2) by auto
  moreover have "finite {A, ?A'}" by simp
  moreover have "{A, ?A'} ≠ {}"
    by simp
  ultimately have "prob (⋂i∈{A, ?A'}. i) = (∏i∈{A, ?A'}. prob i)" 
    using indep_events_set_probs[of E "{A, ?A'}"] assms(1) by auto
  then have "prob (A ∩ ?A') = prob A * prob ?A'" by simp
  moreover have "prob (A ∩ ?A') = 0" by simp
  moreover have "prob A * prob ?A' = prob A * (1 - prob A)"
    using assms(1) assms(2) indep_events_set_events prob_compl by auto 
  moreover have "prob A * (1 - prob A) > 0" using assms(3) assms(4) by (simp add: algebra_simps)
  ultimately show False by auto
qed

lemma indep_events_contain_compl_prob01: 
  assumes "indep_events_set E"
  assumes "A ∈ E"
  assumes "space M - A ∈ E"
  shows "prob A = 0 ∨ prob A = 1"
proof (rule ccontr)
  let ?A' = "space M - A"
  assume a: "¬ (prob A = 0 ∨ prob A = 1)"
  then have "prob A > 0"
    by (simp add: zero_less_measure_iff)
  moreover have "prob A < 1"
    using a measure_ge_1_iff by fastforce
  ultimately have "?A' ∉ E" using assms(1) assms(2) indep_events_not_contain_compl by auto
  then show False using assms(3) by auto
qed

lemma indep_events_set_singleton: 
  assumes "A ∈ events"
  shows "indep_events_set {A}"
proof (intro indep_events_setI)
  show "{A} ⊆ events" using assms by simp
next
  fix J assume "J ⊆ {A}" "finite J" "J ≠ {}"
  then have "J = {A}" by auto
  then show "prob (⋂J) = prod prob J" by simp
qed
 

lemma indep_events_pairs: 
  assumes "indep_events_set S"
  assumes "A ∈ S" "B ∈ S" "A ≠ B"
  shows "indep_event A B"
  using assms indep_events_set_probs[of "S" "{A, B}"] 
  by (intro indep_eventI) (simp_all add: indep_events_set_events)

lemma indep_events_inter_pairs: 
  assumes "indep_events_set S"
  assumes "finite A" "finite B"
  assumes "A ≠ {}" "B ≠ {}"
  assumes "A ⊆ S" "B ⊆ S" "A ∩ B = {}"
  shows "indep_event (⋂A) (⋂B)"
proof (intro indep_eventI)
  have "A ⊆ events" "B ⊆ events" using indep_events_set_events assms by auto
  then show "⋂ A ∈ events" "⋂ B ∈ events" using Inter_event_ss assms by auto
next
  have "A ∪ B ⊆ S" using assms by auto
  then have "prob (⋂(A ∪ B)) = prod prob (A ∪ B)" using assms
    by (metis Un_empty indep_events_subset infinite_Un prob_space.indep_events_set_prod_all prob_space_axioms) 
  also have "... = prod prob A * prod prob B" using assms(8)
    by (simp add: assms(2) assms(3) prod.union_disjoint) 
  finally have "prob (⋂(A ∪ B)) = prob (⋂ A) * prob (⋂ B)" 
    using assms indep_events_subset indep_events_set_prod_all by metis 
  moreover have "⋂ (A ∪ B) = (⋂ A ∩ ⋂ B)" by auto
  ultimately show "prob (⋂ A ∩ ⋂ B) = prob (⋂ A) * prob (⋂ B)"
    by simp
qed

lemma indep_events_inter_single: 
  assumes "indep_events_set S"
  assumes "finite B"
  assumes "B ≠ {}"
  assumes "A ∈ S" "B ⊆ S" "A ∉ B"
  shows "indep_event A (⋂B)"
proof -
  have "{A} ≠ {}" "finite {A}" "{A} ⊆ S" using assms by simp_all
  moreover have "{A} ∩ B = {}" using assms(6) by auto
  ultimately show ?thesis using indep_events_inter_pairs[of S "{A}" B] assms by auto
qed

lemma indep_events_set_prob1: 
  assumes "A ∈ events"
  assumes "prob A = 1"
  assumes "A ∉ S"
  assumes "indep_events_set S"
  shows "indep_events_set (S ∪ {A})"
proof (intro indep_events_setI)
  show " S ∪ {A} ⊆ events" using assms(1) assms(4) indep_events_set_events by auto
next
  fix J assume jss: "J ⊆ S ∪ {A}" and finJ: "finite J" and jne: "J ≠ {}"
  show "prob (⋂J) = prod prob J"
  proof (cases "A ∈ J")
    case t1: True
    then show ?thesis 
    proof (cases "J = {A}")
      case True
      then show ?thesis using indep_events_set_singleton assms(1) by auto
    next
      case False
      then have jun: "(J - {A}) ∪ {A} = J" using t1 by auto
      have "J - {A} ⊆ S" using jss by auto
      then have iej: "indep_events_set (J - {A})" using indep_events_subset2[of S "J - {A}"] assms(4) 
        by auto
      have jsse: "J - {A} ⊆ events" using indep_events_set_events jss
        using assms(4) by blast 
      have jne2: "J - {A} ≠ {}" using False jss jne by auto
      have split: "(J - {A}) ∩ {A} = {}" by auto
      then have "prob (⋂i∈J. i) = prob ((⋂i∈(J - {A}). i) ∩ A)" using jun
        by (metis Int_commute Inter_insert Un_ac(3) image_ident insert_is_Un) 
      also have "... = prob ((⋂i∈(J - {A}). i))" 
        using prob1_basic_Inter[of A "J - {A}"] jsse assms(2) jne2 assms(1) finJ 
        by (simp add: Int_commute)
      also have "... = prob (⋂(J - {A})) * prob A" using assms(2) by simp
      also have "... = (prod prob (J - {A})) * prob A"
        using iej indep_events_set_prod_all[of "J - {A}"] jne2 finJ finite_subset by auto
      also have "... = prod prob ((J - {A}) ∪ {A})" using split
        by (metis finJ jun mult.commute prod.remove t1) 
      finally show ?thesis using jun by auto 
    qed 
  next
    case False
    then have jss2: "J ⊆ S" using jss by auto
    then have "indep_events_set J" using assms(4) indep_events_subset2[of S J] by auto
    then show ?thesis using indep_events_set_probs finJ jne jss2 by auto
  qed
qed

lemma indep_events_set_prob0: 
  assumes "A ∈ events"
  assumes "prob A = 0"
  assumes "A ∉ S"
  assumes "indep_events_set S"
  shows "indep_events_set (S ∪ {A})"
proof (intro indep_events_setI)
  show "S ∪ {A}⊆ events" using assms(1) assms(4) indep_events_set_events by auto
next
  fix J assume jss: "J ⊆ S ∪ {A}" and finJ: "finite J" and jne: "J ≠ {}"
  show "prob (⋂J) = prod prob J"
  proof (cases "A ∈ J")
    case t1: True
    then show ?thesis 
    proof (cases "J = {A}")
      case True
      then show ?thesis using indep_events_set_singleton assms(1) by auto
    next
      case False
      then have jun: "(J - {A}) ∪ {A} = J" using t1 by auto
      have "J - {A} ⊆ S" using jss by auto
      then have iej: "indep_events_set (J - {A})" using indep_events_subset2[of S "J - {A}"] assms(4) by auto
      have jsse: "J - {A} ⊆ events" using indep_events_set_events jss
        using assms(4) by blast 
      have jne2: "J - {A} ≠ {}" using False jss jne by auto
      have split: "(J - {A}) ∩ {A} = {}" by auto
      then have "prob (⋂i∈J. i) = prob ((⋂i∈(J - {A}). i) ∩ A)" using jun
        by (metis Int_commute Inter_insert Un_ac(3) image_ident insert_is_Un) 
      also have "... = 0" 
        using prob0_basic_Inter[of A "J - {A}"] jsse assms(2) jne2 assms(1) finJ 
        by (simp add: Int_commute)
      also have "... = prob (⋂(J - {A})) * prob A" using assms(2) by simp
      also have "... = (prod prob (J - {A})) * prob A" using iej indep_events_set_prod_all[of "J - {A}"] jne2 finJ finite_subset by auto
      also have "... = prod prob ((J - {A}) ∪ {A})" using split
        by (metis finJ jun mult.commute prod.remove t1) 
      finally show ?thesis using jun by auto 
    qed 
  next
    case False
    then have jss2: "J ⊆ S" using jss by auto
    then have "indep_events_set J" using assms(4) indep_events_subset2[of S J] by auto
    then show ?thesis using indep_events_set_probs finJ jne jss2 by auto
  qed
qed


lemma indep_event_commute: 
  assumes "indep_event A B"
  shows "indep_event B A"
  using indep_eventI[of "B" "A"] indep_eventD[unfolded assms(1), of "A" "B"]
  by (metis Groups.mult_ac(2) Int_commute assms indep_eventD_ev1 indep_eventD_ev2)

text‹Showing complement operation maintains independence ›

lemma indep_event_one_compl:
  assumes "indep_event A B"
  shows "indep_event A (space M - B)"
proof -
  let ?B' = "space M - B"
  have "A = (A ∩ B) ∪ (A ∩ ?B')"
    by (metis Int_Diff Int_Diff_Un assms prob_space.indep_eventD_ev1 prob_space_axioms sets.Int_space_eq2)
  then have "prob A = prob (A ∩ B) + prob (A ∩ ?B')"
    by (metis Diff_Int_distrib Diff_disjoint assms finite_measure_Union indep_eventD_ev1 
        indep_eventD_ev2 sets.Int sets.compl_sets)
  then have "prob (A ∩ ?B') = prob A - prob (A ∩ B)" by simp   
  also have "... = prob A - prob A * prob B" using indep_eventD assms(1) by auto
  also have "... = prob A * (1 - prob B)"
    by (simp add: vector_space_over_itself.scale_right_diff_distrib)
  finally have "prob (A ∩ ?B') = prob A * prob ?B'"
    using prob_compl indep_eventD_ev1 assms(1) indep_eventD_ev2 by presburger 
  then show "indep_event A ?B'" using indep_eventI indep_eventD_ev2 indep_eventD_ev1 assms(1)
    by (meson sets.compl_sets) 
qed

lemma indep_event_one_compl_rev:
  assumes "B ∈ events"
  assumes "indep_event A (space M - B)"
  shows "indep_event A B"
proof -
  have "space M - B ∈ events" using indep_eventD_ev2 assms by auto
  have "space M - (space M - B) = B" using compl_identity assms by simp
  then show ?thesis using indep_event_one_compl[of "A" "space M - B"] assms(2) by auto
qed

lemma indep_event_double_compl: "indep_event A B ⟹ indep_event (space M - A) (space M - B)"
  using indep_event_one_compl indep_event_commute by auto

lemma indep_event_double_compl_rev: "A ∈ events ⟹ B ∈ events ⟹ 
    indep_event (space M - A) (space M - B) ⟹ indep_event A B"
  using indep_event_double_compl[of "space M - A" "space M - B"] compl_identity by auto

lemma indep_events_set_one_compl: 
  assumes "indep_events_set S"
  assumes "A ∈ S"
  shows "indep_events_set ({space M - A} ∪ (S - {A}))"
proof (intro indep_events_setI)
  show "{space M - A} ∪ (S - {A}) ⊆ events"
    using indep_events_set_events assms(1) assms(2) by auto
next
  fix J assume jss: "J ⊆ {space M - A} ∪ (S - {A})"
  assume finJ: "finite J"
  assume jne: "J ≠ {}" 
  show "prob (⋂J) = prod prob J"
  proof (cases "J - {space M - A} = {}")
    case True
    then have "J = {space M - A}" using jne by blast
    then show ?thesis by simp
  next
    case jne2: False
    have jss2: "J - {space M - A} ⊆ S" using jss assms(2) by auto
    moreover have "A ∉ (J - {space M - A})" using jss by auto
    moreover have "finite (J - {space M - A})" using finJ by simp
    ultimately have "indep_event A (⋂ (J - {space M - A}))" 
      using indep_events_inter_single[of S "(J - {space M - A})" A] assms jne2 by auto
    then have ie: "indep_event (space M - A) (⋂ (J - {space M - A}))" 
      using indep_event_one_compl indep_event_commute by auto
    have iess: "indep_events_set (J - {space M - A})" 
      using jss2 indep_events_subset2[of S "J - {space M - A}"] assms(1) by auto
    show ?thesis 
    proof (cases "space M - A ∈ J")
      case True
      then have split: "J = (J - {space M - A}) ∪ {space M - A}" by auto
      then have "prob (⋂ J) = prob (⋂ ((J - {space M - A}) ∪ {space M - A}))" by simp
      also have "... = prob ((⋂ (J - {space M - A})) ∩ (space M - A))"
        by (metis Inter_insert True ‹J = J - {space M - A} ∪ {space M - A}› inf.commute insert_Diff) 
      also have "... = prob (⋂ (J - {space M - A})) * prob (space M - A)" 
        using ie indep_eventD[of "⋂ (J - {space M - A})" "space M - A"] indep_event_commute by auto
      also have "... = (prod prob ((J - {space M - A}))) * prob (space M - A)"
        using indep_events_set_prod_all[of "J - {space M - A}"] iess jne2 finJ by auto
      finally have "prob (⋂ J) = prod prob J" using split
        by (metis Groups.mult_ac(2) True finJ prod.remove) 
      then show ?thesis by simp
    next
      case False
      then show ?thesis using iess
        by (simp add: assms(1) finJ indep_events_set_prod_all jne) 
    qed
  qed
qed

lemma indep_events_set_update_compl: 
  assumes "indep_events_set E"
  assumes "E = A ∪ B"
  assumes "A ∩ B = {}"
  assumes "finite E"
  shows "indep_events_set (((-) (space M) ` A) ∪ B)"
using assms(2) assms(3)  proof (induct "card A" arbitrary: A B)
  case 0
  then show ?case using assms(1)
    using assms(4) by auto 
next
  case (Suc x)
  then obtain a A' where aeq: "A = insert a A'" and anotin: "a ∉ A'"
    by (metis card_Suc_eq_finite)
  then have xcard: "card A' = x"
    using Suc(2) Suc(3) assms(4) by auto
  let ?B' = "B ∪ {a}" 
  have "E = A' ∪ ?B'" using aeq Suc.prems by auto
  moreover have "A' ∩ ?B' = {}" using anotin Suc.prems(2) aeq by auto
  moreover have "?B' ≠ {}" by simp
  ultimately have ies: "indep_events_set ((-) (space M) ` A' ∪ ?B')" 
    using Suc.hyps(1)[of "A'" ?B'] xcard by auto
  then have "a ∈ A ∪ B" using aeq by auto
  then show ?case 
  proof (cases "(A ∪ B) - {a} = {}")
    case True
    then have "A = {a}" "B = {}" using Suc.prems aeq by auto
    then have "((-) (space M) ` A ∪ B) = {space M - a}" by auto
    moreover have "space M - a ∈ events" using aeq assms(1) Suc.prems indep_events_set_events by auto
    ultimately show ?thesis using indep_events_set_singleton by simp
  next
    case False
    have "a ∈ (-) (space M) ` A' ∪ ?B'" using aeq by auto
    then have ie: "indep_events_set ({space M - a} ∪ ((-) (space M) ` A' ∪ ?B' - {a}))" 
      using indep_events_set_one_compl[of "(-) (space M) ` A' ∪ ?B'" a] ies by auto
    show ?thesis 
    proof (cases "a ∈ (-) (space M) ` A'")
      case True
      then have "space M - a ∈ A'"
        by (smt (verit) ‹E = A' ∪ (B ∪ {a})› assms(1) compl_identity image_iff indep_events_set_events 
            indep_events_subset2 inf_sup_ord(3))
      then have "space M - a ∈ A" using aeq by auto
      moreover have "indep_events_set A" using Suc.prems(1) indep_events_subset2 assms(1)
        using aeq by blast 
      moreover have "a ∈ A" using aeq by auto
      ultimately have probs: "prob a = 0 ∨ prob a = 1" using indep_events_contain_compl_prob01[of A a] by auto
      have "((-) (space M) ` A ∪ B) = (-) (space M) ` A' ∪ {space M - a} ∪ B" using aeq by auto
      moreover have "((-) (space M) ` A' ∪ ?B' - {a}) = ((-) (space M) ` A' - {a}) ∪ B"
        using Suc.prems(2) aeq by auto
      moreover have "(-) (space M) ` A' = ((-) (space M) ` A' - {a}) ∪ {a}" using True by auto
      ultimately have "((-) (space M) ` A ∪ B) = {space M - a} ∪ ((-) (space M) ` A' ∪ ?B' - {a}) ∪ {a}"
        by (smt (verit) Un_empty_right Un_insert_right Un_left_commute) (* Longish*)
      moreover have "a ∉ {space M - a} ∪ ((-) (space M) ` A' ∪ ?B' - {a})"
        using Diff_disjoint ‹space M - a ∈ A'› anotin empty_iff insert_iff by fastforce 
      moreover have "a ∈ events" using Suc.prems(1) assms(1) indep_events_set_events aeq by auto
      ultimately show ?thesis
        using ie indep_events_set_prob0 indep_events_set_prob1 probs by presburger
    next
      case False
      then have "(((-) (space M) `A' ∪ ?B') - {a}) = (-) (space M) `A' ∪ B" 
        using Suc.prems(2) aeq by auto
      moreover have "(-) (space M) ` A = (-) (space M) ` A' ∪ {space M - a}" using aeq
        by simp
      ultimately have "((-) (space M) ` A ∪ B) = {space M - a} ∪ ((-) (space M) ` A' ∪ ?B' - {a})"
        by auto
      then show ?thesis using ie by simp
    qed
  qed
qed

lemma indep_events_set_compl: 
  assumes "indep_events_set E"
  assumes "finite E"
  shows "indep_events_set ((λ e. space M - e) ` E)"
  using indep_events_set_update_compl[of E E "{}"] assms by auto

lemma indep_event_empty:
  assumes "A ∈ events"
  shows "indep_event A {}"
  using assms indep_eventI by auto


lemma indep_event_compl_inter:
  assumes "indep_event A C"
  assumes "B ∈ events"
  assumes "indep_event A (B ∩ C)"
  shows "indep_event A ((space M - B) ∩ C)"
proof (intro indep_eventI)
  show "A ∈ events" using assms(1) indep_eventD_ev1 by auto
  show "(space M - B) ∩ C ∈ events" using assms(3) indep_eventD_ev2
    by (metis Diff_Int_distrib2 assms(1) sets.Diff sets.Int_space_eq1)
next
  have ac: "A ∩ C ∈ events" using assms(1) indep_eventD_ev1 indep_eventD_ev2 sets.Int_space_eq1 
    by auto
  have "prob (A ∩ ((space M - B) ∩ C)) = prob (A ∩ (space M - B) ∩ C)"
    by (simp add: inf_sup_aci(2))
  also have "... = prob (A ∩ C ∩ (space M - B))"
    by (simp add: ac_simps)
  also have "... = prob (A ∩ C) - prob (A ∩ C ∩ B)"
    using prob_compl_diff_inter[of "A ∩ C" "B"] ac assms(2) by auto
  also have "... = prob (A) * prob C - (prob A * prob (C ∩ B))"
    using assms(1) assms(3) indep_eventD
    by (simp add: inf_commute inf_left_commute) 
  also have "... = prob A * (prob C - prob (C ∩ B))" by (simp add: algebra_simps)
  finally have "prob (A ∩ ((space M - B) ∩ C)) = prob A * (prob (C ∩ (space M - B)))" 
    using prob_compl_diff_inter[of "C" "B"] using assms(1) assms(2)
    by (simp add: indep_eventD_ev2) 
  then show "prob (A ∩ ((space M - B) ∩ C)) = prob A * prob ((space M - B) ∩ C)" by (simp add: ac_simps)
qed

(* Indep events indexed lemmas *)

lemma indep_events_index_subset:
  "indep_events F E ⟷ (∀J⊆E. indep_events F J)"
  unfolding indep_events_def
  by (meson image_mono set_eq_subset subset_trans) 

lemma indep_events_index_subset2:
  "indep_events F E ⟹ J ⊆ E ⟹ indep_events F J"
  using indep_events_index_subset by auto

lemma indep_events_events_ss: "indep_events F E ⟹  F ` E ⊆ events" 
  unfolding indep_events_def by (auto) 

lemma indep_events_events: "indep_events F E ⟹ (⋀e. e ∈ E ⟹ F e ∈ events)" 
  using indep_events_events_ss by auto

lemma indep_events_probs: "indep_events F E ⟹ J ⊆ E ⟹ finite J ⟹ J ≠ {} ⟹ prob (⋂(F ` J)) = (∏i∈J. prob (F i))" 
  unfolding indep_events_def by auto

lemma indep_events_prod_all: "indep_events F E ⟹ finite E ⟹ E ≠ {} ⟹ prob (⋂(F ` E)) = (∏i∈E. prob (F i))" 
  using indep_events_probs by auto

lemma indep_events_ev_not_contain_compl: 
  assumes "indep_events F E"
  assumes "A ∈ E"
  assumes "prob (F A) > 0" "prob (F A) < 1"
  shows "(space M - F A) ∉ F ` E" (is "?A' ∉ F ` E")
proof (rule ccontr)
  assume "¬ ?A' ∉ F ` E" 
  then have "?A' ∈ F ` E" by auto
  then obtain Ae where aeq: "?A' = F Ae" and "Ae ∈ E" by blast
  then have "{A, Ae} ⊆ E" using assms(2) by auto
  moreover have "finite {A, Ae}" by simp
  moreover have "{A, Ae} ≠ {}"
    by simp
  ultimately have "prob (⋂i∈{A, Ae}. F i) = (∏i∈{A, Ae}. prob (F i))" using indep_events_probs[of F E "{A, Ae}"] assms(1) by auto
  moreover have "A ≠ Ae"
    using subprob_not_empty using aeq by auto
  ultimately have "prob (F A ∩ ?A') = prob (F A) * prob (?A')" using aeq by simp
  moreover have "prob (F A ∩ ?A') = 0" by simp 
  moreover have "prob (F A) * prob ?A' = prob (F A) * (1 - prob (F A))"
    using assms(1) assms(2) indep_events_events prob_compl by metis 
  moreover have "prob (F A) * (1 - prob (F A)) > 0" using assms(3) assms(4) by (simp add: algebra_simps)
  ultimately show False by auto
qed

lemma indep_events_singleton: 
  assumes "F A ∈ events"
  shows "indep_events F {A}"
proof (intro indep_eventsI)
  show "⋀i. i ∈ {A} ⟹ F i ∈ events" using assms by simp
next
  fix J assume "J ⊆ {A}" "finite J" "J ≠ {}"
  then have "J = {A}" by auto
  then show "prob (⋂ (F ` J)) = (∏i∈J. prob (F i))" by simp
qed
 

lemma indep_events_ev_pairs: 
  assumes "indep_events F S"
  assumes "A ∈ S" "B ∈ S" "A ≠ B"
  shows "indep_event (F A) (F B)"
  using assms indep_events_probs[of F "S" "{A, B}"] 
  by (intro indep_eventI) (simp_all add: indep_events_events)

lemma indep_events_ev_inter_pairs: 
  assumes "indep_events F S"
  assumes "finite A" "finite B"
  assumes "A ≠ {}" "B ≠ {}"
  assumes "A ⊆ S" "B ⊆ S" "A ∩ B = {}"
  shows "indep_event (⋂(F ` A)) (⋂(F ` B))"
proof (intro indep_eventI)
  have "(F ` A) ⊆ events" "(F `  B) ⊆ events" using indep_events_events assms(1) assms(6) assms(7) by fast+
  then show "⋂ (F ` A) ∈ events" "⋂ (F `B) ∈ events" using Inter_event_ss assms by auto
next
  have "A ∪ B ⊆ S" using assms by auto
  moreover have "finite (A ∪ B)" using assms(2) assms(3) by simp
  moreover have "A ∪ B ≠ {}" using assms by simp
  ultimately have "prob (⋂(F `(A ∪ B))) = (∏i∈A ∪ B. prob (F i))" using assms
    using  indep_events_probs[of F S "A ∪ B"] by simp
  also have "... = (∏i∈A. prob (F i)) * (∏i∈B. prob (F i))" 
    using assms(8) prod.union_disjoint[of A B "λ i. prob (F i)"] assms(2) assms(3) by simp
  finally have "prob (⋂(F `(A ∪ B))) = prob (⋂ (F ` A)) * prob (⋂ (F ` B))" 
    using assms indep_events_index_subset indep_events_prod_all by metis 
  moreover have "⋂ (F ` (A ∪ B)) = (⋂ (F ` A)) ∩ ⋂ (F ` B)" by auto
  ultimately show "prob (⋂ (F ` A) ∩ ⋂ (F ` B)) = prob (⋂ (F ` A)) * prob (⋂ (F ` B))"
    by simp
qed


lemma indep_events_ev_inter_single: 
  assumes "indep_events F S"
  assumes "finite B"
  assumes "B ≠ {}"
  assumes "A ∈ S" "B ⊆ S" "A ∉ B"
  shows "indep_event (F A) (⋂(F ` B))"
proof -
  have "{A} ≠ {}" "finite {A}" "{A} ⊆ S" using assms by simp_all
  moreover have "{A} ∩ B = {}" using assms(6) by auto
  ultimately show ?thesis using indep_events_ev_inter_pairs[of F S "{A}" B] assms by auto
qed

lemma indep_events_fn_eq: 
  assumes "⋀ Ai. Ai ∈ E ⟹ F Ai = G Ai"
  assumes "indep_events F E"
  shows "indep_events G E"
proof (intro indep_eventsI)
  show "⋀i. i ∈ E ⟹ G i ∈ events" using assms(2) indep_events_events assms(1)
    by metis 
next
  fix J assume jss: "J ⊆ E" "finite J" "J ≠ {}"
  moreover have "G ` J = F ` J" using assms(1) calculation(1) by auto
  moreover have "⋀ i . i ∈ J ⟹ prob (G i) = prob (F i)"  using jss assms(1) by auto
  moreover have "(∏i∈J. prob (F i)) = (∏i∈J. prob (G i))" using calculation(5) by auto
  ultimately show "prob (⋂ (G ` J)) = (∏i∈J. prob (G i))"
    using assms(2) indep_events_probs[of F E J] by simp
qed

lemma indep_events_fn_eq_iff: 
  assumes "⋀ Ai. Ai ∈ E ⟹ F Ai = G Ai"
  shows "indep_events F E ⟷ indep_events G E"
  using indep_events_fn_eq assms by auto

lemma indep_events_one_compl: 
  assumes "indep_events F S"
  assumes "A ∈ S"
  shows "indep_events (λ i. if (i = A) then (space M - F i) else F i) S" (is "indep_events ?G S")
proof (intro indep_eventsI)
  show "⋀i. i ∈ S ⟹ (if i = A then space M - F i else F i) ∈ events"
    using indep_events_events assms(1) assms(2)
    by (metis sets.compl_sets) 
next
  define G where "G ≡?G"
  fix J assume jss: "J ⊆ S"
  assume finJ: "finite J"
  assume jne: "J ≠ {}" 
  show "prob (⋂i∈J. ?G i) = (∏i∈J. prob (?G i))"
  proof (cases "J = {A}")
    case True
    then show ?thesis by simp
  next
    case jne2: False
    have jss2: "J - {A} ⊆ S" using jss assms(2) by auto
    moreover have "A ∉ (J - {A})" using jss by auto
    moreover have "finite (J - {A})" using finJ by simp
    moreover have "J - {A} ≠ {}" using jne2 jne by auto
    ultimately have "indep_event (F A) (⋂ (F ` (J -  {A})))" 
      using indep_events_ev_inter_single[of F S "(J - {A})" A] assms by auto
    then have ie: "indep_event (G A) (⋂ (G ` (J -  {A})))" 
      using indep_event_one_compl indep_event_commute G_def by auto
    have iess: "indep_events G (J - {A})" 
      using jss2 G_def indep_events_index_subset2[of F S "J - {A}"] assms(1) 
        indep_events_fn_eq[of "J - {A}"] by auto
    show ?thesis 
    proof (cases "A ∈ J")
      case True
      then have split: "G ` J = insert (G A) (G ` (J - {A}))" by auto
      then have "prob (⋂ (G ` J)) = prob (⋂ (insert (G A) (G ` (J - {A}))))" by auto
      also have "... = prob ((G A)∩ ⋂ (G ` (J - {A})) )"
        using Inter_insert by simp
      also have "... =  prob (G A) * prob (⋂ (G ` (J - {A})))" 
        using ie indep_eventD[of "G A" "⋂ (G ` (J - {A}))" ] by auto
      also have "... = prob (G A) * (∏i ∈ (J - {A}). prob (G i)) "
        using indep_events_prod_all[of G "J - {A}"] iess jne2 jne finJ by auto
      finally have "prob (⋂ (G ` J)) = (∏i ∈ J. prob (G i))" using split
        by (metis True finJ prod.remove) 
      then show ?thesis using G_def by simp
    next
      case False
      then have "prob (⋂i∈J. G i) = (∏i∈J. prob (G i))" using iess
        by (simp add: assms(1) finJ indep_events_prod_all jne) 
      then show ?thesis using G_def by simp
    qed
  qed
qed

lemma indep_events_update_compl: 
  assumes "indep_events F E"
  assumes "E = A ∪ B"
  assumes "A ∩ B = {}"
  assumes "finite E"
  shows "indep_events (λ Ai. if (Ai ∈ A) then (space M - (F Ai)) else (F Ai)) E" 
using assms(2) assms(3)  proof (induct "card A" arbitrary: A B)
  case 0
  let ?G = "(λAi. if Ai ∈ A then space M - F Ai else F Ai)"
  have "E = B" using  assms(4) ‹E = A ∪ B› ‹0 = card A›
    by simp 
  then have "⋀ i. i ∈ E ⟹ F i = ?G i" using ‹A ∩ B = {}› by auto
  then show ?case using assms(1) indep_events_fn_eq[of E F ?G] by simp
next
  case (Suc x)
  define G where  "G ≡ (λAi. if Ai ∈ A then space M - F Ai else F Ai)"
  obtain a A' where aeq: "A = insert a A'" and anotin: "a ∉ A'"
    using Suc.hyps by (metis card_Suc_eq_finite)
  then have xcard: "card A' = x"
    using Suc(2) Suc(3) assms(4) by auto
  define G1 where "G1 ≡ (λAi. if Ai ∈ A' then space M - F Ai else F Ai)"
  let ?B' = "B ∪ {a}" 
  have eeq: "E = A' ∪ ?B'" using aeq Suc.prems by auto
  moreover have "A' ∩ ?B' = {}" using anotin Suc.prems(2) aeq by auto
  moreover have "?B' ≠ {}" by simp
  ultimately have ies: "indep_events G1 (A' ∪ ?B')" 
    using Suc.hyps(1)[of "A'" ?B'] xcard G1_def by auto
  then have "a ∈ A ∪ B" using aeq by auto
  define G2  where "G2 ≡ λ Ai. if Ai = a then (space M - (G1 Ai)) else (G1 Ai)" 
  have "a ∈ A' ∪ ?B'" by auto
  then have ie: "indep_events G2 E" 
    using indep_events_one_compl[of G1 "(A' ∪ ?B')" a] ies G2_def eeq by auto
  moreover have "⋀ i. i ∈ E ⟹ G2 i = G i"
    unfolding G2_def G1_def G_def
    by (simp add: aeq anotin) 
  ultimately have "indep_events G E" using indep_events_fn_eq[of E G2 G] by auto
  then show ?case  using G_def by simp
qed

lemma indep_events_compl: 
  assumes "indep_events F E"
  assumes "finite E"
  shows "indep_events (λ Ai. space M - F Ai) E"
proof -
  have "indep_events (λAi. if Ai ∈ E then space M - F Ai else F Ai) E"
    using indep_events_update_compl[of F E E "{}"] assms by auto
  moreover have "⋀ i. i ∈ E ⟹ (λAi. if Ai ∈ E then space M - F Ai else F Ai) i = (λ Ai. space M - F Ai) i"
    by simp
  ultimately show ?thesis 
    using indep_events_fn_eq[of E "(λAi. if Ai ∈ E then space M - F Ai else F Ai)"] by auto
qed

lemma indep_events_impl_inj_on: 
  assumes "finite A"
  assumes "indep_events F A"
  assumes "⋀ A' . A' ∈ A ⟹ prob (F A') > 0 ∧ prob (F A') < 1"
  shows "inj_on F A"
proof (intro inj_onI, rule ccontr)
  fix x y assume xin: "x ∈ A" and yin: "y ∈ A" and feq: "F x = F y"
  assume contr: "x ≠ y"
  then have "{x, y} ⊆ A" "{x, y} ≠ {}" "finite {x, y}" using xin yin by auto
  then have "prob (⋂j∈{x, y}. F j) = (∏j∈{x, y}. prob (F j))" 
    using assms(2) indep_events_probs[of F A "{x, y}"] by auto
  moreover have "(∏j∈{x, y}. prob (F j)) = prob (F x) * prob (F y)" using contr by auto
  moreover have "prob (⋂j∈{x, y}. F j) = prob (F x)" using feq by simp
  ultimately have "prob (F x) = prob (F x) * prob (F x)" using feq by simp
  then show False using assms(3) using xin by fastforce 
qed

lemma indep_events_imp_set:
  assumes "finite A"
  assumes "indep_events F A"
  assumes "⋀ A' . A' ∈ A ⟹ prob (F A') > 0 ∧ prob (F A') < 1"
  shows "indep_events_set (F ` A)"
proof (intro indep_events_setI)
  show "F ` A ⊆ events" using assms(2) indep_events_events by auto
next 
  fix J assume jss: "J ⊆ F ` A" and finj: "finite J" and jne:"J ≠ {}"
  have bb: "bij_betw F A (F `A)" using bij_betw_imageI indep_events_impl_inj_on assms by meson
  then obtain I where iss: "I ⊆ A" and jeq: "J = F ` I" 
    using bij_betw_obtain_subsetl[OF bb] jss by metis
  moreover have "I ≠ {}" "finite I" using finj jeq jne assms(1) finite_subset iss by blast+
  ultimately have "prob (⋂ (F ` I)) = (∏i∈I. prob (F i))" 
    using jne finj jss indep_events_probs[of F A I] assms(2) by (simp)
  moreover have "bij_betw F I J" using jeq iss jss bb by (meson bij_betw_subset)
  ultimately show "prob (⋂ J) = prod prob J" using bij_betw_prod_prob jeq by (metis) 
qed

lemma indep_event_set_equiv_bij:
  assumes "bij_betw F A E"
  assumes "finite E"
  shows "indep_events_set E ⟷ indep_events F A"
proof -
  have im: "F ` A = E"
    using assms(1) by (simp add:  bij_betw_def) 
  then have ss: "(∀e. e ∈ E ⟶ e ∈ events) ⟷ (F ` A ⊆ events)"
    using image_iff by (simp add: subset_iff) 
  have prob: "(∀ J. J ⊆ E ⟶ finite J ⟶ J ≠ {} ⟶ prob (⋂i∈J. i) = (∏i∈J. prob i)) ⟷
        (∀ I. I ⊆ A ⟶ finite I ⟶ I ≠ {} ⟶ prob (⋂i∈I. F i) = (∏i∈I. prob (F i)))"
  proof (intro allI impI iffI)
    fix I assume p1: " ∀J⊆E. finite J ⟶ J ≠ {} ⟶ prob (⋂i∈J. i) = prod prob J"
      and iss: "I ⊆ A" and f1: "finite I" and i1: "I ≠ {}" 
    then obtain J where jeq: "J = F ` I" and jss: "J ⊆ E"
      using bij_betw_obtain_subsetr[OF assms(1) iss]by metis 
    then have "prob (⋂J) = prod prob J" using i1 f1 p1 jss by auto
    moreover have "bij_betw F I J" using jeq jss assms(1) iss
      by (meson bij_betw_subset) 
    ultimately show "prob (⋂ (F ` I)) = (∏i∈I. prob (F i))" using bij_betw_prod_prob
      by (metis jeq)  
  next
    fix J assume p2: "∀I⊆A. finite I ⟶ I ≠ {} ⟶ prob (⋂ (F ` I)) = (∏i∈I. prob (F i))"
      and jss:  "J ⊆ E" and f2: "finite J" and j1: "J ≠ {}"
    then obtain I where iss: "I ⊆ A" and jeq: "J = F ` I" 
      using bij_betw_obtain_subsetl[OF assms(1)] by metis
    moreover have "finite A" using assms(1) assms(2)
      by (simp add: bij_betw_finite) 
    ultimately have "prob (⋂ (F ` I)) = (∏i∈I. prob (F i))" using j1 f2 p2 jss
      by (simp add: finite_subset)
    moreover have "bij_betw F I J" using jeq iss assms(1) jss by (meson bij_betw_subset)
    ultimately show "prob (⋂i∈J. i) = prod prob J" using bij_betw_prod_prob jeq
      by (metis image_ident) 
  qed
  have "indep_events_set E ⟹ indep_events F A"
  proof (intro indep_eventsI)
    show "⋀i. indep_events_set E ⟹ i ∈ A ⟹ F i ∈ events" 
      using indep_events_set_events ss by auto
    show "⋀J. indep_events_set E ⟹ J ⊆ A ⟹ finite J ⟹ J ≠ {} ⟹ prob (⋂ (F ` J)) = (∏i∈J. prob (F i))"
      using indep_events_set_probs prob by auto
  qed
  moreover have "indep_events F A ⟹ indep_events_set E"
  proof (intro indep_events_setI) 
    have "⋀e. indep_events F A ⟹ e ∈ E ⟹ e ∈ events" using ss indep_events_def by metis
    then show "indep_events F A ⟹ E ⊆ events" by auto
    show "⋀J. indep_events F A ⟹ J ⊆ E ⟹ finite J ⟹ J ≠ {} ⟹ prob (⋂J) = prod prob J"
      using prob indep_events_def by (metis image_ident) 
  qed
  ultimately show ?thesis by auto
qed

subsection ‹ Mutual Independent Events ›

text ‹Note, set based version only if no duplicates in usage case. The mutual\_indep\_events definition 
is more general and recommended ›
definition mutual_indep_set:: "'a set ⇒ 'a set set ⇒ bool"
  where "mutual_indep_set A S ⟷ A ∈ events ∧ S ⊆ events ∧ (∀ T ⊆ S . T ≠ {} ⟶ prob (A ∩ (⋂T)) = prob A * prob (⋂T))"  
(* Note condition about T not empty, only necessary due to Univ issue*)
(* Use every subset, rather than the not version given by Zhao *)

lemma mutual_indep_setI[intro]: "A ∈ events ⟹ S ⊆ events ⟹ (⋀ T. T ⊆ S ⟹ T ≠ {} ⟹ 
    prob (A ∩ (⋂T)) = prob A * prob (⋂T)) ⟹ mutual_indep_set A S" 
  using mutual_indep_set_def by simp

lemma mutual_indep_setD[dest]: "mutual_indep_set A S ⟹ T ⊆ S ⟹ T ≠ {} ⟹ prob (A ∩ (⋂T)) = prob A * prob (⋂T)"
  using mutual_indep_set_def by simp

lemma mutual_indep_setD2[dest]: "mutual_indep_set A S ⟹ A ∈ events"
  using mutual_indep_set_def by simp

lemma mutual_indep_setD3[dest]: "mutual_indep_set A S ⟹ S ⊆ events"
  using mutual_indep_set_def by simp

lemma mutual_indep_subset: "mutual_indep_set A S ⟹ T ⊆ S ⟹ mutual_indep_set A T"
  using mutual_indep_set_def by auto

lemma mutual_indep_event_set_defD: 
  assumes "mutual_indep_set A S"
  assumes "finite T"
  assumes "T ⊆ S"
  assumes "T ≠ {}"
  shows "indep_event A (⋂T)"
proof (intro indep_eventI)
  show "A ∈ events" using mutual_indep_setD2 assms(1) by auto
  show "⋂ T ∈ events" using Inter_event_ss assms mutual_indep_setD3 finite_subset by blast
  show "prob (A ∩ ⋂ T) = prob A * prob (⋂ T) " 
    using assms(1) mutual_indep_setD assms(3) assms(4) by simp
qed

lemma mutual_indep_event_defI: "A ∈ events ⟹ S ⊆ events ⟹ (⋀ T. T ⊆ S ⟹ T ≠ {} ⟹ 
    indep_event A (⋂T)) ⟹ mutual_indep_set A S"
  using indep_eventD mutual_indep_set_def by simp

lemma mutual_indep_singleton_event: "mutual_indep_set A S ⟹ B ∈ S ⟹ indep_event A B" 
  using mutual_indep_event_set_defD empty_subsetI
  by (metis Set.insert_mono cInf_singleton finite.emptyI finite_insert insert_absorb insert_not_empty) 

lemma mutual_indep_cond: 
  assumes "A ∈ events" and "T ⊆ events" and "finite T"
  and "mutual_indep_set A S" and "T ⊆ S" and "T ≠ {}" and "prob (⋂T) ≠ 0"
shows "𝒫(A |(⋂T)) = prob A"
proof -
  have "⋂T ∈ events" using assms
    by (simp add: Inter_event_ss) 
  then have "𝒫(A | (⋂T)) = prob ((⋂T) ∩ A)/prob(⋂T)"  using cond_prob_ev_def assms(1)
    by blast
  also have "... = prob (A ∩ (⋂T))/prob(⋂T)"
    by (simp add: inf_commute) 
  also have "... = prob A * prob (⋂T)/prob(⋂T)" using assms mutual_indep_setD by auto
  finally show ?thesis using assms(7) by simp
qed

lemma mutual_indep_cond_full: 
  assumes "A ∈ events" and "S ⊆ events" and "finite S"
  and "mutual_indep_set A S" and  "S ≠ {}" and "prob (⋂S) ≠ 0"
shows "𝒫(A |(⋂S)) = prob A"
  using mutual_indep_cond[of A S S] assms by auto

lemma mutual_indep_cond_single: 
  assumes "A ∈ events" and "B ∈ events"
  and "mutual_indep_set A S" and "B ∈ S" and "prob B ≠ 0"
  shows "𝒫(A |B) = prob A"
  using mutual_indep_cond[of "A" "{B}" S] assms by auto

lemma mutual_indep_set_empty: "A ∈ events ⟹ mutual_indep_set A {}"
  using mutual_indep_setI by auto

lemma not_mutual_indep_set_itself: 
  assumes "prob A > 0" and "prob A < 1"
  shows "¬ mutual_indep_set A {A}"
proof (rule ccontr)
  assume "¬ ¬ mutual_indep_set A {A}"
  then have "mutual_indep_set A {A}"
    by simp
  then have "⋀ T . T ⊆ {A} ⟹ T ≠ {} ⟹ prob (A ∩ (⋂ T)) = prob A * prob (⋂T)"
    using mutual_indep_setD by simp
  then have eq: "prob (A ∩ (⋂ {A})) = prob A * prob (⋂{A})"
    by blast 
  have "prob (A ∩ (⋂{A})) = prob A" by simp
  moreover have "prob A * (prob (⋂ {A})) = (prob A)^2"
    by (simp add: power2_eq_square) 
  ultimately show False using eq assms by auto
qed

lemma is_mutual_indep_set_itself:
  assumes "A ∈ events"
  assumes "prob A = 0 ∨ prob A = 1"
  shows "mutual_indep_set A {A}"
proof (intro mutual_indep_setI)
  show "A ∈ events" "{A} ⊆ events" using assms(1) by auto
  fix T assume "T ⊆ {A}" and "T ≠ {}"
  then have teq: "T = {A}" by auto
  have "prob (A ∩ (⋂{A})) = prob A" by simp
  moreover have "prob A * (prob (⋂ {A})) = (prob A)^2"
    by (simp add: power2_eq_square) 
  ultimately show  "prob (A ∩ (⋂ T)) = prob A * prob (⋂T)" using teq assms by auto
qed

lemma mutual_indep_set_singleton: 
  assumes "indep_event A B"
  shows "mutual_indep_set A {B}"
  using indep_eventD_ev1 indep_eventD_ev2 assms 
  by (intro mutual_indep_event_defI) (simp_all add: subset_singleton_iff)

lemma mutual_indep_set_one_compl: 
  assumes "mutual_indep_set A S"
  assumes "finite S"
  assumes "B ∈ S"
  shows "mutual_indep_set A ({space M - B} ∪ S)"
proof (intro mutual_indep_event_defI)
  show "A ∈ events" using assms(1) mutual_indep_setD2 by auto
next
  show "{space M - B} ∪ (S) ⊆ events"
    using assms(1) assms(2) mutual_indep_setD3 assms(3) by blast 
next
  fix T assume jss: "T ⊆ {space M - B} ∪ (S)"
  assume tne: "T ≠ {}"
  let ?T' = "T - {space M - B}"
  show "indep_event A (⋂ T)"
  proof (cases "?T' = {}")
    case True
    then have "T = {space M - B}" using tne by blast
    moreover have "indep_event A B" using assms(1) assms(3) assms(3) mutual_indep_singleton_event by auto
    ultimately show ?thesis using indep_event_one_compl by auto
  next
    case tne2: False
    have finT: "finite T" using jss assms(2) finite_subset by fast
    have tss2: "?T' ⊆ S" using jss assms(2) by auto
    show ?thesis proof (cases "space M - B ∈ T")
      case True
      have "?T' ∪ {B} ⊆ S" using assms(3) tss2 by auto
      then have "indep_event A (⋂(?T' ∪ {B}))" using assms(1) mutual_indep_event_set_defD tne2 finT
        by (meson Un_empty assms(2) finite_subset)
      moreover have "indep_event A (⋂?T')" 
        using assms(1) mutual_indep_event_set_defD finT finite_subset tss2 tne2 by auto
      moreover have "⋂(?T' ∪ {B}) = B ∩ (⋂?T')" by auto
      moreover have "B ∈ events" using assms(3) assms(1) mutual_indep_setD3 by auto
      ultimately have "indep_event A ((space M - B) ∩ (⋂?T'))" using indep_event_compl_inter by auto
      then show ?thesis
        by (metis Inter_insert True insert_Diff) 
    next
      case False
      then have "T ⊆ S" using jss by auto
      then show ?thesis using assms(1) mutual_indep_event_set_defD finT tne by auto
    qed
  qed
qed

lemma mutual_indep_events_set_update_compl: 
  assumes "mutual_indep_set X E"
  assumes "E = A ∪ B"
  assumes "A ∩ B = {}"
  assumes "finite E"
  shows "mutual_indep_set X (((-) (space M) ` A) ∪ B)"
using assms(2) assms(3) proof (induct "card A" arbitrary: A B)
  case 0
  then show ?case using assms(1)
    using assms(4) by auto 
next
  case (Suc x)
  then obtain a A' where aeq: "A = insert a A'" and anotin: "a ∉ A'"
    by (metis card_Suc_eq_finite)
  then have xcard: "card A' = x"
    using Suc(2) Suc(3) assms(4) by auto
  let ?B' = "B ∪ {a}" 
  have "E = A' ∪ ?B'" using aeq Suc.prems by auto
  moreover have "A' ∩ ?B' = {}" using anotin Suc.prems(2) aeq by auto
  ultimately have ies: "mutual_indep_set X ((-) (space M) ` A' ∪ ?B')" 
    using Suc.hyps(1)[of "A'" ?B'] xcard by auto
  then have "a ∈ A ∪ B" using aeq by auto
  then show ?case 
  proof (cases "(A ∪ B) - {a} = {}")
    case True
    then have "A = {a}" "B = {}" using Suc.prems aeq by auto
    moreover have "indep_event X a" using mutual_indep_singleton_event ies by auto
    ultimately show ?thesis using mutual_indep_set_singleton indep_event_one_compl by simp
  next
    case False
    let ?c = "(-) (space M)"
    have un: "?c ` A ∪ B = ?c ` A' ∪ ({?c a}) ∪ (?B' - {a})"
      using Suc(4) aeq by force 
    moreover have "?B' - {a} ⊆ ?B'" by auto
    moreover have "?B' - {a} ⊆ ?c ` A' ∪ {?c a} ∪ (?B')" by auto
    moreover have "?c ` A' ∪ {?c a} ⊆ ?c ` A' ∪ {?c a} ∪ (?B')" by auto
    ultimately have ss: "?c ` A ∪ B ⊆ {?c a} ∪ (?c ` A' ∪ ?B')" 
      using Un_least by auto
    have "a ∈ (-) (space M) ` A' ∪ ?B'" using aeq by auto
    then have ie: "mutual_indep_set X ({?c a} ∪ (?c ` A' ∪ ?B'))" 
      using mutual_indep_set_one_compl[of  X "?c ` A' ∪ ?B'" a] ies ‹E = A' ∪ (B ∪ {a})› assms(4) by blast
    then show ?thesis using mutual_indep_subset ss by auto
  qed
qed

lemma mutual_indep_events_compl: 
  assumes "finite S"
  assumes "mutual_indep_set A S"
  shows "mutual_indep_set A ((λ s . space M - s) ` S)"
  using mutual_indep_events_set_update_compl[of A S S "{}"] assms by auto

lemma mutual_indep_set_all:
  assumes "A ⊆ events"
  assumes "⋀ Ai. Ai ∈ A ⟹ (mutual_indep_set Ai (A - {Ai}))"
  shows "indep_events_set A"
proof (intro indep_events_setI)
  show "A ⊆ events"
    using assms(1) by auto
next
  fix J assume ss: "J ⊆ A" and fin: "finite J" and ne: "J ≠ {}"
  from fin ne ss show "prob (⋂J) = prod prob J"
  proof (induct J rule: finite_ne_induct)
    case (singleton x)
    then show ?case by simp
  next
    case (insert x F)
    then have "mutual_indep_set x (A - {x})" using assms(2) by simp
    moreover have "F ⊆ (A - {x})" using insert.prems insert.hyps by auto
    ultimately have "prob (x ∩ (⋂F)) = prob x * prob (⋂F)"
      by (simp add: local.insert(2) mutual_indep_setD) 
    then show ?case using insert.hyps insert.prems by simp
  qed
qed

text ‹Prefered version using indexed notation ›
definition mutual_indep_events:: "'a set ⇒ (nat ⇒ 'a set) ⇒ nat set ⇒ bool"
  where "mutual_indep_events A F I ⟷ A ∈ events ∧ (F ` I ⊆ events) ∧ (∀ J ⊆ I . J ≠ {} ⟶ prob (A ∩ (⋂j ∈ J . F j)) = prob A * prob (⋂j ∈ J . F j))"
(* Not condition about T not empty, only necessary due to Univ issue?*)
(* Use every subset, rather than the not version given by Zhao, should this include condition re prob *)

lemma mutual_indep_eventsI[intro]: "A ∈ events ⟹ (F ` I ⊆ events) ⟹ (⋀ J. J ⊆ I ⟹ J ≠ {} ⟹ 
    prob (A ∩ (⋂j ∈ J . F j)) = prob A * prob (⋂j ∈ J . F j)) ⟹ mutual_indep_events A F I" 
  using mutual_indep_events_def by simp

lemma mutual_indep_eventsD[dest]: "mutual_indep_events A F I ⟹ J ⊆ I ⟹ J ≠ {} ⟹ prob (A ∩ (⋂j ∈ J . F j)) = prob A * prob (⋂j ∈ J . F j)"
  using mutual_indep_events_def by simp

lemma mutual_indep_eventsD2[dest]: "mutual_indep_events A F I ⟹ A ∈ events"
  using mutual_indep_events_def by simp

lemma mutual_indep_eventsD3[dest]: "mutual_indep_events A F I ⟹ F ` I ⊆ events"
  using mutual_indep_events_def by simp

lemma mutual_indep_ev_subset: "mutual_indep_events A F I ⟹ J ⊆ I ⟹ mutual_indep_events A F J"
  using mutual_indep_events_def by (meson image_mono subset_trans)

lemma mutual_indep_event_defD: 
  assumes "mutual_indep_events A F I"
  assumes "finite J"
  assumes "J ⊆ I"
  assumes "J ≠ {}"
  shows "indep_event A (⋂j ∈ J . F j)"
proof (intro indep_eventI)
  show "A ∈ events" using mutual_indep_setD2 assms(1) by auto
  show "prob (A ∩ ⋂ (F ` J)) = prob A * prob (⋂ (F ` J))" 
    using assms(1) mutual_indep_eventsD assms(3) assms(4) by simp
  have "finite (F ` J)" using finite_subset assms(2) by simp 
  then show "(⋂j ∈ J . F j) ∈ events" 
    using Inter_event_ss[of "F ` J"] assms mutual_indep_eventsD3 by blast
qed

lemma mutual_ev_indep_event_defI: "A ∈ events ⟹ F ` I ⊆ events ⟹ (⋀ J. J ⊆ I ⟹ J ≠ {} ⟹ 
    indep_event A (⋂(F` J))) ⟹ mutual_indep_events A F I"
  using indep_eventD mutual_indep_events_def[of A F I] by auto

lemma mutual_indep_ev_singleton_event: 
  assumes "mutual_indep_events A F I"
  assumes "B ∈ F ` I"
  shows"indep_event A B" 
proof -
  obtain J where beq: "B = F J" and "J ∈ I" using assms(2) by blast
  then have "{J} ⊆ I" and "finite {J}" and "{J} ≠ {}" by auto
  moreover have "B = ⋂ (F ` {J})" using beq by simp
  ultimately show ?thesis using mutual_indep_event_defD assms(1)
    by meson
qed

lemma mutual_indep_ev_singleton_event2: 
  assumes "mutual_indep_events A F I"
  assumes "i ∈ I"
  shows"indep_event A (F i)" 
  using  mutual_indep_event_defD[of A F I "{i}"] assms by auto 

lemma mutual_indep_iff: 
  shows "mutual_indep_events A F I ⟷ mutual_indep_set A (F ` I)"
proof (intro iffI mutual_indep_setI mutual_indep_eventsI)
  show "mutual_indep_events A F I ⟹ A ∈ events" using mutual_indep_eventsD2 by simp
  show "mutual_indep_set A (F ` I) ⟹ A ∈ events" using mutual_indep_setD2 by simp
  show "mutual_indep_events A F I ⟹ F ` I ⊆ events" using mutual_indep_eventsD3 by simp
  show "mutual_indep_set A (F ` I) ⟹ F ` I ⊆ events" using mutual_indep_setD3 by simp
  show "⋀T. mutual_indep_events A F I ⟹ T ⊆ F ` I ⟹ T ≠ {} ⟹ prob (A ∩ ⋂ T) = prob A * prob (⋂ T)"
    using mutual_indep_eventsD by (metis empty_is_image subset_imageE) 
  show "⋀J. mutual_indep_set A (F ` I) ⟹ J ⊆ I ⟹ J ≠ {} ⟹ prob (A ∩ ⋂ (F ` J)) = prob A * prob (⋂ (F ` J))"
    using mutual_indep_setD by (simp add: image_mono) 
qed

lemma mutual_indep_ev_cond: 
  assumes "A ∈ events" and "F ` J ⊆ events" and "finite J"
  and "mutual_indep_events A F I" and "J ⊆ I" and "J ≠ {}" and "prob (⋂(F `J)) ≠ 0"
shows "𝒫(A |(⋂(F ` J))) = prob A"
proof -
  have "⋂(F ` J) ∈ events" using assms
    by (simp add: Inter_event_ss) 
  then have "𝒫(A | (⋂(F ` J))) = prob ((⋂(F ` J)) ∩ A)/prob(⋂(F ` J))" 
    using cond_prob_ev_def assms(1) by blast
  also have "... = prob (A ∩ (⋂(F ` J)))/prob(⋂(F ` J))"
    by (simp add: inf_commute) 
  also have "... = prob A * prob (⋂(F ` J))/prob(⋂(F ` J))" 
    using assms mutual_indep_eventsD by auto
  finally show ?thesis using assms(7) by simp
qed

lemma mutual_indep_ev_cond_full:
  assumes "A ∈ events" and "F ` I ⊆ events" and "finite I"
  and "mutual_indep_events A F I" and  "I ≠ {}" and "prob (⋂(F ` I)) ≠ 0"
shows "𝒫(A |(⋂(F `I))) = prob A"
  using mutual_indep_ev_cond[of A F I I] assms by auto

lemma mutual_indep_ev_cond_single: 
  assumes "A ∈ events" and "B ∈ events"
  and "mutual_indep_events A F I" and "B ∈ F ` I" and "prob B ≠ 0"
shows "𝒫(A |B) = prob A"
proof -
  obtain i where "B = F i" and "i ∈ I" using assms by blast
  then show ?thesis using mutual_indep_ev_cond[of "A" F "{i}" I] assms by auto
qed

lemma mutual_indep_ev_empty: "A ∈ events ⟹ mutual_indep_events A F {}"
  using mutual_indep_eventsI by auto

lemma not_mutual_indep_ev_itself: 
  assumes "prob A > 0" and "prob A < 1" and "A = F i"
  shows "¬ mutual_indep_events A F {i}"
proof (rule ccontr)
  assume "¬ ¬ mutual_indep_events A F {i}"
  then have "mutual_indep_events A F {i}"
    by simp
  then have "⋀ J . J ⊆ {i} ⟹ J ≠ {} ⟹ prob (A ∩ (⋂ (F ` J))) = prob A * prob (⋂(F ` J))"
    using mutual_indep_eventsD by simp
  then have eq: "prob (A ∩ (⋂ (F `{i}))) = prob A * prob (⋂(F ` {i}))"
    by blast 
  have "prob (A ∩ (⋂(F `{i}))) = prob A" using assms(3) by simp
  moreover have "prob A * (prob (⋂ {A})) = (prob A)^2"
    by (simp add: power2_eq_square) 
  ultimately show False using eq assms by auto
qed

lemma is_mutual_indep_ev_itself:
  assumes "A ∈ events" and "A = F i"
  assumes "prob A = 0 ∨ prob A = 1"
  shows "mutual_indep_events A F {i}"
proof (intro mutual_indep_eventsI)
  show "A ∈ events" "F ` {i} ⊆ events" using assms(1) assms(2)  by auto
  fix J assume "J ⊆ {i}" and "J ≠ {}"
  then have teq: "J = {i}" by auto
  have "prob (A ∩ (⋂(F `{i}))) = prob A" using assms(2) by simp
  moreover have "prob A * (prob (⋂ (F `{i}))) = (prob A)^2"
    using assms(2) by (simp add: power2_eq_square) 
  ultimately show  "prob (A ∩ ⋂ (F ` J)) = prob A * prob (⋂ (F ` J))" using teq assms by auto
qed

lemma mutual_indep_ev_singleton: 
  assumes "indep_event A (F i)"
  shows "mutual_indep_events A F {i}"
  using indep_eventD_ev1 indep_eventD_ev2 assms 
  by (intro mutual_ev_indep_event_defI) (simp_all add: subset_singleton_iff)

lemma mutual_indep_ev_one_compl: 
  assumes "mutual_indep_events A F I"
  assumes "finite I"
  assumes "i ∈ I"
  assumes "space M - F i = F j"
  shows "mutual_indep_events A F ({j} ∪  I)"
proof (intro mutual_ev_indep_event_defI)
  show "A ∈ events" using assms(1) mutual_indep_setD2 by auto
next
  show "F ` ({j} ∪ I) ⊆ events"
    using assms(1) assms(2) mutual_indep_eventsD3 assms(3) assms(4)
    by (metis image_insert image_subset_iff insert_is_Un insert_subset sets.compl_sets)  
next
  fix J assume jss: "J ⊆ {j} ∪ I"
  assume tne: "J ≠ {}"
  let ?J' = "J - {j}"
  show "indep_event A (⋂ (F ` J))"
  proof (cases "?J' = {}")
    case True
    then have "J = {j}" using tne by blast
    moreover have "indep_event A (F i)" 
      using assms(1) assms mutual_indep_ev_singleton_event2 by simp
    ultimately show ?thesis using indep_event_one_compl assms(4) by fastforce 
  next
    case tne2: False
    have finT: "finite J" using jss assms(2) finite_subset by fast
    have tss2: "?J' ⊆ I" using jss assms(2) by auto
    show ?thesis proof (cases "j ∈ J")
      case True
      have "?J' ∪ {i} ⊆ I" using assms(3) tss2 by auto
      then have "indep_event A (⋂(F ` ?J' ∪ { F i}))" 
        using assms(1) mutual_indep_event_defD tne2 finT  assms(2) finite_subset
        by (metis Diff_cancel Un_Diff_cancel Un_absorb Un_insert_right image_insert) 
      moreover have "indep_event A (⋂(F ` ?J'))" 
        using assms(1) mutual_indep_event_defD finT finite_subset tss2 tne2 by auto
      moreover have "(⋂(F ` ?J' ∪ { F i})) = F i ∩ (⋂(F ` ?J'))" by auto
      moreover have "F i ∈ events" using assms(3) assms(1) mutual_indep_eventsD3 by simp
      ultimately have "indep_event A (F j ∩ (⋂(F ` ?J')))" 
        using indep_event_compl_inter[of A "⋂(F ` ?J')" "F i"] assms(4) by auto
      then show ?thesis using Inter_insert True insert_Diff by (metis image_insert) 
    next
      case False
      then have "J ⊆ I" using jss by auto
      then show ?thesis using assms(1) mutual_indep_event_defD finT tne by auto
    qed
  qed
qed

lemma mutual_indep_events_update_compl: 
  assumes "mutual_indep_events X F S"
  assumes "S = A ∪ B"
  assumes "A ∩ B = {}"
  assumes "finite S"
  assumes "bij_betw G A A'"
  assumes "⋀ i. i ∈ A ⟹ F (G i) = space M - F i"
  shows "mutual_indep_events X F (A' ∪ B)"
using assms(2) assms(3) assms(6) assms(5) proof (induct "card A" arbitrary: A B A')
  case 0
  then have aempty: "A = {}" using finite_subset assms(4) by simp
  then have "A' = {}" using "0.prems"(4) by (metis all_not_in_conv bij_betwE bij_betw_inv)
  then show ?case using assms(1) using "0.prems"(1) aempty by simp
next
  case (Suc x)
  then obtain a C where aeq: "C = A - {a}" and ain: "a ∈ A"
    by fastforce 
  then have xcard: "card C = x"
    using Suc(2) Suc(3) assms(4) by auto
  let ?C' = "A' - {G a}"
  have compl:  "(⋀i. i ∈ C ⟹ F (G i) = space M - F i)" using Suc.prems aeq by simp
  have bb: "bij_betw G C ?C'" using Suc.prems(4) aeq bij_betw_remove[of G A A' a] ain by simp
  let ?B' = "B ∪ {a}" 
  have "S = C ∪ ?B'" using aeq Suc.prems ain by auto
  moreover have "C ∩ ?B' = {}" using ain Suc.prems(2) aeq by auto
  ultimately have ies: "mutual_indep_events X F (?C' ∪ ?B')" 
    using Suc.hyps(1)[of "C" ?B'] xcard compl bb by auto
  then have "a ∈ A ∪ B" using ain by auto
  then show ?case 
  proof (cases "(A ∪ B) - {a} = {}")
    case True
    then have aeq: "A = {a}" and beq: "B = {}" using Suc.prems ain by auto
    then have "A' = {G a}" using aeq Suc.prems ain aeq bb bij_betwE bij_betw_empty1 insert_Diff
      by (metis Un_Int_eq(4) Un_commute ‹C ∩ (B ∪ {a}) = {}› ‹S = C ∪ (B ∪ {a})›)  
    moreover have "F (G a) = space M - (F a)" using Suc.prems ain by auto
    moreover have "indep_event X (F a)" using mutual_indep_ev_singleton_event ies by auto
    ultimately show ?thesis using mutual_indep_ev_singleton indep_event_one_compl beq by auto
  next
    case False
    have un: "A' ∪ B = ?C' ∪ {G a} ∪ (?B' - {a})" using Suc.prems aeq  
      by (metis Diff_insert_absorb Un_empty_right Un_insert_right ain bij_betwE 
          disjoint_iff_not_equal insert_Diff)
    moreover have "?B' - {a} ⊆ ?B'" by auto
    moreover have "?B' - {a} ⊆ ?C' ∪ {G a} ∪ (?B')" by auto
    moreover have "?C' ∪ {G a} ⊆ ?C' ∪ {G a} ∪ (?B')" by auto
    ultimately have ss: "A' ∪ B ⊆ {G a} ∪ (?C' ∪ ?B')" 
      using Un_least by auto
    have "a ∈ ?C' ∪ ?B'" using aeq by auto
    then have ie: "mutual_indep_events X F ({G a} ∪ (?C' ∪ ?B'))" 
      using mutual_indep_ev_one_compl[of X F "(?C' ∪ ?B')" "a" "G a"] using Suc.prems(3)
      by (metis ‹S = C ∪ (B ∪ {a})› ain assms(4) bb bij_betw_finite ies infinite_Un)  
    then show ?thesis using mutual_indep_ev_subset ss by auto
  qed
qed

lemma mutual_indep_ev_events_compl: 
  assumes "finite S"
  assumes "mutual_indep_events A F S"
  assumes "bij_betw G S S'"
  assumes "⋀ i. i ∈ S ⟹ F (G i) = space M - F i"
  shows "mutual_indep_events A F S'"
  using mutual_indep_events_update_compl[of A F S S "{}"] assms by auto

text ‹Important lemma on relation between independence and mutual independence of a set ›
lemma mutual_indep_ev_set_all:
  assumes "F ` I ⊆ events"
  assumes "⋀ i. i ∈ I ⟹ (mutual_indep_events (F i) F (I - {i}))"
  shows "indep_events F I"
proof (intro indep_eventsI)
  show "⋀i. i ∈ I ⟹ F i ∈ events"
    using assms(1) by auto
next
  fix J assume ss: "J ⊆ I" and fin: "finite J" and ne: "J ≠ {}"
  from fin ne ss show "prob (⋂ (F ` J)) = (∏i∈J. prob (F i))"
  proof (induct J rule: finite_ne_induct)
    case (singleton x)
    then show ?case by simp
  next
    case (insert x X)
    then have "mutual_indep_events (F x) F (I - {x})" using assms(2) by simp
    moreover have "X ⊆ (I - {x})" using insert.prems insert.hyps by auto
    ultimately have "prob (F x ∩ (⋂(F `X))) = prob (F x) * prob (⋂(F ` X))"
      by (simp add: local.insert(2) mutual_indep_eventsD) 
    then show ?case using insert.hyps insert.prems by simp
  qed
qed

end
end