Theory 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)
  ― ‹Easier to represent the state as maps from edges to colours, not sets of coloured edges›
   ―‹colour the edges randomly›
  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 ― ‹the inequality could be strict›
    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
  ―‹the event to avoid: monochromatic cliques, given @{term "K ⊆ W"};
      we are considering edges over the entire graph @{term W}›
  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"  ― ‹probability calculation›
    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