Theory LLL_Applications
section ‹Lovasz Local Framework Application ›
theory LLL_Applications imports "Lovasz_Local.Lovasz_Local_Lemma"
"Lovasz_Local.Indep_Events" "Twelvefold_Way.Twelvefold_Way_Core"
Design_Theory.Multisets_Extras Basic_Bounds_Application
begin
subsection ‹More set extras ›
lemma multiset_remove1_filter: "a ∈# A ⟹ P a ⟹
{#b ∈# A . P b#} = {#b ∈# remove1_mset a A . P b#} + {#a#}"
by auto
lemma card_partition_image:
assumes "finite C"
assumes "finite (⋃c ∈ C . f c)"
assumes "(⋀ c. c∈C ⟹ card (f c) = k)"
assumes "(⋀ c1 c2. c1 ∈ C ⟹ c2 ∈ C ⟹ c1 ≠ c2 ⟹ f c1 ∩ f c2 = {})"
shows "k * card (f ` C) = card (⋃c ∈ C . f c)"
proof -
have "card (⋃c ∈ C . f c) = card (⋃(f ` C))" by simp
moreover have "finite (f ` C)" using assms(1) by auto
moreover have "finite (⋃(f ` C))" using assms(2) by auto
moreover have "⋀c. c ∈ f ` C ⟹ card c = k" using assms(3) by auto
moreover have "(⋀c1 c2. c1 ∈ f ` C ⟹ c2 ∈ f ` C ⟹ c1 ≠ c2 ⟹ c1 ∩ c2 = {})" using assms(4) by auto
ultimately show ?thesis using card_partition[of "f ` C" k] by auto
qed
lemma mset_set_implies:
assumes "image_mset f (mset_set A) = B"
assumes "⋀ a . a ∈ A ⟹ P (f a)"
shows "⋀ b. b ∈# B ⟹ P b"
proof -
fix b assume "b ∈# B"
then obtain a where "a ∈ A" and eqb: "f a = b"
using assms(1) by (meson bij_mset_obtain_set_elem)
then show "P b" using assms(2) by auto
qed
lemma card_partition_image_inj:
assumes "finite C"
assumes "inj_on f C"
assumes "finite (⋃c ∈ C . f c)"
assumes "(⋀ c. c∈C ⟹ card (f c) = k)"
assumes "(⋀ c1 c2. c1 ∈ C ⟹ c2 ∈ C ⟹ c1 ≠ c2 ⟹ f c1 ∩ f c2 = {})"
shows "k * card (C) = card (⋃c ∈ C . f c)"
proof -
have "card C = card (f ` C)" using assms(2) card_image
by fastforce
then show ?thesis using card_partition_image assms
by metis
qed
lemma size_big_union_sum2:
fixes M :: "'a ⇒ 'b multiset"
shows "size (∑ x ∈# X . M x) = (∑x ∈#X . size (M x))"
by (induct X) auto
lemma size_big_union_sum2_const:
fixes M :: "'a ⇒ 'b multiset"
assumes "⋀ x . x ∈# X ⟹ size (M x) = k"
shows "size (∑ x ∈# X . M x) = size X * k"
proof -
have "size (∑ x ∈# X . M x) = (∑x ∈#X . size (M x))"
using size_big_union_sum2 by auto
also have "... = (∑x ∈#X . k)" using assms by auto
finally show ?thesis by auto
qed
lemma count_sum_mset2: "count (∑ x ∈# X . M x) a = (∑ x ∈# X . count (M x) a)"
using count_sum_mset by (smt (verit) image_image_mset sum_over_fun_eq)
lemma mset_subset_eq_elemI:
"(⋀a . a ∈# A ⟹ count A a ≤ count B a) ⟹ A ⊆# B"
by (intro mset_subset_eqI) (metis zero_le count_eq_zero_iff)
lemma mset_obtain_from_filter:
assumes "a ∈# {# b ∈# B . P b #}"
shows "a ∈# B" and "P a"
using assms apply (metis multiset_partition union_iff)
using assms by (metis (mono_tags, lifting) Multiset.set_mset_filter mem_Collect_eq)
subsection ‹Mutual Independence Principle for Hypergraphs ›
context fin_hypergraph_nt
begin
definition (in incidence_system) block_intersect_count :: "'a set ⇒ nat" where
"block_intersect_count b ≡ size {# b2 ∈# (ℬ - {#b#}) . b2 ∩ b ≠ {} #}"
lemma (in hypergraph) edge_intersect_count_inc:
assumes "e ∈# E"
shows "size {# f ∈# E . f ∩ e ≠ {}#} = block_intersect_count e + 1"
unfolding block_intersect_count_def
proof -
have "e ∩ e ≠ {}" using blocks_nempty assms(1) by simp
then have "{#f ∈# E. f ∩ e ≠ {}#} = {#f ∈# remove1_mset e E. f ∩ e ≠ {}#} + {#e#}"
using multiset_remove1_filter[of e E "λ f. f ∩ e ≠ {}"] assms(1) by blast
then show "size {#f ∈# E. f ∩ e ≠ {}#} = size {#b2 ∈# remove1_mset e E. b2 ∩ e ≠ {}#} + 1"
by (metis size_single size_union)
qed
lemma disjoint_set_is_mutually_independent:
assumes iin: "i ∈ {0..<(size E)}"
assumes idffn: "idf ∈ {0..<size E} →⇩E set_mset E"
assumes Aefn: "⋀ i. i ∈ {0..<size E} ⟹ Ae i = {f ∈ 𝒞⇧2 . mono_edge f (idf i)}"
shows "prob_space.mutual_indep_events (uniform_count_measure (𝒞⇧2)) (Ae i) Ae
({j ∈{0..<(size E)} . (idf j ∩ idf i) = {}})"
proof -
interpret P: vertex_colour_space 𝒱 E 2
using order_ge_two by (unfold_locales) (auto)
have "P.mutual_indep_events (Ae i) Ae ({j ∈{0..<(size E)} . (idf j ∩ idf i) = {}})"
proof (intro P.mutual_indep_eventsI)
show "Ae i ∈ P.events" using P.sets_eq iin Aefn by simp
next
show "Ae ` {j ∈ {0..<𝖻}. idf j ∩ idf i = {}} ⊆ P.events" using P.sets_eq Aefn by auto
next
show "⋀J. J ⊆ {j ∈ {0..<𝖻}. idf j ∩ idf i = {}} ⟹ J ≠ {} ⟹
P.prob (Ae i ∩ ⋂ (Ae ` J)) = P.prob (Ae i) * P.prob (⋂ (Ae ` J))"
proof -
let ?e = "idf i"
fix J assume jss: "J ⊆ {j ∈ {0..<𝖻}. idf j ∩ ?e = {}}" and ne: "J ≠ {}"
then have "finite J" using finite_subset finite_nat_set_iff_bounded_le mem_Collect_eq
by (metis (full_types) finite_Collect_conjI finite_atLeastLessThan)
have jin: "⋀ j . j ∈ J ⟹ j ∈ {0..<𝖻}" using jss by auto
have iedge: "⋀i. i ∈ {0..<size E} ⟹ idf i ∈# E" using idffn by auto
define P' where "P' ≡ (𝒱 - ?e) →⇩E {0..<2::colour}"
then have finP: "finite P'" using finite_PiE finite_sets by (metis P.finP finite_Diff)
define T where "T ≡ λ p. {f ∈ 𝒞⇧2 . ∀ v ∈ (𝒱 - ?e) . f v = p v}"
have Tss: "⋀ p. T p ⊆ 𝒞⇧2" unfolding T_def by auto
have Pdjnt: "⋀ p1 p2. p1 ∈ P' ⟹ p2 ∈ P' ⟹ p1 ≠ p2 ⟹ T p1 ∩ T p2 = {}"
proof -
fix p1 p2 assume p1in: "p1 ∈ P'" and p2in: "p2 ∈ P'" and pne: "p1 ≠ p2"
have "⋀ x. x ∈ T p1 ⟹ x ∉ T p2"
proof (rule ccontr)
fix x assume xin: "x ∈ T p1" and "¬ x ∉ T p2"
then have xin2: "x ∈ T p2" by simp
then have "x ∈ 𝒞⇧2" and "∀ v ∈ (𝒱 - ?e) . x v = p1 v" and "∀ v ∈ (𝒱 - ?e) . x v = p2 v"
using T_def xin by auto
then have "⋀ v. v ∈ (𝒱 - ?e) ⟹ p1 v = p2 v" by auto
then have "p1 = p2" using p1in p2in unfolding P'_def
using PiE_ext by metis
then show False using pne by simp
qed
then show "T p1 ∩ T p2 = {}" by auto
qed
have cp: "⋀ p. p ∈ P' ⟹ card (T p) = 2 powi (card ?e)"
proof -
fix p assume pin: "p ∈ P'"
have "card (𝒱 - ?e) = card 𝒱 - card ?e" using iedge wellformed iin
using block_complement_def block_complement_size by auto
moreover have "card 𝒱 ≥ card ?e" using iedge wellformed iin
by (simp add: block_size_lt_order)
ultimately have "(card 𝒱 - card (𝒱 - ?e)) = card ?e" by simp
then have "card {0..<2::colour} ^ (card 𝒱 - card (𝒱 - ?e)) = 2 powi (card ?e)" by auto
moreover have "(⋀a. a ∈ (𝒱 - ?e) ⟹ p a ∈ {0..<2})"
using pin P'_def by auto
ultimately show "card (T p) = 2 powi (card ?e)"
unfolding T_def using card_PiE_filter_range_set[of "𝒱 - ?e" p "{0..<2::colour}" 𝒱 ]
finite_sets all_n_vertex_colourings_alt by auto
qed
define Ps where "Ps ≡ {p ∈ P' . T p ⊆ ⋂(Ae ` J)}"
have psss: "Ps ⊆ P'" unfolding Ps_def P'_def by auto
have p1: "⋀ i. i ∈ {0..<𝖻} ⟹ P.prob(Ae i) = 1/(2 powi (int (card (idf i)) - 1))"
using Aefn P.prob_monochromatic_edge_inv iedge by simp
have bunrep: "⋂(Ae ` J) = (⋃p ∈ Ps . T p)"
proof (intro subset_antisym subsetI)
fix x assume "x ∈ ⋂(Ae ` J)"
then have xin: "x ∈ 𝒞⇧2" and xmono: "⋀ j. j ∈ J ⟹ mono_edge x (idf j)"
using jin Aefn ne by auto
define p where "p = (λ v . if (v ∈ 𝒱 - ?e) then x v else undefined)"
then have pin: "p ∈ P'" unfolding P'_def using xin all_n_vertex_colourings_alt by auto
then have xtin: "x ∈ T p" unfolding T_def p_def
by (simp add: xin)
have "T p ⊆ ⋂(Ae ` J)"
proof (intro subsetI)
fix y assume yin: "y ∈ T p"
have "⋀ j . j ∈ J ⟹ mono_edge y (idf j)"
proof -
fix j assume jin: "j ∈ J"
then have "idf j ∩ idf i = {}" using jss by auto
then have "⋀ v . v ∈ idf j ⟹ v ∉ ?e" by auto
then have "⋀ v . v ∈ idf j ⟹ v ∈ 𝒱 - ?e" using jss wellformed
by (metis (no_types, lifting) DiffI ‹j ∈ J› basic_trans_rules(31) iedge mem_Collect_eq)
then have "⋀ v . v ∈ idf j ⟹ y v = x v" using yin T_def p_def by auto
then show "mono_edge y (idf j)" using xmono jin
by (simp add: mono_edge_def)
qed
moreover have "y ∈ 𝒞⇧2"
using Tss yin by auto
ultimately show "y ∈⋂(Ae ` J)" using Aefn jin by auto
qed
then have "p ∈ Ps" unfolding Ps_def using pin by auto
then show "x ∈ (⋃ p ∈ Ps . T p)"
using xtin by auto
next
fix x assume "x ∈ (⋃ p ∈ Ps . T p)"
then show "x ∈ ⋂(Ae ` J)" unfolding Ps_def by auto
qed
moreover have dfo: "disjoint_family_on (λ p. T p) Ps"
using psss Pdjnt disjoint_family_on_def by blast
moreover have "(λ p . T p) ` Ps ⊆ P.events"
unfolding T_def Ps_def using P.sets_eq by auto
moreover have finPs: "finite Ps" using finP psss finite_subset by auto
ultimately have "P.prob (⋂(Ae ` J)) = (∑ p ∈ Ps. P.prob (T p))"
using P.finite_measure_finite_Union[of Ps "λ p . T p"] by simp
moreover have "⋀ p. p ∈ Ps ⟹ P.prob (T p) = card (T p)/card (𝒞⇧2)"
using measure_uniform_count_measure[of "𝒞⇧2"] Tss
by (simp add: P.MU_def P.fin_Ω)
ultimately have "P.prob (⋂(Ae ` J)) = (∑ p ∈ Ps. real (card (T p)))/(card (𝒞⇧2))"
using sum_divide_distrib[of _ Ps "card (𝒞⇧2)"] by (simp)
also have "... = (∑ p ∈ Ps. 2 powi (card ?e))/(card (𝒞⇧2))"
using cp psss by (simp add: Ps_def)
finally have "P.prob (⋂(Ae ` J)) = (card Ps * (2 powi (card ?e)))/(card (𝒞⇧2))"
by simp
then have "P.prob (Ae i) * P.prob (⋂(Ae ` J)) =
1/(2 powi (int (card (?e)) - 1)) * ((card Ps * (2 powi (card ?e)))/(card (𝒞⇧2)))"
using iin p1 by simp
also have "... = (((2 powi (card ?e)))/(2 powi (int (card (?e)) - 1))) * (card Ps/card (𝒞⇧2))"
by (simp add: field_simps)
also have "... = 2 * (card Ps/card (𝒞⇧2))"
using power_int_diff[of "2::real" "int (card ?e)" "(int (card (?e)) - 1)"] by simp
finally have prob: "P.prob (Ae i) * P.prob (⋂(Ae ` J)) = (card Ps * 2)/(card (𝒞⇧2))" by simp
have "(Ae i) ∩ (⋂(Ae ` J)) = (⋃p ∈ Ps . ((Ae i) ∩ T p))"
using bunrep by auto
moreover have "disjoint_family_on (λ p. (Ae i) ∩ T p) Ps"
using dfo disjoint_family_on_bisimulation[of T Ps "(λ p. (Ae i) ∩ T p)"] by auto
moreover have "(λ p . (Ae i) ∩ T p) ` Ps ⊆ P.events"
unfolding T_def using P.sets_eq by auto
ultimately have "P.prob ((Ae i) ∩ (⋂(Ae ` J))) = (∑ p ∈ Ps. P.prob ((Ae i) ∩ T p))"
using P.finite_measure_finite_Union[of Ps "λp. (Ae i) ∩ T p"] finPs by simp
moreover have tss2: "⋀ p. (Ae i) ∩ T p ⊆ 𝒞⇧2" using Tss by auto
moreover have "⋀ p. p ∈ Ps ⟹ P.prob ((Ae i) ∩ T p) = card ((Ae i) ∩ T p)/card (𝒞⇧2)"
using measure_uniform_count_measure[of "𝒞⇧2"] tss2 P.MU_def P.fin_Ω by simp
ultimately have "P.prob ((Ae i) ∩ (⋂(Ae ` J))) = (∑ p ∈ Ps. card ((Ae i) ∩ T p))/(card (𝒞⇧2))"
using sum_divide_distrib[of _ Ps "card (𝒞⇧2)"] by (simp)
moreover have "⋀ p. p ∈ Ps ⟹ card ((Ae i) ∩ (T p)) = 2"
proof -
fix p assume "p ∈ Ps"
define h where "h ≡ λ c. (λ v. if (v ∈ 𝒱) then (if (v ∈ ?e) then c else p v) else undefined)"
have hc: "⋀ c v. v ∈ ?e ⟹ h c v = c" unfolding h_def using wellformed iin iedge by auto
have hne: "⋀ c1 c2. c1 ≠ c2 ⟹ h c1 ≠ h c2"
proof (rule ccontr)
fix c1 c2 assume ne: "c1 ≠ c2" "¬ h c1 ≠ h c2"
then have eq: "h c1 = h c2" by simp
have "⋀ v . v ∈ ?e ⟹ h c1 v = c1" using hc by simp
then have "⋀ v . v ∈ ?e ⟹ c1 = c2" using hc eq by auto
then show False using ne eq using V_nempty blocks_nempty iedge iin by blast
qed
then have hdjnt: "⋀ n. (∀c1 ∈ {0..<n}. ∀c2 ∈ {0..<n}. c1 ≠ c2 ⟶ {h c1} ∩ {h c2} = {})"
by auto
have heq: "⋀ c. c ∈ {0..<2} ⟹ {f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)} = {h c}"
proof -
fix c assume "c ∈ {0..<2::nat}"
have "⋀ x f. f ∈ {f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)} ⟹ f x = h c x"
unfolding h_def using mono_edge_colD all_n_vertex_colourings_alt by auto
then have "⋀ f . f ∈ {f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)} ⟹ f = h c"
by auto
moreover have "h c ∈ {f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)}"
proof -
have "h c ∈ 𝒞⇧2" unfolding h_def using all_n_vertex_colourings_alt
by (smt (verit, ccfv_SIG) DiffI P'_def PiE_I PiE_mem ‹c ∈ {0..<2}› ‹p ∈ Ps› psss subset_eq)
moreover have "mono_edge_col (h c) ?e c" using mono_edge_colI hc by auto
ultimately show ?thesis unfolding h_def by auto
qed
ultimately show "{f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)} = {h c}"
by blast
qed
have "Ae i = (⋃ c ∈ {0..<2}. {f ∈ 𝒞⇧2 . mono_edge_col f ?e c})"
using Aefn iedge iin mono_edge_set_union[of ?e 2] by auto
then have "(Ae i) ∩ (T p) = (⋃ c ∈ {0..<2}. {f ∈ 𝒞⇧2 . mono_edge_col f ?e c ∧ (∀ v ∈ (𝒱 - ?e) . f v = p v)})"
unfolding T_def by auto
then have "card ((Ae i) ∩ (T p)) = card ((⋃ c ∈ {0..<2}. {h c}))" using heq by simp
moreover have "(1:: nat) * card {0..<2::nat} = card ((⋃ c ∈ {0..<2}. {h c}))"
proof -
have "inj_on (λc. {h c}) {0..<2}" using hdjnt inj_onI
by (metis (mono_tags, lifting) hne insertI1 singletonD)
then show ?thesis
using card_partition_image_inj[of "{0..<2}" "λ c . {h c}" "1:: nat"] hdjnt by auto
qed
ultimately show "card ((Ae i) ∩ (T p)) = 2" by auto
qed
ultimately show "P.prob (Ae i ∩ ⋂ (Ae ` J)) = P.prob (Ae i) * P.prob (⋂ (Ae ` J))"
using prob by simp
qed
qed
then show ?thesis using P.MU_def by auto
qed
lemma intersect_empty_set_size:
assumes "⋀ e . e ∈#E ⟹ size {# f ∈# (E - {#e#}) . f ∩ e ≠ {}#} ≤ d"
assumes "e2 ∈# E"
shows "size {#e ∈# E . e ∩ e2 = {} #} ≥ size E - d - 1" (is "size ?S' ≥ size E - d - 1")
proof -
have a1alt: "⋀ e . e ∈#E ⟹ size {# f ∈# E . f ∩ e ≠ {}#} ≤ d + 1"
using edge_intersect_count_inc assms(1) block_intersect_count_def by force
have "E = ?S' + {#e ∈# E. e ∩ e2 ≠ {}#}" by auto
then have "size E = size ?S' + size {#e ∈# E. e ∩ e2 ≠ {}#}"
by (metis size_union)
then have "size ?S' = size E - size {#e ∈# E. e ∩ e2 ≠ {}#}" by simp
moreover have "size {#e ∈# E . e ∩ e2 ≠ {} #} ≤ d + 1" using a1alt assms(2) by auto
ultimately show ?thesis by auto
qed
subsection ‹Application Property B ›
text ‹Probabilistic framework clearly notated ›
proposition erdos_propertyB_LLL:
assumes "⋀ e. e ∈#E ⟹ card e ≥ k"
assumes "⋀ e . e ∈#E ⟹ size {# f ∈# (E - {#e#}) . f ∩ e ≠ {}#} ≤ d"
assumes "exp(1)*(d+1) ≤ (2 powi (k - 1))"
assumes "k > 0"
shows "has_property_B"
proof -
interpret P: vertex_colour_space 𝒱 E 2
by unfold_locales (auto simp add: order_ge_two)
let ?N = "{0..<size E}"
obtain id where ideq: "image_mset id (mset_set ?N) = E" and idin: "id ∈ ?N →⇩E set_mset E"
using obtain_function_on_ext_funcset[of "?N" E] by auto
then have iedge: "⋀i. i ∈ ?N ⟹ id i ∈# E" by auto
define Ae where "Ae ≡ λ i. {f ∈ 𝒞⇧2 . mono_edge f (id i)}"
have "0 < P.prob (⋂Ai∈?N. space P.MU - Ae Ai)"
proof (intro P.lovasz_local_symmetric[of ?N Ae d "(1/(2 powi (k-1)))"])
have mis: "⋀i . i ∈ ?N ⟹ P.mutual_indep_events (Ae i) Ae ({j ∈?N . (id j ∩ id i) = {}})"
using disjoint_set_is_mutually_independent[of _ id Ae] P.MU_def assms idin by (simp add: Ae_def)
then show "⋀ i . i ∈ ?N ⟹ ∃ S. S ⊆ ?N - {i} ∧ card S ≥ card ?N - d - 1 ∧
P.mutual_indep_events (Ae i) Ae S"
proof -
fix i assume iin: "i ∈ ?N"
define S' where "S' ≡ {j ∈ ?N. (id j) ∩ (id i) = {}}"
then have "S' ⊆ ?N - {i}" using iedge assms(1) using blocks_nempty iin by auto
moreover have "P.mutual_indep_events (Ae i) Ae S'" using mis iin S'_def by simp
moreover have "card S' ≥ card ?N - d - 1"
unfolding S'_def using function_map_multi_filter_size[of id ?N E "λ e . e ∩ (id i) = {}"]
ideq intersect_empty_set_size[of d "id i"] iin iedge assms(2) by auto
ultimately show "∃ S. S ⊆ ?N - {i} ∧ card S ≥ card ?N - d - 1 ∧ P.mutual_indep_events (Ae i) Ae S"
by blast
qed
show "⋀ i. i ∈ ?N ⟹ P.prob(Ae i) ≤ 1/(2 powi (k-1))"
unfolding Ae_def using P.prob_monochromatic_edge_bound[of _ k] iedge assms(4) assms(1) by auto
show "exp(1) * (1 / 2 powi int (k - 1)) * (d + 1) ≤ 1"
using assms(3) by (simp add: field_simps del:One_nat_def)
(metis Num.of_nat_simps(2) assms(4) diff_is_0_eq diff_less less_one of_nat_diff power_int_of_nat)
qed (auto simp add: Ae_def E_nempty P.sets_eq P.space_eq)
then obtain f where fin: "f ∈ 𝒞⇧2" and "⋀ i. i ∈ ?N ⟹ ¬ mono_edge f (id i)" using Ae_def
P.obtain_intersection_prop[of Ae ?N "λ f i. mono_edge f (id i)"] P.space_eq P.sets_eq by auto
then have "⋀ e. e ∈# E ⟹ ¬ mono_edge f e"
using ideq mset_set_implies[of id ?N E "λ e. ¬ mono_edge f e"] by blast
then show ?thesis unfolding is_n_colourable_def
using is_proper_colouring_alt2 fin all_n_vertex_colourings_def[of 2] by auto
qed
end
subsection ‹Application Corollary ›
text ‹A corollary on hypergraphs where k \ge 9›
lemma exp_ineq_k9:
fixes k:: nat
assumes "k ≥ 9"
shows "exp(1::real) * (k *(k -1) + 1) < 2^(k-1)"
using assms
proof (induct k rule: nat_induct_at_least)
case base
show ?case using exp_le by auto
next
case (Suc n)
have "Suc n * (Suc n - 1) + 1 = n * (n - 1) + 1 + 2*n" by (simp add: algebra_simps power2_eq_square)
then have "exp (1::real) * (Suc n * (Suc n - 1) + 1) = exp 1 * (n * (n - 1) + 1) + exp 1 * 2*n"
by (simp add: field_simps)
moreover have "exp (1::real) * (n * (n - 1) + 1) < 2^(n-1)" using Suc.hyps by simp
moreover have "exp (1:: real) * 2*n ≤ exp (1::real) * (n * (n - 1) + 1)"
proof -
have "2*n ≤ (n * (n - 1) + 1)" using Suc.hyps(1) Groups.mult_ac(2) diff_le_mono mult_le_mono1
nat_le_linear numeral_Bit1 numerals(1) ordered_cancel_comm_monoid_diff_class.le_imp_diff_is_add
by (metis (no_types, opaque_lifting) Suc_eq_plus1 not_less_eq_eq numeral_Bit0 trans_le_add1)
then have "2 * real n ≤ real (n * (n - 1) + 1)" using Suc.hyps by linarith
then show ?thesis using exp_gt_one[of "1::real"] by simp
qed
moreover have "2 ^ (Suc n - 1) = 2 * 2^(n-1)"
by (metis Nat.le_imp_diff_is_add Suc(1) add_leD1 cross3_simps(8) diff_Suc_1 eval_nat_numeral(3)
power.simps(2) semiring_norm(174))
ultimately show ?case by (smt (verit))
qed
context fin_kuniform_regular_hypgraph_nt
begin
text ‹Good example of a combinatorial counting proof in a formal environment ›
lemma (in fin_dregular_hypergraph) hdeg_remove_one:
assumes "e ∈# E"
assumes "v ∈# mset_set e"
shows "size {# f ∈# (E - {#e#}) . v ∈ f#} = d - 1"
proof -
have "v ∈ e"
using assms by (meson count_mset_set(3) not_in_iff)
then have vvertex: "v ∈ 𝒱" using wellformed[of e] assms(1) by auto
then have "{# f ∈# (E - {#e#}) . v ∈ f#} = {# f ∈# E . v ∈ f#} - {#e#}"
by (simp add: diff_union_cancelR assms(1) finite_blocks)
then have "size {# f ∈# (E - {#e#}) . v ∈ f#} = size {# f ∈# E . v ∈ f#} - 1"
by (metis ‹v ∈# mset_set e› count_eq_zero_iff count_mset_set(3) assms(1) multiset_remove1_filter
size_Diff_singleton union_iff union_single_eq_member)
moreover have "size {# f ∈# E . v ∈ f#} = d"
using hdegree_def const_degree vvertex by auto
ultimately show "size {# f ∈# (E - {#e#}) . v ∈ f#} = d - 1" by simp
qed
lemma max_intersecting_edges:
assumes "e ∈# E"
shows "size {# f ∈# (E - {#e#}) . f ∩ e ≠ {}#} ≤ k * (k -1)"
proof -
have eq: "{# f ∈# (E - {#e#}) . f ∩ e ≠ {}#} ⊆# (∑ v ∈# (mset_set e) . {#f ∈# (E - {#e#}) . v ∈ f #})"
proof (intro mset_subset_eq_elemI)
fix a assume "a ∈# {#f ∈# remove1_mset e E. f ∩ e ≠ {}#}" (is "a ∈# ?E'")
then have ain: "a ∈# remove1_mset e E" and "a ∩ e ≠ {}"
using mset_obtain_from_filter by fast+
then obtain v where "v ∈ a" and "v ∈ e" by blast
then have vvertex: "v ∈ 𝒱" using wellformed[of e] assms(1) by auto
have "count ?E' a ≤ count {#f ∈# E - {#e#}. v ∈ f #} a"
by (metis ‹a ∈# ?E'› ‹v ∈ a› count_filter_mset le_eq_less_or_eq mset_obtain_from_filter(2))
moreover have "count {#f ∈# E - {#e#}. v ∈ f #} a ≤
(∑ v ∈# (mset_set e) . count {#f ∈# (E - {#e#}) . v ∈ f #} a)"
by (metis ‹v ∈ e› assms(1) finite_blocks finite_set_mset_mset_set sum_image_mset_mono_mem)
moreover have "count (∑ v ∈# (mset_set e) . {#f ∈# (E - {#e#}) . v ∈ f #}) a =
(∑ v ∈# (mset_set e) . count {#f ∈# (E - {#e#}) . v ∈ f #} a)"
using count_sum_mset2 by fast
ultimately show "count ?E' a ≤ count (∑v∈#mset_set e. filter_mset ((∈) v) (remove1_mset e E)) a"
by linarith
qed
have "size (mset_set e) = k"
using uniform assms(1) by auto
then have "size (∑ v ∈# (mset_set e) . {#f ∈# (E - {#e#}) . v ∈ f #}) = k * (k - 1)"
using size_big_union_sum2_const[of "mset_set e" "λ v .{#f ∈# (E - {#e#}) . v ∈ f #}" "k - 1"]
hdeg_remove_one assms(1) by fast
then show ?thesis
using eq by (metis size_mset_mono)
qed
corollary erdos_propertyB_LLL9:
assumes "k ≥ 9"
shows "has_property_B"
proof -
define d where "d = k*(k-1)"
have "⋀ e. e ∈# E ⟹ card e ≥ k"
using uniform by simp
moreover have "⋀ e . e ∈# E ⟹ size {# f ∈# (E - {#e#}) . f ∩ e ≠ {}#} ≤ d"
using max_intersecting_edges d_def by simp
moreover have "exp(1)*(d+1) < (2 powi ( k - 1))"
unfolding d_def using exp_ineq_k9 assms(1) by simp
moreover have "k > 0" using assms by auto
ultimately show ?thesis using erdos_propertyB_LLL[of k d] assms
using int_ops(1) int_ops(2) int_ops(6) less_eq_real_def nat_less_as_int by auto
qed
end
end