Theory Lovasz_Local.Lovasz_Local_Lemma
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 "(∏x∈A. 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 ≤ (∏i∈J. 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 | ⋂Aj∈S. space M - F Aj) = P1/P2 ∧
P1 ≤ prob (F Ai)∧ P2 ≥ (∏ Aj ∈ N . (1 - (f Aj)))"
shows "𝒫(F Ai | ⋂Aj∈S. 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 | ⋂Aj∈S. 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 (⋂Aj∈B. space M - F Aj) ⟹ 𝒫(F (g i) | ⋂Aj∈B. 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 | ⋂Aj∈S. 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: "(∏Ai∈X. 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 "... ≥ (∏Ai∈X. 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) ≥ (∏Ai∈insert 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"
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
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
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"
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