Theory Lovasz_Local_Lemma

(* Theory: Lovasz_Local_Lemma
   Author: Chelsea Edmonds *)

section ‹Lovasz Local Lemma ›

theory Lovasz_Local_Lemma 
  imports 
    Basic_Method 
    "HOL-Real_Asymp.Real_Asymp" 
    Indep_Events
    Digraph_Extensions
begin

subsection ‹Random Lemmas on Product Operator ›

lemma prod_constant_ge: 
  fixes y :: "'b :: {comm_monoid_mult, linordered_semidom}"
  assumes "card A  k"
  assumes "y  0" and "y < 1"
  shows "(xA. y)  y ^ k"
  using assms power_decreasing by fastforce

lemma (in linordered_idom) prod_mono3:
  assumes "finite J" "I  J" "i. i  J  0  f i"  "(i. i  J  f i  1)"
  shows "prod f J  prod f I"
proof -
  have "prod f J  (iJ. if i  I then f i else 1)"
    using assms by (intro prod_mono) auto
  also have " = prod f I"
    using finite J I  J by (simp add: prod.If_cases Int_absorb1)
  finally show ?thesis .
qed

lemma bij_on_ss_image: 
  assumes "A  B"
  assumes "bij_betw g B B'"
  shows "g ` A  B'"
  using assms by (auto simp add: bij_betw_apply subsetD)

lemma bij_on_ss_proper_image: 
  assumes "A  B"
  assumes "bij_betw g B B'"
  shows "g ` A  B'"
  by (smt (verit, ccfv_SIG) assms bij_betw_iff_bijections bij_betw_subset leD psubsetD psubsetI subsetI)


subsection ‹Dependency Graph Concept ›

text ‹Uses directed graphs. The pair\_digraph locale was sufficient as multi-edges are irrelevant ›

locale dependency_digraph = pair_digraph "G :: nat pair_pre_digraph" + prob_space "M :: 'a measure" 
  for G M + fixes F :: "nat  'a set"
  assumes vss: "F ` (pverts G)  events"
  assumes mis: " i. i  (pverts G)  mutual_indep_events (F i) F ((pverts G) - ({i}  neighborhood i))" 
begin

lemma dep_graph_indiv_nh_indep: 
  assumes "A  pverts G" "B  pverts G"
  assumes "B  neighborhood A"
  assumes "A  B"
  assumes "prob (F B)  0"
  shows "𝒫((F A) | (F B)) = prob (F A)"
proof-
  have "B  {A}  neighborhood A" using assms(3) assms(4) by auto
  then have "B  (pverts G - ({A}  neighborhood A))" using assms(2) by auto
  moreover have "mutual_indep_events (F A) F (pverts G - ({A}  neighborhood A))" using mis assms by auto
  ultimately show ?thesis using 
      assms(5) assms(1) assms(2) vss mutual_indep_ev_cond_single by auto
qed

lemma mis_subset: 
  assumes "i  pverts G"
  assumes "A  pverts G"
  shows "mutual_indep_events (F i) F (A - ({i}  neighborhood i))"
proof (cases "A  ({i}  neighborhood i)")
  case True
  then have "A - ({i}  neighborhood i) = {}" by auto
  then show ?thesis using mutual_indep_ev_empty vss assms(1) by blast
next
  case False
  then have "A - ({i}  neighborhood i)  pverts G - ({i}  neighborhood i)" using assms(2) by auto
  then show ?thesis using mutual_indep_ev_subset mis assms(1) by blast
qed

lemma dep_graph_indep_events:
  assumes "A  pverts G"
  assumes " Ai. Ai  A  out_degree G Ai = 0"
  shows "indep_events F A"
proof -
  have " Ai. Ai  A  (mutual_indep_events (F Ai) F (A - {Ai}))"
  proof -
    fix Ai assume ain: "Ai  A"
    then have "(neighborhood Ai) = {}" using assms(2) neighborhood_empty_iff by simp
    moreover have "mutual_indep_events (F Ai) F (A - ({Ai}  neighborhood Ai))" 
      using mis_subset[of Ai A] ain assms(1) by auto
    ultimately show "mutual_indep_events (F Ai) F (A - {Ai})" by simp
  qed
  then show ?thesis using mutual_indep_ev_set_all[of F A] vss by auto 
qed

end

subsection ‹Lovasz Local General Lemma ›
context prob_space
begin

lemma compl_sets_index: 
  assumes "F ` A  events"
  shows "(λ i. space M - F i) ` A  events"
proof (intro subsetI)
  fix x assume "x  (λi. space M - F i) ` A"
  then obtain i where xeq: "x = space M - F i" and "i  A" by blast
  then have "F i  events" using assms by auto
  thus "x  events" using sets.compl_sets xeq by simp
qed

lemma lovasz_inductive_base: 
  assumes "dependency_digraph G M F"
  assumes " Ai . Ai  A  g Ai  0  g Ai < 1"
  assumes " Ai.  Ai  A  (prob (F Ai)  (g Ai) * ( Aj  pre_digraph.neighborhood G Ai. (1 - (g Aj))))"
  assumes "Ai  A"
  assumes "pverts G = A"
  shows "prob (F Ai)  g Ai"
proof -
  have genprod: " S. S  A  (Aj  S . (1 - (g Aj)))  1" using assms(2)
    by (smt (verit) prod_le_1 subsetD) 
  interpret dg: dependency_digraph G M F using assms(1) by simp
  have "dg.neighborhood Ai  A" using assms(3) dg.neighborhood_wf assms(5) by simp
  then  show ?thesis 
    using genprod assms mult_left_le by (smt (verit)) 
