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 (jJ. A j) = (jJ. 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 (iJ. case i of True  A | False  B) = 
      (iJ. 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) = (iJ. prob i)))"

lemma indep_events_setI[intro]: "E  events  (J. J  E  finite J  J  {}  
    prob (J) = (iJ. prob i))  indep_events_set E"
  using indep_events_set_def by simp

lemma indep_events_subset:
  "indep_events_set E  (JE. 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) = (iJ. 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 (iJ. 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 (iJ. 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  (JE. 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)) = (iJ. prob (F i))" 
  unfolding indep_events_def by auto

lemma indep_events_prod_all: "indep_events F E  finite E  E  {}  prob ((F ` E)) = (iE. 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)) = (iJ. 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))) = (iA  B. prob (F i))" using assms
    using  indep_events_probs[of F S "A  B"] by simp
  also have "... = (iA. prob (F i)) * (iB. 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 "(iJ. prob (F i)) = (iJ. prob (G i))" using calculation(5) by auto
  ultimately show "prob ( (G ` J)) = (iJ. 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 (iJ. ?G i) = (iJ. 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 (iJ. G i) = (iJ. 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)) = (iI. 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 (iJ. i) = (iJ. prob i)) 
        ( I. I  A  finite I  I  {}  prob (iI. F i) = (iI. prob (F i)))"
  proof (intro allI impI iffI)
    fix I assume p1: " JE. finite J  J  {}  prob (iJ. 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)) = (iI. prob (F i))" using bij_betw_prod_prob
      by (metis jeq)  
  next
    fix J assume p2: "IA. finite I  I  {}  prob ( (F ` I)) = (iI. 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)) = (iI. 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 (iJ. 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)) = (iJ. 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)) = (iJ. 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