Theory Ramsey_Bounds.Ramsey_Bounds
section ‹Lower bounds for Ramsey numbers›
text ‹Probabilistic proofs of lower bounds for Ramsey numbers. Variations and strengthenings of
the classical Erdős--Szekeres upper bound, which is proved in the original Ramsey theory
Also a number of simple properties of Ramsey numbers, including the equivalence of the clique/anticlique
and edge colouring definitions.›
theory Ramsey_Bounds
imports
"HOL-Library.Ramsey"
"HOL-Library.Infinite_Typeclass"
"HOL-Probability.Probability"
"Undirected_Graph_Theory.Undirected_Graph_Basics"
begin
subsection ‹Preliminaries›
text ‹Elementary facts involving binomial coefficients›
lemma choose_two_real: "of_nat (n choose 2) = real n * (real n - 1) / 2"
proof (cases "even n")
case True
then show ?thesis
by (auto simp: choose_two dvd_def)
next
case False
then have "even (n-1)"
by simp
then show ?thesis
by (auto simp: choose_two dvd_def)
qed
lemma add_choose_le_power: "(n + k) choose n ≤ Suc k ^ n"
proof -
have *: "(∏i<n. of_nat (n+k - i) / of_nat (n - i)) ≤ (∏i<n. real (Suc k))"
proof (intro prod_mono conjI)
fix i
assume i: "i ∈ {..<n}"
then have "real (n + k - i) / real (n - i) = 1 + k/real(n-i)"
by (auto simp: divide_simps)
also have "… ≤ 1 + real k"
using i by (simp add: divide_inverse inverse_le_1_iff mult_left_le)
finally show "real (n + k - i) / real (n - i) ≤ real (Suc k)"
by simp
qed auto
then have "real((n + k) choose n) ≤ real (Suc k ^ n)"
by (simp add: binomial_altdef_of_nat lessThan_atLeast0)
then show ?thesis
by linarith
qed
lemma choose_le_power: "m choose k ≤ (Suc m - k) ^ k"
by (metis Suc_diff_le add_choose_le_power add_diff_inverse_nat binomial_eq_0_iff less_le_not_le nle_le zero_le)
lemma sum_nsets_one: "(∑U∈[V]⇗Suc 0⇖. f U) = (∑x∈V. f {x})"
proof -
have bij: "bij_betw (λx. {x}) V ([V]⇗Suc 0⇖)"
by (auto simp: inj_on_def bij_betw_def nsets_one)
show ?thesis
using sum.reindex_bij_betw [OF bij] by (metis (no_types, lifting) sum.cong)
qed
subsection ‹Relating cliques to graphs; Ramsey numbers›
text ‹When talking about Ramsey numbers, sometimes cliques are best, sometimes colour maps›
lemma nsets2_eq_all_edges: "[A]⇗2⇖ = all_edges A"
using card_2_iff' unfolding nsets_def all_edges_def
by fastforce
lemma indep_eq_clique_compl: "indep R E = clique R (all_edges R - E)"
by (auto simp: indep_def clique_def all_edges_def)
lemma all_edges_subset_iff_clique: "all_edges K ⊆ E ⟷ clique K E"
by (fastforce simp: card_2_iff clique_def all_edges_def)
definition "clique_indep ≡ λm n K E. card K = m ∧ clique K E ∨ card K = n ∧ indep K E"
lemma clique_all_edges_iff: "clique K (E ∩ all_edges K) ⟷ clique K E"
by (simp add: clique_def all_edges_def)
lemma indep_all_edges_iff: "indep K (E ∩ all_edges K) ⟷ indep K E"
by (simp add: indep_def all_edges_def)
lemma clique_indep_all_edges_iff: "clique_indep s t K (E ∩ all_edges K) = clique_indep s t K E"
by (simp add: clique_all_edges_iff clique_indep_def indep_all_edges_iff)
text ‹identifying Ramsey numbers (possibly not the minimum) for a given type and pair of integers›
definition is_clique_RN where
"is_clique_RN ≡ λU::'a itself. λm n r.
(∀V::'a set. ∀E. finite V ⟶ card V ≥ r ⟶ (∃K⊆V. clique_indep m n K E))"
text ‹could be generalised to allow e.g. any hereditarily finite set›
abbreviation is_Ramsey_number :: "[nat,nat,nat] ⇒ bool" where
"is_Ramsey_number m n r ≡ partn_lst {..<r} [m,n] 2"
lemma is_clique_RN_imp_partn_lst:
fixes U :: "'a itself"
assumes r: "is_clique_RN U m n r" and inf: "infinite (UNIV::'a set)"
shows "partn_lst {..<r} [m,n] 2"
unfolding partn_lst_def
proof (intro strip)
fix f
assume f: "f ∈ [{..<r}]⇗2⇖ → {..<length [m,n]}"
obtain V::"'a set" where "finite V" and V: "card V = r"
by (metis inf infinite_arbitrarily_large)
then obtain φ where φ: "bij_betw φ V {..<r}"
using to_nat_on_finite by blast
have φ_iff: "φ v = φ w ⟷ v=w" if "v∈V" "w∈V" for v w
by (metis φ bij_betw_inv_into_left that)
define E where "E ≡ {e. ∃x∈V. ∃y∈V. e = {x,y} ∧ x ≠ y ∧ f {φ x, φ y} = 0}"
obtain K where "K⊆V" and K: "clique_indep m n K E"
by (metis r V ‹finite V› is_clique_RN_def nle_le)
then consider (0) "card K = m" "clique K E" | (1) "card K = n" "indep K E"
by (meson clique_indep_def)
then have "∃i<2. monochromatic {..<r} ([m, n] ! i) 2 f i"
proof cases
case 0
have "f e = 0"
if e: "e ⊆ φ ` K" "finite e" "card e = 2" for e :: "nat set"
proof -
obtain x y where "x∈V" "y∈V" "e = {φ x, φ y} ∧ x ≠ y"
using e ‹K⊆V› φ by (fastforce simp: card_2_iff)
then show ?thesis
using e 0
apply (simp add: φ_iff clique_def E_def doubleton_eq_iff image_iff)
by (metis φ_iff insert_commute)
qed
moreover have "φ ` K ∈ [{..<r}]⇗m⇖"
unfolding nsets_def
proof (intro conjI CollectI)
show "φ ` K ⊆ {..<r}"
by (metis ‹K ⊆ V› φ bij_betw_def image_mono)
show "finite (φ ` K)"
using ‹φ ` K ⊆ {..<r}› finite_nat_iff_bounded by auto
show "card (φ ` K) = m"
by (metis "0"(1) ‹K ⊆ V› φ bij_betw_same_card bij_betw_subset)
qed
ultimately show ?thesis
apply (simp add: image_subset_iff monochromatic_def)
by (metis (mono_tags, lifting) mem_Collect_eq nsets_def nth_Cons_0 pos2)
next
case 1
have "f e = Suc 0"
if e: "e ⊆ φ ` K" "finite e" "card e = 2" for e :: "nat set"
proof -
obtain x y where "x∈V" "y∈V" "e = {φ x, φ y} ∧ x ≠ y"
using e ‹K⊆V› φ by (fastforce simp: card_2_iff)
then show ?thesis
using e 1 f bij_betw_imp_surj_on [OF φ]
apply (simp add: indep_def E_def card_2_iff Pi_iff doubleton_eq_iff image_iff)
by (metis ‹K ⊆ V› doubleton_in_nsets_2 imageI in_mono less_2_cases_iff less_irrefl numeral_2_eq_2)
qed
then have "f ` [φ ` K]⇗2⇖ ⊆ {Suc 0}"
by (simp add: image_subset_iff nsets_def)
moreover have "φ ` K ∈ [{..<r}]⇗n⇖"
unfolding nsets_def
proof (intro conjI CollectI)
show "φ ` K ⊆ {..<r}"
by (metis ‹K ⊆ V› φ bij_betw_def image_mono)
show "finite (φ ` K)"
using ‹φ ` K ⊆ {..<r}› finite_nat_iff_bounded by auto
show "card (φ ` K) = n"
by (metis "1"(1) ‹K ⊆ V› φ bij_betw_same_card bij_betw_subset)
qed
ultimately show ?thesis
by (metis less_2_cases_iff monochromatic_def nth_Cons_0 nth_Cons_Suc)
qed
then show "∃i<length [m,n]. monochromatic {..<r} ([m, n] ! i) 2 f i"
by (simp add: numeral_2_eq_2)
qed
lemma partn_lst_imp_is_clique_RN:
fixes U :: "'a itself"
assumes "partn_lst {..<r} [m,n] 2"
shows "is_clique_RN U m n r"
unfolding is_clique_RN_def
proof (intro strip)
fix V::"'a set" and E ::"'a set set"
assume V: "finite V" "r ≤ card V"
obtain φ where φ: "bij_betw φ {..<card V} V"
using ‹finite V› bij_betw_from_nat_into_finite by blast
define f :: "nat set ⇒ nat" where "f ≡ λe. if φ`e ∈ E then 0 else 1"
have f: "f ∈ nsets {..<r} 2 → {..<2}"
by (simp add: f_def)
obtain i H where "i<2" and H: "H ⊆ {..<r}" "finite H" "card H = [m,n] ! i"
and mono: "f ` (nsets H 2) ⊆ {i}"
using partn_lstE [OF assms f]
by (metis (mono_tags, lifting) length_Cons list.size(3) mem_Collect_eq nsets_def numeral_2_eq_2)
have [simp]: "⋀v w. ⟦v ∈ H; w ∈ H⟧ ⟹ φ v = φ w ⟷ v=w"
using bij_betw_imp_inj_on [OF φ] H
by (meson V(2) inj_on_def inj_on_subset lessThan_subset_iff)
define K where "K ≡ φ ` H"
have [simp]: "⋀v w. ⟦v ∈ K; w ∈ K⟧ ⟹ inv_into {..<card V} φ v = inv_into {..<card V} φ w ⟷ v=w"
using bij_betw_inv_into_right [OF φ] H V φ
by (metis K_def image_mono inv_into_injective lessThan_subset_iff subset_iff)
have "K ⊆ V"
using H φ V bij_betw_imp_surj_on by (fastforce simp: K_def nsets_def)
have [simp]: "card (φ ` H) = card H"
using H by (metis V(2) φ bij_betw_same_card bij_betw_subset lessThan_subset_iff)
consider (0) "i=0" | (1) "i=1"
using ‹i<2› by linarith
then have "clique_indep m n K E"
proof cases
case 0
have "{v, w} ∈ E" if "v ∈ K" and "w ∈ K" and "v ≠ w" for v w
proof -
have *: "{inv_into {..<card V} φ v, inv_into {..<card V} φ w} ∈ [H]⇗2⇖"
using that bij_betw_inv_into_left [OF φ] H(1) V(2)
by (auto simp: nsets_def card_insert_if K_def)
show ?thesis
using 0 ‹K ⊆ V› mono bij_betw_inv_into_right[OF φ] that
apply (simp add: f_def image_subset_iff)
by (metis "*" image_empty image_insert subsetD)
qed
then show ?thesis
unfolding clique_indep_def clique_def
by (simp add: "0" H(3) K_def)
next
case 1
have "{v, w} ∉ E" if "v ∈ K" and "w ∈ K" and "v ≠ w" for v w
proof -
have *: "{inv_into {..<card V} φ v, inv_into {..<card V} φ w} ∈ [H]⇗2⇖"
using that bij_betw_inv_into_left [OF φ] H(1) V(2)
by (auto simp: nsets_def card_insert_if K_def)
show ?thesis
using 1 ‹K ⊆ V› mono bij_betw_inv_into_right[OF φ] that
apply (simp add: f_def image_subset_iff)
by (metis "*" image_empty image_insert subsetD)
qed
then show ?thesis
unfolding clique_indep_def indep_def
by (simp add: "1" H(3) K_def)
qed
with ‹K ⊆ V› show "∃K. K ⊆ V ∧ clique_indep m n K E" by blast
qed
text ‹All complete graphs of a given cardinality are the same›
lemma is_clique_RN_any_type:
assumes "is_clique_RN (U::'a itself) m n r" "infinite (UNIV::'a set)"
shows "is_clique_RN (V::'b::infinite itself) m n r"
by (metis partn_lst_imp_is_clique_RN is_clique_RN_imp_partn_lst assms)
lemma is_Ramsey_number_le:
assumes "is_Ramsey_number m n r" and le: "m' ≤ m" "n' ≤ n"
shows "is_Ramsey_number m' n' r"
using partn_lst_less [where α = "[m,n]" and α' = "[m',n']"] assms
by (force simp: less_Suc_eq)
definition RN where
"RN ≡ λm n. LEAST r. is_Ramsey_number m n r"
lemma is_Ramsey_number_RN: "partn_lst {..< (RN m n)} [m,n] 2"
by (metis LeastI_ex RN_def ramsey2_full)
lemma RN_le: "⟦is_Ramsey_number m n r⟧ ⟹ RN m n ≤ r"
by (simp add: Least_le RN_def)
lemma RN_le_ES: "RN i j ≤ ES 2 i j"
by (simp add: RN_le ramsey2_full)
lemma RN_mono:
assumes "m' ≤ m" "n' ≤ n"
shows "RN m' n' ≤ RN m n"
by (meson RN_le assms is_Ramsey_number_RN is_Ramsey_number_le)
lemma indep_iff_clique [simp]: "K ⊆ V ⟹ indep K (all_edges V - E) ⟷ clique K E"
by (auto simp: clique_def indep_def all_edges_def)
lemma clique_iff_indep [simp]: "K ⊆ V ⟹ clique K (all_edges V - E) ⟷ indep K E"
by (auto simp: clique_def indep_def all_edges_def)
lemma is_Ramsey_number_commute_aux:
assumes "is_Ramsey_number m n r"
shows "is_Ramsey_number n m r"
unfolding partn_lst_def
proof (intro strip)
fix f
assume f: "f ∈ [{..<r}]⇗2⇖ → {..<length [n, m]}"
define f' where "f' ≡ λA. 1 - f A"
then have "f' ∈ [{..<r}]⇗2⇖ → {..<2}"
by (auto simp: f'_def)
then obtain i H where "i<2" and H: "H ∈ [{..<r}]⇗([m,n] ! i)⇖" "f' ` [H]⇗2⇖ ⊆ {i}"
using assms by (auto simp: partn_lst_def monochromatic_def numeral_2_eq_2)
then have "H ⊆ {..<r}"
by (auto simp: nsets_def)
then have fless2: "∀x∈[H]⇗2⇖. f x < Suc (Suc 0)"
using funcset_mem [OF f] nsets_mono by force
show "∃i<length [n, m]. monochromatic {..<r} ([n,m] ! i) 2 f i"
unfolding monochromatic_def
proof (intro exI bexI conjI)
show "f ` [H]⇗2⇖ ⊆ {1-i}"
using H fless2 by (fastforce simp: f'_def)
show "H ∈ [{..<r}]⇗([n, m] ! (1-i))⇖"
using ‹i<2› H by (fastforce simp: less_2_cases_iff f'_def image_subset_iff)
qed auto
qed
subsection ‹Elementary properties of Ramsey numbers›
lemma is_Ramsey_number_commute: "is_Ramsey_number m n r ⟷ is_Ramsey_number n m r"
by (meson is_Ramsey_number_commute_aux)
lemma RN_commute_aux: "RN n m ≤ RN m n"
using RN_le is_Ramsey_number_RN is_Ramsey_number_commute by blast
lemma RN_commute: "RN m n = RN n m"
by (simp add: RN_commute_aux le_antisym)
lemma RN_le_choose: "RN k l ≤ (k+l choose k)"
by (metis ES2_choose ramsey2_full RN_le)
lemma RN_le_choose': "RN k l ≤ (k+l choose l)"
by (metis RN_commute RN_le_choose add.commute)
lemma RN_0 [simp]: "RN 0 m = 0"
unfolding RN_def
proof (intro Least_equality)
show "is_Ramsey_number 0 m 0"
by (auto simp: partn_lst_def monochromatic_def nsets_def)
qed auto
lemma RN_1 [simp]:
assumes "m>0" shows "RN (Suc 0) m = Suc 0"
unfolding RN_def
proof (intro Least_equality)
have [simp]: "[{..<Suc 0}]⇗2⇖ = {}" "[{}]⇗2⇖ = {}"
by (auto simp: nsets_def card_2_iff)
show "is_Ramsey_number (Suc 0) m (Suc 0)"
by (auto simp: partn_lst_def monochromatic_def)
fix i
assume i: "is_Ramsey_number (Suc 0) m i"
show "i ≥ Suc 0"
proof (cases "i=0")
case True
with i assms show ?thesis
by (auto simp: partn_lst_def monochromatic_def nsets_empty_iff less_Suc_eq)
qed auto
qed
lemma RN_0' [simp]: "RN m 0 = 0" and RN_1' [simp]: "m>0 ⟹ RN m (Suc 0) = Suc 0"
using RN_1 RN_commute by auto
lemma is_clique_RN_2: "is_clique_RN TYPE(nat) 2 m m"
unfolding is_clique_RN_def
proof (intro strip)
fix V :: "'a set" and E
assume "finite V"
and "m ≤ card V"
show "∃K. K ⊆ V ∧ clique_indep 2 m K E"
proof (cases "∃K. K ⊆ V ∧ card K = 2 ∧ clique K E")
case False
then have "indep V E"
apply (clarsimp simp: clique_def indep_def card_2_iff)
by (smt (verit, best) doubleton_eq_iff insert_absorb insert_iff subset_iff)
then show ?thesis
unfolding clique_indep_def
by (meson ‹m ≤ card V› card_Ex_subset smaller_indep)
qed (metis clique_indep_def)
qed
lemma RN_2 [simp]:
shows "RN 2 m = m"
proof (cases "m>1")
case True
show ?thesis
unfolding RN_def
proof (intro Least_equality)
show "is_Ramsey_number 2 m m"
using is_clique_RN_imp_partn_lst is_clique_RN_2 by blast
fix i
assume "is_Ramsey_number 2 m i"
then have i: "is_clique_RN TYPE(nat) 2 m i"
using partn_lst_imp_is_clique_RN by blast
obtain V :: "nat set" where V: "card V = i" "finite V"
by force
show "i ≥ m"
proof (cases "i<m")
case True
then have "¬ (∃K⊆V. card K = 2 ∧ clique K {})"
by (auto simp: clique_def card_2_iff')
with i V True show ?thesis
unfolding is_clique_RN_def clique_indep_def by (metis card_mono dual_order.refl)
qed auto
qed
next
case False
then show ?thesis
by (metis RN_0' RN_1' Suc_1 less_2_cases_iff not_less_eq)
qed
lemma RN_2' [simp]:
shows "RN m 2 = m"
using RN_2 RN_commute by force
lemma RN_3plus:
assumes "k ≥ 3"
shows "RN k m ≥ m"
proof -
have "RN 2 m = m"
using assms by auto
with RN_mono[of 2 k m m] assms show ?thesis
by force
qed
lemma RN_3plus':
assumes "k ≥ 3"
shows "RN m k ≥ m"
using RN_3plus RN_commute assms by presburger
lemma clique_iff: "F ⊆ all_edges K ⟹ clique K F ⟷ F = all_edges K"
by (auto simp: clique_def all_edges_def card_2_iff)
lemma indep_iff: "F ⊆ all_edges K ⟹ indep K F ⟷ F = {}"
by (auto simp: indep_def all_edges_def card_2_iff)
lemma all_edges_empty_iff: "all_edges K = {} ⟷ (∃v. K ⊆ {v})"
using clique_iff [OF empty_subsetI] by (metis clique_def empty_iff singleton_iff subset_iff)
lemma Ramsey_number_zero: "¬ is_Ramsey_number (Suc m) (Suc n) 0"
by (metis RN_1 RN_le is_Ramsey_number_le not_one_le_zero Suc_le_eq One_nat_def zero_less_Suc)
subsection ‹The product lower bound›
lemma Ramsey_number_times_lower: "¬ is_clique_RN (TYPE(nat*nat)) (Suc m) (Suc n) (m*n)"
proof
define edges where "edges ≡ {{(x,y),(x',y)}| x x' y. x<m ∧ x'<m ∧ y<n}"
assume "is_clique_RN (TYPE(nat*nat)) (Suc m) (Suc n) (m*n)"
then obtain K where K: "K ⊆ {..<m} × {..<n}" and "clique_indep (Suc m) (Suc n) K edges"
unfolding is_clique_RN_def
by (metis card_cartesian_product card_lessThan finite_cartesian_product finite_lessThan le_refl)
then consider "card K = Suc m ∧ clique K edges" | "card K = Suc n ∧ indep K edges"
by (meson clique_indep_def)
then show False
proof cases
case 1
then have "inj_on fst K" "fst ` K ⊆ {..<m}"
using K by (auto simp: inj_on_def clique_def edges_def doubleton_eq_iff)
then have "card K ≤ m"
by (metis card_image card_lessThan card_mono finite_lessThan)
then show False
by (simp add: "1")
next
case 2
then have snd_eq: "snd u ≠ snd v" if "u ∈ K" "v ∈ K" "u ≠ v" for u v
using that K unfolding edges_def indep_def
by (smt (verit, best) lessThan_iff mem_Collect_eq mem_Sigma_iff prod.exhaust_sel subsetD)
then have "inj_on snd K"
by (meson inj_onI)
moreover have "snd ` K ⊆ {..<n}"
using comp_sgraph.wellformed K by auto
ultimately show False
by (metis "2" Suc_n_not_le_n card_inj_on_le card_lessThan finite_lessThan)
qed
qed
theorem RN_times_lower:
shows "RN (Suc m) (Suc n) > m*n"
by (metis partn_lst_imp_is_clique_RN Ramsey_number_times_lower is_Ramsey_number_RN
partn_lst_greater_resource linorder_le_less_linear)
corollary RN_times_lower':
shows "⟦m>0; n>0⟧ ⟹ RN m n > (m-1)*(n-1)"
using RN_times_lower gr0_conv_Suc by force
lemma RN_eq_0_iff: "RN m n = 0 ⟷ m=0 ∨ n=0"
by (metis RN_0 RN_0' RN_times_lower' gr0I not_less_zero)
lemma RN_gt1:
assumes "2 ≤ k" "3 ≤ l" shows "k < RN k l"
using RN_times_lower' [of k l] RN_3plus'[of l k] assms
apply (simp add: eval_nat_numeral)
by (metis Suc_le_eq Suc_pred leD n_less_n_mult_m nat_less_le zero_less_diff)
lemma RN_gt2:
assumes "2 ≤ k" "3 ≤ l" shows "k < RN l k"
by (simp add: RN_commute assms RN_gt1)
subsection ‹A variety of upper bounds, including a stronger Erdős--Szekeres›
lemma RN_1_le: "RN (Suc 0) l ≤ Suc 0"
by (metis RN_0' RN_1 gr_zeroI le_cases less_imp_le)
lemma is_Ramsey_number_add:
assumes "i>1" "j>1"
and n1: "is_Ramsey_number (i - 1) j n1"
and n2: "is_Ramsey_number i (j - 1) n2"
shows "is_Ramsey_number i j (n1+n2)"
proof -
have "partn_lst {..<Suc (n1 + n2 - 1)} [i, j] (Suc (Suc 0))"
using ramsey_induction_step [of n1 i j 1 n2 "n1+n2-1"] ramsey1_explicit assms
by (simp add: numeral_2_eq_2)
moreover have "n1>0"
using assms
by (metis Ramsey_number_zero Suc_pred' gr0I not_less_iff_gr_or_eq zero_less_diff)
ultimately show ?thesis
by (metis One_nat_def Suc_1 Suc_pred' add_gr_0)
qed
lemma RN_le_add_RN_RN:
assumes "i>1" "j>1"
shows "RN i j ≤ RN (i - Suc 0) j + RN i (j - Suc 0)"
using is_Ramsey_number_add RN_le assms is_Ramsey_number_RN
by simp
text ‹Cribbed from Bhavik Mehta›
lemma RN_le_choose_strong: "RN k l ≤ (k + l - 2) choose (k - 1)"
proof (induction n ≡ "k+l" arbitrary: k l)
case 0
then show ?case
by simp
next
case (Suc n)
have *: "RN k l ≤ k + l - 2 choose (k - 1)" if "k ≤ Suc 0"
using that by (metis One_nat_def RN_1_le RN_le_choose Suc_pred binomial_n_0 neq0_conv diff_is_0_eq')
show ?case
proof (cases "k ≤ Suc 0 ∨ l ≤ Suc 0")
case True
with * show ?thesis
using le_Suc_eq by fastforce
next
case False
then have 2: "k > 1" "l > 1"
by auto
have "RN (k - Suc 0) l ≤ k - Suc 0 + l - 2 choose (k - Suc 0 - Suc 0)"
by (metis False Nat.add_diff_assoc2 One_nat_def Suc diff_Suc_1 nat_le_linear)
moreover
have "RN k (l - Suc 0) ≤ k - Suc 0 + l - 2 choose (k - Suc 0)"
by (metis False Nat.diff_add_assoc2 Suc diff_Suc_1 nat_le_linear One_nat_def diff_add_assoc)
ultimately
show ?thesis
using RN_le_add_RN_RN [OF 2] 2 by (simp add: choose_reduce_nat eval_nat_numeral)
qed
qed
lemma RN_le_power2: "RN i j ≤ 2 ^ (i+j-2)"
by (meson RN_le_choose_strong binomial_le_pow2 le_trans)
lemma RN_le_power4: "RN i i ≤ 4 ^ (i-1)"
proof -
have "(i + i - 2) = 2 * (i-1)"
by simp
then show ?thesis
using RN_le_power2 [of i i] by (simp add: power_mult)
qed
text ‹Bhavik Mehta again›
lemma RN_le_argpower: "RN i j ≤ j ^ (i-1)"
proof (cases "i=0 ∨ j=0")
case True
then show ?thesis
by auto
next
case False
then show ?thesis
using RN_le_choose_strong [of i j] add_choose_le_power[of "i-1" "j-1"]
by (simp add: numeral_2_eq_2)
qed
lemma RN_le_argpower': "RN j i ≤ j ^ (i-1)"
using RN_commute RN_le_argpower by presburger
subsection ‹Probabilistic lower bounds: the main theorem and applications›
text ‹General probabilistic setup, omitting the actual probability calculation.
Andrew Thomason's proof (private communication)›
theorem Ramsey_number_lower_gen:
fixes n k::nat and p::real
assumes n: "(n choose k) * p ^ (k choose 2) + (n choose l) * (1 - p) ^ (l choose 2) < 1"
assumes p01: "0<p" "p<1"
shows "¬ is_Ramsey_number k l n"
proof
assume con: "is_Ramsey_number k l n"
define W where "W ≡ {..<n}"
have "finite W" and cardW: "card W = n"
by (auto simp: W_def)
define Ω :: "(nat set ⇒ nat) set" where "Ω ≡ (all_edges W) →⇩E {..<2}"
have cardΩ: "card Ω = 2 ^ (n choose 2)"
by (simp add: Ω_def ‹finite W› W_def card_all_edges card_funcsetE finite_all_edges)
define coloured where "coloured ≡ λF. λf::nat set ⇒ nat. λc. {e ∈ F. f e = c}"
have finite_coloured[simp]: "finite (coloured F f c)" if "finite F" for f c F
using coloured_def that by auto
define pr where "pr ≡ λF f. p ^ card (coloured F f 0) * (1-p) ^ card (coloured F f 1)"
have pr01: "0 < pr U f" "pr U f ≤ 1" for U f
using ‹0<p› ‹p<1› by (auto simp: mult_le_one power_le_one pr_def cardΩ)
define M where "M ≡ point_measure Ω (pr (all_edges W))"
have space_eq: "space M = Ω"
by (simp add: M_def space_point_measure)
have sets_eq: "sets M = Pow Ω"
by (simp add: M_def sets_point_measure)
have fin_Ω[simp]: "finite Ω"
by (simp add: Ω_def finite_PiE ‹finite W› finite_all_edges)
have coloured_insert:
"coloured (insert e F) f c = (if f e = c then insert e (coloured F f c) else coloured F f c)"
for f e c F
by (auto simp: coloured_def)
have eq2: "{..<2} = {0, Suc 0}"
by (simp add: insert_commute lessThan_Suc numeral_2_eq_2)
have sum_pr_1 [simp]: "sum (pr U) (U →⇩E {..<2}) = 1" if "finite U" for U
using that
proof (induction U)
case empty
then show ?case
by (simp add: pr_def coloured_def)
next
case (insert e F)
then have [simp]: "e ∉ coloured F f c" "coloured F (f(e := c)) c' = coloured F f c'" for f c c'
by (auto simp: coloured_def)
have inj: "inj_on (λ(y, g). g(e := y)) ({..<2} × (F →⇩E {..<2}))"
using ‹e ∉ F› by (fastforce simp: inj_on_def fun_eq_iff)
show ?case
using insert
apply (simp add: pr_def coloured_insert PiE_insert_eq sum.reindex [OF inj] sum.cartesian_product')
apply (simp add: eq2 mult_ac flip: sum_distrib_left)
done
qed
interpret P: prob_space M
proof
have "sum (pr (all_edges W)) Ω = 1"
using Ω_def sum_pr_1 ‹finite W› finite_all_edges by blast
with pr01 show "emeasure M (space M) = 1"
unfolding M_def
by (metis fin_Ω prob_space.emeasure_space_1 prob_space_point_measure zero_le
ennreal_1 linorder_not_less nle_le sum_ennreal)
qed
define mono where "mono ≡ λc K. {f ∈ Ω. all_edges K ⊆ coloured (all_edges W) f c}"
have mono_ev: "mono c K ∈ P.events" if "c<2" for K c
by (auto simp: sets_eq mono_def Ω_def)
have mono_sub_Ω: "mono c K ⊆ Ω" if "c<2" for K c
using mono_ev sets_eq that by auto
have emeasure_eq: "emeasure M C = (if C ⊆ Ω then (∑a∈C. ennreal (pr (all_edges W) a)) else 0)" for C
by (simp add: M_def emeasure_notin_sets emeasure_point_measure_finite sets_point_measure)
define pc where "pc ≡ λc::nat. if c=0 then p else 1-p"
have pc0: "0 ≤ pc c" for c
using p01 pc_def by auto
have coloured_upd: "coloured F (λl∈F. if l ∈ G then c else f l) c'
= (if c=c' then G ∪ coloured (F-G) f c' else coloured (F-G) f c')" if "G ⊆ F" for F G f c c'
using that by (auto simp: coloured_def)
have prob_mono: "P.prob (mono c K) = pc c ^ (r choose 2)"
if "K ∈ nsets W r" "c<2" for r K c
proof -
let ?EWK = "all_edges W - all_edges K"
have §: "K ⊆ W" "finite K" "card K = r"
using that by (auto simp: nsets_def)
have *: "{f ∈ Ω. all_edges K ⊆ coloured (all_edges W) f c} =
(⋃g ∈ ?EWK →⇩E {..<2}. {λl ∈ all_edges W. if l ∈ all_edges K then c else g l})"
(is "?L = ?R")
proof
have "∃g∈?EWK →⇩E {..<2}. f = (λl∈all_edges W. if l ∈ all_edges K then c else g l)"
if f: "f ∈ Ω" and c: "all_edges K ⊆ coloured (all_edges W) f c" for f
using that
apply (intro bexI [where x="restrict f ?EWK"])
apply (force simp: Ω_def coloured_def subset_iff)+
done
then show "?L ⊆ ?R" by auto
show "?R ⊆ ?L"
using that all_edges_mono[OF ‹K ⊆ W›] by (auto simp: coloured_def Ω_def nsets_def PiE_iff)
qed
have [simp]: "card (all_edges K ∪ coloured ?EWK f c)
= (r choose 2) + card (coloured ?EWK f c)" for f c
using § ‹finite W›
by (subst card_Un_disjoint) (auto simp: finite_all_edges coloured_def card_all_edges)
have pr_upd: "pr (all_edges W) (λl ∈ all_edges W. if l ∈ all_edges K then c else f l)
= pc c ^ (r choose 2) * pr ?EWK f"
if "f ∈ ?EWK →⇩E {..<2}" for f
using that all_edges_mono[OF ‹K ⊆ W›] p01 ‹c<2› §
by (simp add: pr_def coloured_upd pc_def power_add)
have "emeasure M (mono c K) = (∑f ∈ mono c K. ennreal (pr (all_edges W) f))"
using that by (simp add: emeasure_eq mono_sub_Ω)
also have "… = (∑f∈(⋃g∈?EWK →⇩E {..<2}.
{λe∈all_edges W. if e ∈ all_edges K then c else g e}).
ennreal (pr (all_edges W) f))"
by (simp add: mono_def *)
also have "… = (∑g∈?EWK →⇩E {..<2}.
∑f∈{λe∈all_edges W. if e ∈ all_edges K then c else g e}.
ennreal (pr (all_edges W) f))"
proof (rule sum.UNION_disjoint_family)
show "finite (?EWK →⇩E {..<2::nat})"
by (simp add: ‹finite W› finite_PiE finite_all_edges)
show "disjoint_family_on (λg. {λe∈all_edges W. if e ∈ all_edges K then c else g e}) (?EWK →⇩E {..<2})"
apply (simp add: disjoint_family_on_def fun_eq_iff)
by (metis DiffE PiE_E)
qed auto
also have "… = (∑x∈?EWK →⇩E {..<2}. ennreal (pc c ^ (r choose 2) * pr ?EWK x))"
by (simp add: pr_upd)
also have "… = ennreal (∑f∈?EWK →⇩E {..<2}.
pc c ^ (r choose 2) * pr ?EWK f)"
using pr01 pc0 sum.cong sum_ennreal by (smt (verit) mult_nonneg_nonneg zero_le_power)
also have "… = ennreal (pc c ^ (r choose 2))"
by (simp add: ‹finite W› finite_all_edges flip: sum_distrib_left)
finally have "emeasure M (mono c K) = ennreal (pc c ^ (r choose 2))" .
then show ?thesis
using p01 that by (simp add: measure_eq_emeasure_eq_ennreal pc_def)
qed
define Reds where "Reds ≡ (⋃K ∈ nsets W k. mono 0 K)"
define Blues where "Blues ≡ (⋃K ∈ nsets W l. mono 1 K)"
have Uev: "⋃ (mono c ` [W]⇗r⇖) ∈ P.events" for c r
by (simp add: local.mono_def sets_eq subset_iff)
then have "Reds ∈ P.events" "Blues ∈ P.events"
by (auto simp: Reds_def Blues_def)
have prob_0: "P.prob Reds ≤ (n choose k) * (p ^ (k choose 2))"
proof -
have "P.prob Reds ≤ (∑K ∈ nsets W k. P.prob (mono 0 K))"
by (simp add: Reds_def ‹finite W› finite_imp_finite_nsets measure_UNION_le mono_ev)
also have "… ≤ (n choose k) * (p ^ (k choose 2))"
by (simp add: prob_mono pc_def cardW)
finally show ?thesis .
qed
moreover
have prob_1: "P.prob Blues ≤ (n choose l) * ((1-p) ^ (l choose 2))"
proof -
have "P.prob Blues ≤ (∑K ∈ nsets W l. P.prob (mono 1 K))"
by (simp add: Blues_def ‹finite W› finite_imp_finite_nsets measure_UNION_le mono_ev)
also have "… ≤ (n choose l) * ((1-p) ^ (l choose 2))"
by (simp add: prob_mono pc_def cardW)
finally show ?thesis .
qed
ultimately have "P.prob (Reds ∪ Blues) < 1"
using P.finite_measure_subadditive ‹Blues ∈ P.events› ‹Reds ∈ P.events› n
by fastforce
with P.prob_space Uev sets_eq obtain F where F: "F ∈ Ω - (Reds ∪ Blues)"
unfolding Reds_def Blues_def space_eq
by (smt (verit, del_insts) Pow_iff Un_subset_iff equalityI Diff_iff subset_iff)
have False if "i < 2" "H ∈ [W]⇗([k, l] ! i)⇖" "F ` [H]⇗2⇖ ⊆ {i}" for i H
proof -
have "¬ all_edges H ⊆ {e ∈ all_edges W. F e = 0}" "¬ all_edges H ⊆ {e ∈ all_edges W. F e = 1}"
using F that
by (auto simp: less_2_cases_iff nsets2_eq_all_edges Ω_def Reds_def Blues_def mono_def coloured_def image_subset_iff)
moreover have "H ⊆ W"
using that by (auto simp: nsets_def)
ultimately show False
using that all_edges_mono [OF ‹H ⊆ W›] by (auto simp: less_2_cases_iff nsets2_eq_all_edges)
qed
moreover have "F ∈ [{..<n}]⇗2⇖ → {..<2}"
using F by (auto simp: W_def Ω_def nsets2_eq_all_edges)
ultimately show False
using con by (force simp: W_def partn_lst_def monochromatic_def numeral_2_eq_2)
qed
text ‹Andrew's calculation for the Ramsey lower bound. Symmetric, so works for both colours›
lemma Ramsey_lower_calc:
fixes s::nat and t::nat and p::real
assumes "s ≥ 3" "t ≥ 3" "n > 4"
and n: "real n ≤ exp ((real s - 1) * (real t - 1) / (2*(s+t)))"
defines "p ≡ real s / (real s + real t)"
shows "(n choose s) * p ^ (s choose 2) < 1/2"
proof -
have p01: "0<p" "p<1"
using assms by (auto simp: p_def)
have "exp ((real s - 1) * (real t - 1) / (2*(s+t))) ≤ exp (t / (s+t)) powr ((s-1)/2)"
using ‹s ≥ 3› by (simp add: mult_ac divide_simps of_nat_diff exp_powr_real)
with assms p01 have "n ≤ exp (t / (s+t)) powr ((s-1)/2)"
by linarith
then have "n * p powr ((s-1)/2) ≤ (exp (t / (s+t)) * p) powr ((s-1)/2)"
using ‹0<p› by (simp add: powr_mult)
also have "… < 1"
proof -
have "exp (real t / real (s+t)) * p < 1"
proof -
have "p = 1 - t / (s+t)"
using assms by (simp add: p_def divide_simps)
also have "… < exp (- real t / real (s+t))"
using assms by (simp add: exp_minus_greater)
finally show ?thesis
by (simp add: exp_minus divide_simps mult.commute)
qed
then show ?thesis
using powr01_less_one assms(1) p01(1) by auto
qed
finally have "n * p powr ((s-1)/2) < 1" .
then have "(n * p powr ((s-1)/2)) ^ s < 1"
using ‹s ≥ 3› by (simp add: power_less_one_iff)
then have B: "n^s * p ^ (s choose 2) < 1"
using ‹0<p› ‹4 < n› ‹s ≥ 3›
by (simp add: choose_two_real powr_powr powr_mult of_nat_diff mult.commute flip: powr_realpow)
have "(n choose s) * p ^ (s choose 2) ≤ n^s / fact s * p ^ (s choose 2)"
proof (intro mult_right_mono)
show "real (n choose s) ≤ real (n ^ s) / fact s"
using binomial_fact_pow[of n s] of_nat_mono
by (fastforce simp: divide_simps mult.commute)
qed (use p01 in auto)
also have "… < 1 / fact s"
using B by (simp add: divide_simps)
also have "… ≤ 1/2"
by (smt (verit, best) One_nat_def Suc_1 Suc_leD assms fact_2 fact_mono frac_less2 numeral_3_eq_3)
finally show ?thesis .
qed
text ‹Andrew Thomason's specific example›
corollary Ramsey_number_lower_off_diag:
fixes n k::nat
assumes "k ≥ 3" "l ≥ 3" and n: "real n ≤ exp ((real k - 1) * (real l - 1) / (2*(k+l)))"
shows "¬ is_Ramsey_number k l n"
proof
assume con: "is_Ramsey_number k l n"
then have "(k - 1) * (l - 1) < n"
using RN_times_lower' [of k l] assms by (metis RN_le numeral_3_eq_3 order_less_le_trans zero_less_Suc)
moreover have "2*2 ≤ (k - 1) * (l - 1)"
using assms by (intro mult_mono) auto
ultimately have "n > 4"
by simp
define p where "p ≡ k / (k+l)"
have p01: "0<p" "p<1"
using assms by (auto simp: p_def)
have "real (n choose k) * p ^ (k choose 2) < 1/2"
using Ramsey_lower_calc ‹4 < n› assms n p_def by auto
moreover
have "1-p = real l / (real l + real k)"
using ‹k ≥ 3› by (simp add: p_def divide_simps)
with assms have "(n choose l) * (1-p) ^ (l choose 2) < 1/2"
by (metis Ramsey_lower_calc add.commute mult.commute ‹4 < n›)
ultimately show False
using con Ramsey_number_lower_gen p01 by force
qed
theorem RN_lower_off_diag:
assumes "s ≥ 3" "t ≥ 3"
shows "RN s t > exp ((real s - 1) * (real t - 1) / (2*(s+t)))"
using Ramsey_number_lower_off_diag [OF assms] is_Ramsey_number_RN by force
text ‹The original Ramsey number lower bound, by Erdős›
proposition Ramsey_number_lower:
fixes n s::nat
assumes "s ≥ 3" and n: "real n ≤ 2 powr (s/2)"
shows "¬ is_Ramsey_number s s n"
proof
assume con: "is_Ramsey_number s s n"
then have "s ≤ n"
using RN_3plus' RN_le assms(1) le_trans by blast
have "s > 1" using assms by arith
have "n>0"
using ‹1 < s› ‹s ≤ n› by linarith
have "(n choose s) ≤ n^s / fact s"
using binomial_fact_pow[of n s]
by (smt (verit) fact_gt_zero of_nat_fact of_nat_mono of_nat_mult pos_divide_less_eq)
then have "(n choose s) * (2 / 2^(s choose 2)) ≤ 2 * n^s / (fact s * 2 ^ (s * (s-1) div 2))"
by (simp add: choose_two divide_simps)
also have "… ≤ 2 powr (1 + s/2) / fact s"
proof -
have [simp]: "real (s * (s - Suc 0) div 2) = real s * (real s - 1) / 2"
by (subst real_of_nat_div) auto
have "n powr s ≤ (2 powr (s/2)) powr s"
using n by (simp add: powr_mono2)
then have "n powr s ≤ 2 powr (s * s / 2)"
using ‹n>0› assms by (simp add: power2_eq_square powr_powr)
then have "2 * n powr s ≤ 2 powr ((2 + s * s) / 2)"
by (simp add: add_divide_distrib powr_add)
then show ?thesis
using n ‹n>0› by (simp add: divide_simps flip: powr_realpow powr_add) argo
qed
also have "… < 1"
proof -
have "2 powr (1 + (k+3)/2) < fact (k+3)" for k
proof (induction k)
case 0
have "2 powr (5/2) = sqrt (2^5)"
by (simp add: powr_half_sqrt_powr)
also have "… < sqrt 36"
by (intro real_sqrt_less_mono) auto
finally show ?case
by (simp add: eval_nat_numeral)
next
case (Suc k)
have "2 powr (1 + real (Suc k + 3) / 2) = 2 powr (1/2) * 2 powr (1 + (k+3)/2)"
by (simp add: powr_add powr_half_sqrt_powr flip: real_sqrt_mult)
also have "… ≤ sqrt 2 * fact (k+3)"
using Suc.IH by (simp add: powr_half_sqrt)
also have "… < real(k + 4) * fact (k + 3)"
using sqrt2_less_2 by simp
also have "… = fact (Suc (k + 3))"
unfolding fact_Suc by simp
finally show ?case by simp
qed
then have "2 powr (1 + s/2) < fact s"
by (metis add.commute ‹s≥3› le_Suc_ex)
then show ?thesis
by (simp add: divide_simps)
qed
finally have less_1: "real (n choose s) * (2 / 2 ^ (s choose 2)) < 1" .
then have "¬ is_Ramsey_number s s n"
by (intro Ramsey_number_lower_gen [where p="1/2"]) (auto simp: power_one_over)
with con show False by blast
qed
theorem RN_lower:
assumes "k ≥ 3"
shows "RN k k > 2 powr (k/2)"
using Ramsey_number_lower assms is_Ramsey_number_RN by force
text ‹and trivially, off the diagonal too›
corollary RN_lower_nodiag:
assumes "k ≥ 3" "l ≥ k"
shows "RN k l > 2 powr (k/2)"
by (meson RN_lower RN_mono assms less_le_trans le_refl of_nat_mono)
lemma powr_half_ge:
fixes x::real
assumes "x≥4"
shows "x ≤ 2 powr (x/2)"
proof -
define f where "f ≡ λx::real. 2 powr (x/2) - x"
have "f 4 ≤ f x"
proof (intro DERIV_nonneg_imp_nondecreasing[of concl: f] exI conjI assms)
show "(f has_real_derivative ln 2 * (2 powr (y/2 - 1)) - 1) (at y)" for y
unfolding f_def by (rule derivative_eq_intros refl | simp add: powr_diff)+
show "ln 2 * (2 powr (y/2 - 1)) - 1 ≥ 0" if "4 ≤ y" for y::real
proof -
have "1 ≤ ln 2 * 2 powr ((4 - 2) / (2::real))"
using ln2_ge_two_thirds by simp
also have "… ≤ ln 2 * (2 powr (y/2 - 1))"
using that by (intro mult_left_mono powr_mono) auto
finally show ?thesis by simp
qed
qed
moreover have "f 4 = 0" by (simp add: f_def)
ultimately show ?thesis
by (simp add: f_def)
qed
corollary RN_lower_self:
assumes "k ≥ 3"
shows "RN k k > k"
proof (cases "k=3")
case False
with assms have "k≥4" by linarith
then have "k ≤ 2 powr (k/2)"
using powr_half_ge numeral_le_real_of_nat_iff by blast
also have "… < RN k k"
using assms by (intro RN_lower) auto
finally show ?thesis
by fastforce
qed (simp add: RN_gt2)
end