qed

lemma lovasz_inductive_base_set: 
  assumes "N  A"
  assumes " Ai . Ai  A  g Ai  0  g Ai < 1"
  assumes " Ai.  Ai  A  (prob (F Ai)  (g Ai) * ( Aj  N. (1 - (g Aj))))"
  assumes "Ai  A"
  shows "prob (F Ai)  g Ai"
proof -
  have genprod: " S. S  A  (Aj  S . (1 - (g Aj)))  1" using assms(2)
    by (smt (verit) prod_le_1 subsetD) 
  then  show ?thesis 
    using genprod assms mult_left_le by (smt (verit)) 
qed

lemma split_prob_lt_helper:
  assumes dep_graph: "dependency_digraph G M F"
  assumes dep_graph_verts: "pverts G = A"
  assumes fbounds: " i . i  A  f i  0  f i < 1"
  assumes prob_Ai: " Ai.  Ai  A  prob (F Ai)  
    (f Ai) * ( Aj  pre_digraph.neighborhood G Ai . (1 - (f Aj)))"
  assumes aiin: "Ai  A"
  assumes "N  pre_digraph.neighborhood G Ai"
  assumes " P1 P2. 𝒫(F Ai | AjS. space M - F Aj) = P1/P2  
    P1  prob (F Ai) P2  ( Aj  N . (1 - (f Aj)))"
  shows "𝒫(F Ai | AjS. space M - F Aj)  f Ai"
proof -
  interpret dg: dependency_digraph G M F using assms(1) by simp
  have lt1: " Aj. Aj  A   (1 - (f Aj))  1"
    using assms(3) by auto
  have gt0: " Aj. Aj  A  (1 - (f Aj)) > 0" using assms(3) by auto
  then have prodgt0: " S'. S'  A   ( Aj  S' . (1 - f Aj)) > 0"
    using prod_pos by (metis subsetD) 
  obtain P1 P2 where peq: "𝒫(F Ai | AjS. space M - F Aj) = P1/P2" and  
   "P1  prob (F Ai)"
    and p2gt: "P2  ( Aj  N . (1 - (f Aj)))" using assms(7) by auto
  then have "P1  (f Ai) * ( Aj  pre_digraph.neighborhood G Ai . (1 - (f Aj)))" 
    using prob_Ai aiin by fastforce
  moreover have "P2  ( Aj  dg.neighborhood Ai . (1 - (f Aj)))" using assms(6) 
      gt0 dg.neighborhood_wf dep_graph_verts subset_iff lt1 dg.neighborhood_finite p2gt
    by (smt (verit, ccfv_threshold) prod_mono3) 
  ultimately have "P1/P2  ((f Ai) * ( Aj  dg.neighborhood Ai . (1 - (f Aj)))/( Aj  dg.neighborhood Ai . (1 - (f Aj))))"
    using frac_le[of "(f Ai) * ( Aj  dg.neighborhood Ai . (1 - (f Aj)))" "P1" "( Aj  dg.neighborhood Ai . (1 - (f Aj)))"] 
      prodgt0[of "dg.neighborhood Ai"] assms(3) dg.neighborhood_wf[of Ai]
    by (simp add: assms(2) bounded_measure finite_measure_compl assms(5))
  then show ?thesis using prodgt0[of "dg.neighborhood Ai"] dg.neighborhood_wf[of Ai] assms(2) peq
    by (metis divide_eq_imp rel_simps(70)) 
qed

lemma lovasz_inequality: 
  assumes finS: "finite S"
  assumes sevents: "F ` S  events"
  assumes S_subset: "S  A - {Ai}"
  assumes prob2: "prob ( Aj  S . (space M - (F Aj))) > 0"
  assumes irange: "i  {0..<card S1}"
  assumes bb: "bij_betw g {0..<card S1} S1"
  assumes s1_def: "S1 = (S  N)"
  assumes s2_def: "S2 = S - S1"
  assumes ne_cond: "i > 0  S2  {}"
  assumes hyps: " B. B  S  g i  A  B  A - {g i}  B  {}  
    0 < prob (AjB. space M - F Aj)  𝒫(F (g i) | AjB. space M - F Aj)  f (g i)"
  shows "𝒫((space M - F (g i)) | ( ((λ i. space M - F i) ` g ` {0..<i}  ((λ i. space M - F i) ` S2)))) 
     (1 - f (g i))"
proof -
  let ?c = "(λ i. space M - F i)"
  define S1ss where "S1ss = g ` {0..<i}" 
  have "i  {0..<i}" by simp
  moreover have "{0..<i}  {0..<card S1}" using irange by simp
  ultimately have ginotin1: "g i  S1ss" using bb S1ss_def irange
    by (smt (verit, best) bij_betw_iff_bijections image_iff subset_eq) 
  have ginotin2: "g i  S2" unfolding s2_def using irange bb by (simp add: bij_betwE) 
  have giS: "g i  S" using irange bij_betw_imp_surj_on imageI Int_iff s1_def bb 
    by blast
  have "{0..<i}  {0..<card S1}" using irange by auto
  then have "S1ss  S1" unfolding S1ss_def using irange bb bij_on_ss_proper_image by meson
  then have sss: "S1ss  S2  S" using s1_def s2_def by blast 
  moreover have xsiin: "g i  A"using irange  
    using giS S_subset by (metis DiffE in_mono)
  moreover have ne: "S1ss  S2  {}" using ne_cond S1ss_def by auto
  moreover have "S1ss  S2  A - {g i}"  using S_subset sss ginotin1 ginotin2 by auto
  moreover have gt02: "0 < prob ( (?c ` (S1ss  S2)))" using finS prob2 sevents
    prob_inter_ss_lt_index[of S ?c "S1ss  S2"] ne sss compl_sets_index[of F S]  by fastforce
  ultimately have ltfAi: "𝒫(F (g i) |  (?c ` (S1ss  S2)))  f (g i)"
    using hyps[of "S1ss  S2"] by blast 
  have "?c ` (S1ss  S2)  events" using sss S1ss  S1 compl_subset_in_events sevents s1_def s2_def
    by fastforce
  then have " (?c ` (S1ss  S2))  events" using Inter_event_ss sss
    by (meson S1ss  S2  {} finite_imageI finite_subset image_is_empty finS subset_iff_psubset_eq)
  moreover have "F (g i)  events" using xsiin giS sevents by auto
  ultimately have "𝒫(?c (g i) |  (?c ` (S1ss  S2)))  1 - f (g i)" 
    using cond_prob_neg[of " (?c ` (S1ss  S2))" "F (g i)"] gt02 xsiin ltfAi by simp
  then show "𝒫(?c (g i) | ( (?c ` g ` {0..<i}  (?c ` S2))))  (1 - f (g i))"
    by (simp add: S1ss_def image_Un)
qed

text ‹The main helper lemma ›
lemma lovasz_inductive: 
  assumes finA: "finite A"
  assumes Aevents: "F ` A  events"
  assumes fbounds: " i . i  A  f i  0  f i < 1"
  assumes dep_graph: "dependency_digraph G M F"
  assumes dep_graph_verts: "pverts G = A"
  assumes prob_Ai: " Ai.  Ai  A  prob (F Ai)  
    (f Ai) * ( Aj  pre_digraph.neighborhood G Ai . (1 - (f Aj)))"
  assumes Ai_in: "Ai  A"
  assumes S_subset: "S  A - {Ai}"
  assumes S_nempty: "S  {}"
  assumes prob2: "prob ( Aj  S . (space M - (F Aj))) > 0"
  shows "𝒫((F Ai) | ( Aj  S . (space M - (F Aj))))  f Ai"
proof -
  let ?c = "λ i. space M - F i"
  have ceq: " A. ?c ` A = ((-) (space M)) ` (F ` A)"  by auto
  interpret dg: dependency_digraph G M F using assms(4) by simp
  have finS: "finite S" using assms finite_subset by (metis finite_Diff) 
  show "𝒫(( F Ai) | ( Aj  S . (space M - (F Aj))))  f Ai" 
    using finS Ai_in S_subset S_nempty prob2
  proof (induct S arbitrary: Ai rule: finite_psubset_induct )
    case (psubset S)
    define S1 where "S1 = (S  dg.neighborhood Ai)"
    define S2 where "S2 = S - S1"
    have " s . s  S2  s  A - ({Ai}  dg.neighborhood Ai)" 
      using S1_def S2_def psubset.prems(2) by blast 
    then have s2ssmis: "S2  A - ({Ai}  dg.neighborhood Ai)" by auto
    have sevents: "F ` S  events" using assms(2) psubset.prems(2) by auto
    then have s1events: "F ` S1  events" using S1_def by auto
    have finS2: "finite S2" and finS1: "finite S1" using S2_def S1_def by (simp_all add: psubset(1))
    have "mutual_indep_set (F Ai) (F ` S2)" using dg.mis[of Ai] mutual_indep_ev_subset s2ssmis 
      psubset.prems(1) dep_graph_verts mutual_indep_iff by auto
    then have mis2: "mutual_indep_set (F Ai) (?c ` S2)" 
      using mutual_indep_events_compl[of "F ` S2" "F Ai"] finS2 ceq[of S2] by simp
    have scompl_ev: "?c ` S  events"
      using compl_sets_index sevents by simp
    then have s2cev: "?c ` S2  events" using S2_def scompl_ev by blast
    have "( Aj  S . space M - (F Aj))  ( Aj  S2 . space M - (F Aj))"
      unfolding S2_def using Diff_subset image_mono Inter_anti_mono by blast
    then have "S2  {}  prob ( Aj  S2 . space M - (F Aj))  0" using psubset.prems(4) s2cev 
      finS2 Inter_event_ss[of "?c ` S2"] finite_measure_mono[of " (?c ` S)" "(?c ` S2)"] by simp
    then have s2prob_eq: "S2  {}  𝒫((F Ai) | ( (?c ` S2))) = prob (F Ai)" using assms(2)
      mutual_indep_cond_full[of " F Ai" "?c ` S2"]  psubset.prems(1) s2cev finS2 mis2 by simp
    show ?case 
    proof (cases "S1 = {}")
      case True
      then show ?thesis using lovasz_inductive_base[of G F A f Ai]  psubset.prems(3) S2_def
          assms(3) assms(4) psubset.prems(1) prob_Ai s2prob_eq dep_graph_verts by (simp) 
    next
      case s1F: False
      then have csgt0: "card S1 > 0" using s1F finS1 card_gt_0_iff by blast
      obtain g where bb: "bij_betw g {0..<card S1} S1" using finS1 ex_bij_betw_nat_finite by auto
      have igt0: "i. i  {0..<card S1}  1 - f (g i)  0"
        using S1_def psubset.prems(2) bb bij_betw_apply assms(3) by fastforce
      have s1ss: "S1  dg.neighborhood Ai" using S1_def by auto
      moreover have " P1 P2. 𝒫(F Ai | AjS. space M - F Aj) = P1/P2   P1  prob (F Ai) 
         P2  ( Aj  S1 . (1 - (f Aj)))"
      proof (cases "S2 = {}")
        case True
        then have Seq: "S1 = S" using S1_def S2_def by auto
        have inter_eventsS: "( Aj  S . (space M - (F Aj)))  events" using  psubset.prems assms
          by (meson measure_notin_sets zero_less_measure_iff)
        then have peq: "𝒫((F Ai) | ( Aj  S1 . ?c Aj)) = 
            prob (( Aj  S1 . ?c Aj)  (F Ai))/prob (( (?c ` S1)))" 
            (is "𝒫((F Ai) | ( Aj  S1 . ?c Aj)) = ?Num/?Den")
          using cond_prob_ev_def[of "( Aj  S1 . (space M - (F Aj)))" "F Ai"] 
          using Seq psubset.prems(1) assms(2) by blast
        have "?Num  prob (F Ai)" using finite_measure_mono assms(2) psubset.prems(1) by simp
        moreover have "?Den  ( Aj  S1 . (1 - (f Aj)))"
        proof -
          have pcond: "prob ((?c ` S1)) = 
              prob (?c (g 0)) * (i  {1..<card S1} . 𝒫(?c (g i) | ((?c ` g ` {0..<i}))))"
            using prob_cond_inter_index_fn_compl[of "S1" F] Seq s1events psubset(1) s1F bb by auto
          have ineq: " i. i  {1..<card S1}  𝒫(?c (g i) | ((?c ` g ` {0..<i})))  (1 - (f (g i)))" 
            using lovasz_inequality[of S1 F A Ai _ S1 g S1 "{}" f] sevents finS psubset.prems(2) 
              psubset.prems(4)  bb psubset.hyps(2)[of _ "g _"] Seq by fastforce
          have "(i. i  {1..<card S1}  1 - f (g i)  0)" using igt0 by simp
          then have "(i  {1..<(card S1)} . 𝒫(?c (g i) | ((?c ` g ` {0..<i})))) 
             (i  {1..<(card S1)} . (1 - (f (g i))))" 
            using ineq prod_mono by (smt(verit, ccfv_threshold))
          moreover have "prob (?c (g 0))  (1 - f (g 0))" 
          proof -
            have g0in: "g 0  A" using bb csgt0 using psubset.prems(2) bij_betwE Seq by fastforce
            then have "prob (?c (g 0)) = 1 - prob (F (g 0))" using Aevents by (simp add: prob_compl) 
            then show ?thesis using lovasz_inductive_base[of G F A f "g 0"] 
                prob_Ai assms(4) dep_graph_verts fbounds g0in by auto
          qed
          moreover have "0  (i = 1..<card S1. 1 - f (g i))" using igt0 by (force intro: prod_nonneg) 
          ultimately have  "prob ((?c ` S1))  (1 - (f (g 0))) * (i  {1..<(card S1)} . (1 - (f (g i))))" 
            using pcond igt0 mult_mono'[of "(1 - (f (g 0)))" ] by fastforce
          moreover have "{0..<card S1} = {0}  {1..<card S1}" using csgt0 by auto
          ultimately have "prob ((?c ` S1))  (i  {0..<(card S1)} . (1 - (f (g i))))" by auto     
          moreover have "(i  {0..<(card S1)} . (1 - (f (g i)))) = (i  S1 . (1 - (f (i))))" 
            using prod.reindex_bij_betw bb by simp
          ultimately show ?thesis by simp
        qed
        ultimately show ?thesis using peq Seq by blast 
      next
        case s2F: False
        have s2inter: " (?c ` S2)  events" 
          using s2F finS2 s2cev Inter_event_ss[of "?c ` S2"]  by auto
        have split: "( Aj  S . (?c Aj)) = ( (?c `S1))  ( (?c ` S2))" 
          using S1_def S2_def by auto
        then have "𝒫(F Ai | ( Aj  S . (?c Aj))) = 𝒫(F Ai | ( (?c `S1))  ( (?c ` S2)))" by simp
        moreover have s2n0: "prob ( (?c ` S2))  0" using psubset.prems(4) S2_def
          by (metis Int_lower2 split finite_measure_mono measure_le_0_iff s2inter semiring_norm(137)) 
        moreover have " (?c ` S1)  events" 
          using finS1 S1_def scompl_ev s1F Inter_event_ss[of "(?c ` S1)"] by auto
        ultimately have peq: "𝒫(F Ai | ( Aj  S . (?c Aj))) = 𝒫(F Ai  ( (?c `S1)) |  (?c ` S2))/ 
          𝒫( (?c `S1) |  (?c `S2))" (is "𝒫(F Ai | ( Aj  S . (?c Aj))) = ?Num/?Den")
          using cond_prob_dual_intersect[of "F Ai" " (?c `S1)" " (?c `S2)"]  assms(2) 
            psubset.prems(1) s2inter by fastforce
        have "?Num  𝒫(F Ai |  (?c `S2))" using cond_prob_inter_set_lt[of "F Ai" " (?c `S2)" "?c ` S1"]
          using s1events finS1 psubset.prems(1) assms(2) s2inter finite_imageI[of S1 F] by blast
        then have "?Num  prob (F Ai)" using s2F s2prob_eq by auto
        moreover have "?Den  ( Aj  S1 . (1 - (f Aj)))"  using psubset.hyps
        proof -
          have "prob ((?c ` S2)) > 0" using s2n0 by (meson zero_less_measure_iff) 
          then have pcond: "𝒫( (?c `S1) |  (?c `S2)) = 
              (i = 0..<card S1 . 𝒫(?c (g i) | ( (?c ` g ` {0..<i}  (?c ` S2)))))"
            using prob_cond_Inter_index_cond_compl_fn[of S1 "?c ` S2" F] s1F finS1 s2cev finS2 s2F 
              s1events bb by auto  
          have  " i. i  {0..<card S1}  𝒫(?c (g i) | ( (?c ` g ` {0..<i}  (?c ` S2))))  (1 - f (g i))"
            using lovasz_inequality[of S F A Ai _ S1 g "dg.neighborhood Ai" S2 f] S1_def S2_def sevents 
              finS psubset.prems(2) psubset.prems(4)  bb psubset.hyps(2)[of _ "g _"] psubset(1) s2F by meson
          then have c1: "𝒫( (?c `S1) |  (?c `S2))  (i = 0..<card S1 . (1 - f (g i)))" 
            using prod_mono igt0 pcond bb  by (smt(verit, ccfv_threshold))
          then have "𝒫( (?c `S1) |  (?c `S2))  (i  {0..<card S1} . (1 - f (g i)))" by blast
          moreover have "(i  {0..<card S1} . (1 - f (g i))) = (x  S1 . (1 - f x))" using bb
            using prod.reindex_bij_betw by fastforce 
          ultimately show ?thesis by simp
        qed 
        ultimately show ?thesis using peq by blast
      qed
      ultimately show ?thesis  by (intro split_prob_lt_helper[of G F A])
        (simp_all add: dep_graph dep_graph_verts fbounds psubset.prems(1) prob_Ai)
    qed
  qed
qed

text ‹The main lemma ›
theorem lovasz_local_general: 
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai . Ai  A   f Ai  0  f Ai < 1"
  assumes "dependency_digraph G M F"
  assumes " Ai.  Ai  A  (prob (F Ai)  (f Ai) * ( Aj  pre_digraph.neighborhood G Ai. (1 - (f Aj))))"
  assumes "pverts G = A"
  shows "prob ( Ai  A . (space M - (F Ai)))  ( Ai  A . (1 - f Ai))" "( Ai  A . (1 - f Ai)) > 0"
proof -
  show gt0: "( Ai  A . (1 - f Ai)) > 0" using assms(4) by (simp add: prod_pos)
  let ?c = "λ i. space M - F i"
  interpret dg: dependency_digraph G M F using assms(5) by simp
  have general: "Ai S. Ai  A  S  A - {Ai}  S  {}   prob ( Aj  S . (?c Aj)) > 0 
      𝒫(F Ai | ( Aj  S . (?c Aj)))  f Ai" 
    using assms lovasz_inductive[of A F f G] by simp
  have base: " Ai. Ai  A  prob (F Ai)  f Ai"
    using lovasz_inductive_base assms(4) assms(6) assms(5) assms(7) by blast
  show "prob ( Ai  A . (?c Ai))  ( Ai  A . (1 - f Ai))"
    using assms(3) assms(1) assms(2) assms(4) general base
  proof (induct A rule: finite_ne_induct)
    case (singleton x)
    then show ?case using singleton.prems singleton prob_compl by auto
  next
    case (insert x X)
    define Ax where "Ax = ?c ` (insert x X)"
    have xie: "F x  events" using insert.prems by simp
    have A'ie: "(?c ` X)  events" using insert.prems insert.hyps by auto
    have "(Ai S. Ai  insert x X  S  insert x X - {Ai}  S  {}  prob ( Aj  S . (?c Aj)) > 0 
       𝒫(F Ai |  (?c ` S))  f Ai)" using insert.prems by simp
    then have  "(Ai S. Ai  X  S  X - {Ai}  S  {}   prob ( Aj  S . (?c Aj)) > 0 
       𝒫(F Ai |  (?c ` S))  f Ai)" by auto
    then have A'gt: "(AiX. 1 - f Ai)  prob ( (?c ` X))"
      using insert.hyps(4) insert.prems(2) insert.prems(1) insert.prems(4) by auto
    then have "prob ((?c ` X)) > 0" using insert.hyps insert.prems prod_pos basic_trans_rules(22) 
      diff_gt_0_iff_gt by (metis (no_types, lifting) insert_Diff insert_subset subset_insertI) 
    then have "𝒫((?c x) | ((?c ` X))) = 1 - 𝒫(F x | ((?c ` X)))" 
      using cond_prob_neg[of "(?c ` X)" "F x"] xie A'ie by simp
    moreover have "𝒫(F x | ((?c ` X)))  f x" using insert.prems(3)[of x X]  insert.hyps(2) insert(3) 
        A'gt 0 < prob ( (?c ` X)) by fastforce
    ultimately have pnxgt: "𝒫((?c x) | ((?c ` X)))  1 - f x" by simp
    have xgt0: "1 - f x  0" using insert.prems(2)[of x] by auto
    have "prob ( Ax) = prob ((?c x)  (?c ` X))" using Ax_def by simp
    also have "... = prob ((?c ` X)) * 𝒫((?c x) | ((?c ` X)))" 
      using prob_intersect_B xie A'ie by simp
    also have "...  (AiX. 1 - f Ai) * (1 - f x)" using A'gt pnxgt mult_left_le 
        0 < prob ((?c ` X)) xgt0 mult_mono by (smt(verit))
    finally have "prob ( Ax)  (Aiinsert x X. 1 - f Ai)"
      by (simp add: local.insert(1) local.insert(3) mult.commute) 
    then show ?case using Ax_def by auto
  qed
qed

subsection ‹Lovasz Corollaries and Variations ›

corollary lovasz_local_general_positive: 
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai . Ai  A   f Ai  0  f Ai < 1"
  assumes "dependency_digraph G M F"
  assumes " Ai.  Ai  A  (prob (F Ai)  
    (f Ai) * ( Aj  pre_digraph.neighborhood G Ai. (1 - (f Aj))))"
  assumes "pverts G = A"
  shows "prob ( Ai  A . (space M - (F Ai))) > 0"
  using assms lovasz_local_general(1)[of A F f G] lovasz_local_general(2)[of A F f G] by simp

theorem lovasz_local_symmetric_dep_graph: 
  fixes e :: real
  fixes d :: nat
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes "dependency_digraph G M F"
  assumes " Ai.  Ai  A  out_degree G Ai  d" 
  assumes " Ai. Ai  A  prob (F Ai)  p"
  assumes "exp(1)* p * (d + 1)  1" (* e should be euler's number ⇒ using exponential function? *)
  assumes "pverts G = A"
  shows "prob ( Ai  A . (space M - (F Ai))) > 0"
proof (cases "d = 0")
  case True
  interpret g: dependency_digraph G M F using assms(4) by simp
  (* Because all have mutual independence ⟹ complete independence *)
  have "indep_events F A" using g.dep_graph_indep_events[of A] assms(8) assms(5) True by simp
  moreover have "p < 1" 
  proof -
    have "exp (1) * p  1" using assms(7) True by simp
    then show ?thesis using exp_gt_one  less_1_mult linorder_neqE_linordered_idom rel_simps(68) 
      verit_prod_simplify(2) by (smt (verit) mult_le_cancel_left1)
  qed
  ultimately show ?thesis 
    using complete_indep_bound3[of A F] assms(2) assms(1) assms(3) assms(6) by force
next
  case False
  define f :: "nat  real" where "f  (λ Ai . 1 /(d + 1))"
  then have fbounds: " Ai. f Ai  0  f Ai < 1" using f_def False by simp
  interpret dg: dependency_digraph G M F using assms(4) by auto
(* Showing bound is the most work *)
  have " Ai. Ai  A  prob (F Ai)  (f Ai) * ( Aj  dg.neighborhood Ai . (1 - (f Aj)))"
  proof -
    fix Ai assume ain: "Ai  A"
    have d_boundslt1: "(1/(d + 1)) < 1" and d_boundsgt0: "(1/(d + 1))> 0" using False by fastforce+ 
    have d_bounds2: "(1 - (1 /(d + 1)))^d < 1" using False 
      by(simp add: field_simps) (smt (verit) of_nat_0_le_iff power_mono_iff)
    have d_bounds0: "(1 - (1 /(d + 1)))^d > 0" using False by (simp)
    have "exp(1) > (1 + 1/d) powr d" using exp_1_gt_powr False by simp
    then have "exp(1) > (1 + 1/d)^d" using False by (simp add: powr_realpow zero_compare_simps(2))
    moreover have "1/(1+ 1/d)^d = (1 - (1/(d+1)))^d"
    proof -
      have "1/(1+ 1/d)^d = 1/((d/d) + 1/d)^d" by (simp add: field_simps)
      then show ?thesis by (simp add: field_simps)
    qed
    ultimately have exp_lt: "1/exp(1) < (1 - (1 /(d + 1)))^d"
      by (metis d_bounds0 frac_less2 less_eq_real_def of_nat_zero_less_power_iff power_eq_if zero_less_divide_1_iff) 
    then have "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > (1 /(d + 1))*(1/exp(1))"
      using exp_lt mult_strict_left_mono[of "1/exp(1)" "(1 - (1 /(d + 1)))^d" "(1/(d+1))"] d_boundslt1 
      by simp
    then have "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > (1/((d+1)*exp(1)))" by auto 
    then have gtp: "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > p"
      by (smt (verit, ccfv_SIG) d_boundslt1 d_boundsgt0 assms(7) divide_divide_eq_left divide_less_cancel 
          divide_less_eq divide_nonneg_nonpos nonzero_mult_div_cancel_left not_exp_le_zero) 
    have "card (dg.neighborhood Ai)  d" using assms(5) dg.out_degree_neighborhood ain by auto
    then have "( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1))))  (1 - (1 /(d + 1)))^d"
      using prod_constant_ge[of  "dg.neighborhood Ai" "d" "1 - (1/d+1)"] using d_boundslt1 by auto
    then have "(1 /(d + 1)) * ( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1))))  (1 /(d + 1))* (1 - (1 /(d + 1)))^d"
      by (simp add: divide_right_mono) 
    then have "(1 /(d + 1)) * ( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1)))) > p" 
      using gtp by simp
    then show "prob (F Ai)  f Ai * ( Aj  dg.neighborhood Ai . (1 - f Aj))"
      using assms(6) Ai  A f_def by force 
  qed
  then show ?thesis using lovasz_local_general_positive[of A F f G] 
      assms(4) assms(1) assms(2) assms(3) assms(8) fbounds by auto
qed

corollary lovasz_local_symmetric4gt: 
  fixes e :: real
  fixes d :: nat
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes "dependency_digraph G M F"
  assumes " Ai.  Ai  A  out_degree G Ai  d" 
  assumes " Ai. Ai  A  prob (F Ai)  p"
  assumes "4 * p * d  1" (* only works if d \ge 3 *)
  assumes "d  3"
  assumes "pverts G = A"
  shows "prob ( Ai  A . (space M - F Ai)) > 0"
proof -
  have "exp(1)* p * (d + 1)  1"
  proof (cases "p = 0")
    case True
    then show ?thesis by simp
  next
    case False
    then have pgt: "p > 0" using assms(1) assms(6) assms(3) ex_min_if_finite less_eq_real_def
      by (meson basic_trans_rules(23) basic_trans_rules(24) linorder_neqE_linordered_idom measure_nonneg)
    have "3 * (d + 1)  4 * d" by (simp add: field_simps assms(8))
    then have "exp(1) * (d + 1)  4 *d"
      using exp_le exp_gt_one[of 1] assms(8)
      by (smt (verit, del_insts) Num.of_nat_simps(2) Num.of_nat_simps(5) le_add2 le_eq_less_or_eq 
          mult_right_mono nat_less_real_le numeral.simps(3) numerals(1) of_nat_numeral) 
    then have "exp(1) * (d + 1) * p  4 *d *p" using pgt by simp 
    then show ?thesis using assms(7) by (simp add: field_simps) 
  qed
  then show ?thesis using assms lovasz_local_symmetric_dep_graph[of A F G d p] by auto
qed


lemma lovasz_local_symmetric4: 
  fixes e :: real
  fixes d :: nat
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes "dependency_digraph G M F"
  assumes " Ai.  Ai  A  out_degree G Ai  d" 
  assumes " Ai. Ai  A  prob (F Ai)  p"
  assumes "4 * p * d  1"
  assumes "d  1"
  assumes "pverts G = A"
  shows "prob ( Ai  A . (space M - F Ai)) > 0"
proof (cases "d  3")
  case True
  then show ?thesis using lovasz_local_symmetric4gt assms
    by presburger
next
  case d3: False
  define f :: "nat  real" where "f  (λ Ai . 1 /(d + 1))"
  then have fbounds: " Ai. f Ai  0  f Ai < 1" using f_def assms(8) by simp
  interpret dg: dependency_digraph G M F using assms(4) by auto
  have " Ai. Ai  A  prob (F Ai)  (f Ai) * ( Aj  dg.neighborhood Ai . (1 - (f Aj)))"
  proof -
    fix Ai assume ain: "Ai  A"
    have d_boundslt1: "(1/(d + 1)) < 1" and d_boundsgt0: "(1/(d + 1))> 0" using assms by fastforce+ 
    have plt: "1/(4*d)  p" using assms(7) assms(8)
      by (metis (mono_tags, opaque_lifting) Num.of_nat_simps(5) bot_nat_0.not_eq_extremum le_numeral_extra(2) 
          more_arith_simps(11) mult_of_nat_commute nat_0_less_mult_iff of_nat_0_less_iff of_nat_numeral 
          pos_divide_less_eq rel_simps(51) verit_comp_simplify(3)) 
    then have gtp: "(1 /(d + 1))* (1 - (1 /(d + 1)))^d  p"
    proof (cases "d = 1")
      case False
      then have "d = 2" using d3 assms(8) by auto 
      then show ?thesis using plt by (simp add: field_simps)
    qed (simp)
    have "card (dg.neighborhood Ai)  d" using assms(5) dg.out_degree_neighborhood ain by auto
    then have "( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1))))  (1 - (1 /(d + 1)))^d"
      using prod_constant_ge[of  "dg.neighborhood Ai" "d" "1 - (1/d+1)"] using d_boundslt1 by auto
    then have "(1 /(d + 1)) * ( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1))))  (1 /(d + 1))* (1 - (1 /(d + 1)))^d"
      by (simp add: divide_right_mono) 
    then have "(1 /(d + 1)) * ( Aj  dg.neighborhood Ai . (1 - (1 /(d + 1))))  p" 
      using gtp by simp
    then show "prob (F Ai)  f Ai * ( Aj  dg.neighborhood Ai . (1 - f Aj))"
      using assms(6) Ai  A f_def by force 
  qed
  then show ?thesis 
    using lovasz_local_general_positive[of A F f G] assms(4) assms(1) assms(2) assms(3) assms(9) fbounds by auto
qed

text ‹Converting between dependency graph and indexed set representation of mutual independence ›

lemma (in pair_digraph) g_Ai_simplification:
  assumes "Ai  A"
  assumes "g Ai  A - {Ai}"
  assumes "pverts G = A"
  assumes "parcs G = {e  A × A . snd e  (A - ({fst e}  (g (fst e))))}"
  shows "g Ai = A - ({Ai}  neighborhood Ai)"
proof -
  have "g Ai = A - ({Ai}  {v  A . v  (A - ({Ai}  (g (Ai))))})"  using assms(2) by auto
  then have "g Ai = A - ({Ai}  {v  A . (Ai, v)  parcs G})"
    using Collect_cong assms(1) mem_Collect_eq assms(3) assms(4) by auto
  then show "g Ai = A - ({Ai}  neighborhood Ai)" unfolding neighborhood_def using assms(3) by simp
qed

lemma define_dep_graph_set:
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai. Ai  A  g Ai  A - {Ai}  mutual_indep_events (F Ai) F (g Ai)"
  shows "dependency_digraph  pverts = A, parcs = {e  A × A . snd e  (A - ({fst e}  (g (fst e))))}  M F"
    (is "dependency_digraph ?G M F")
proof -
  interpret pd: pair_digraph ?G 
    using assms(3)by (unfold_locales) auto 
  have " Ai. Ai  A  g Ai  A - {Ai}" using assms(4) by simp
  then have " i. i  A  g i = A - ({i}  pd.neighborhood i)"
    using pd.g_Ai_simplification[of _ A g] pd.pair_digraph by auto
  then have "dependency_digraph ?G M F" using assms(2) assms(4) by (unfold_locales) auto
  then show ?thesis by simp
qed

lemma define_dep_graph_deg_bound:
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai. Ai  A  g Ai  A - {Ai}  card (g Ai)  card A - d - 1  
    mutual_indep_events (F Ai) F (g Ai)"
  shows " Ai.  Ai  A  
    out_degree  pverts = A, parcs = {e  A × A . snd e  (A - ({fst e}  (g (fst e))))}  Ai  d"
    (is " Ai.  Ai  A  out_degree (with_proj ?G) Ai  d")
proof -
  interpret pd: dependency_digraph ?G M F using assms define_dep_graph_set by simp
  show " Ai.  Ai  A  out_degree ?G Ai  d"
  proof -
    fix Ai assume a: "Ai  A"
    then have geq: "g Ai = A - ({Ai}  pd.neighborhood Ai)" 
      using assms(4)[of Ai] pd.pair_digraph pd.g_Ai_simplification[of Ai A g ]  by simp
    then have pss: "g Ai  A" using a by auto
    then have "card (g Ai) = card (A - ({Ai}  pd.neighborhood Ai))" using assms(4) geq by argo
    moreover have ss: "({Ai}  pd.neighborhood Ai)  A" using pd.neighborhood_wf a  by simp
    moreover have "finite ({Ai}  pd.neighborhood Ai)" 
      using calculation(2) assms(3) finite_subset by auto
    moreover have "Ai  pd.neighborhood Ai" using pd.neighborhood_self_not by simp
    moreover have "card {Ai} = 1" using is_singleton_altdef by auto
    moreover have cardss: "card ({Ai}  pd.neighborhood Ai) = 1 + card (pd.neighborhood Ai)" 
      using calculation(5) calculation(4) card_Un_disjoint pd.neighborhood_finite by auto
    ultimately have eq: "card (g Ai) = card A - 1 - card (pd.neighborhood Ai)" 
      using card_Diff_subset[of "({Ai}  pd.neighborhood Ai)" A] assms(3) by presburger
    have ggt: " Ai. Ai  A  card (g Ai)  int (card A) - int d - 1"
      using assms(4) by fastforce 
    have "card (pd.neighborhood Ai) = card A - 1 - card (g Ai)" 
      using cardss assms(3) card_mono diff_add_inverse diff_diff_cancel diff_le_mono ss eq
      by (metis (no_types, lifting)) 
    moreover have "card A  (1 + card (g Ai))" using pss assms(3) card_seteq not_less_eq_eq by auto 
    ultimately have "card (pd.neighborhood Ai) = int (card A) - 1 - int (card (g Ai))"  by auto
    moreover have "int (card (g Ai))  (card A) - (int d) - 1" using ggt a by simp
    ultimately show "out_degree ?G Ai  d" using pd.out_degree_neighborhood by simp
  qed
qed

lemma obtain_dependency_graph:
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai. Ai  A  
    ( S . S  A - {Ai}  card S  card A - d - 1  mutual_indep_events (F Ai) F S)"
  obtains G where "dependency_digraph G M F" "pverts G = A" " Ai.  Ai  A  out_degree G Ai  d"
proof -
  obtain g where gdef: " Ai. Ai  A  g Ai  A - {Ai}  card (g Ai)  card A - d - 1  
    mutual_indep_events (F Ai) F (g Ai)" using assms(4) by metis
  then show ?thesis 
    using define_dep_graph_set[of A F g] define_dep_graph_deg_bound[of A F g d]that assms by auto 
qed

text ‹This is the variation of the symmetric version most commonly in use ›

theorem lovasz_local_symmetric: 
  fixes d :: nat
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai. Ai  A  ( S . S  A - {Ai}  card S  card A - d - 1  mutual_indep_events (F Ai) F S)" 
  assumes " Ai. Ai  A  prob (F Ai)  p"
  assumes "exp(1)* p * (d + 1)  1"
  shows "prob ( Ai  A . (space M - (F Ai))) > 0"
proof -
  obtain G where odg: "dependency_digraph G M F" "pverts G = A" " Ai.  Ai  A  out_degree G Ai  d"
    using assms obtain_dependency_graph by metis
  then show ?thesis using odg assms lovasz_local_symmetric_dep_graph[of A F G d p] by auto
qed

lemma lovasz_local_symmetric4_set: 
  fixes d :: nat
  assumes "A  {}"
  assumes "F ` A  events"
  assumes "finite A"
  assumes " Ai. Ai  A  ( S . S  A - {Ai}  card S  card A - d - 1  mutual_indep_events (F Ai) F S)" 
  assumes " Ai. Ai  A  prob (F Ai)  p"
  assumes "4 * p * d  1"
  assumes "d  1"
  shows "prob ( Ai  A . (space M - F Ai)) > 0"
proof -
  obtain G where odg: "dependency_digraph G M F" "pverts G = A" " Ai.  Ai  A  out_degree G Ai  d"
    using assms obtain_dependency_graph by metis
  then show ?thesis using odg assms lovasz_local_symmetric4[of A F G d p] by auto
qed
end

end