Theory Red_Steps

section ‹Red Steps: theorems›

theory Red_Steps imports Big_Blue_Steps

begin

text ‹Bhavik Mehta: choose-free Ramsey lower bound that's okay for very small @{term p}›
lemma Ramsey_number_lower_simple: 
  fixes p::real
  assumes n: "n^k * p powr (k^2 / 4) + n^l * exp (-p * l^2 / 4) < 1"
  assumes p01: "0<p" "p<1" and "k>1" "l>1"
  shows "¬ is_Ramsey_number k l n"
proof (rule Ramsey_number_lower_gen)
  have "(n choose k) * p^(k choose 2) ≤ n^k * p powr (real k^2 / 4)"
  proof -
    have "(n choose k) * p^(k choose 2) ≤ real (Suc n - k)^k * p^(k choose 2)"
      using choose_le_power p01 by simp
    also have "… = real (Suc n - k)^k * p powr (k * (real k - 1) / 2)"
      by (metis choose_two_real p01(1) powr_realpow)
    also have "… ≤ n^k * p powr (real k^2 / 4)"
      using p01 ‹k>1› by (intro mult_mono powr_mono') (auto simp: power2_eq_square)
    finally show ?thesis .
  qed
  moreover
  have "real (n choose l) * (1 - p)^(l choose 2) ≤ n^l * exp (-p * real l^2 / 4)"
  proof -
    show ?thesis
    proof (intro mult_mono)
      show "real (n choose l) ≤ n^l"
        by (metis binomial_eq_0_iff binomial_le_pow not_le of_nat_le_iff zero_le)
      have "l * p ≤ 2 * (1 - real l) * -p"
        using assms by (auto simp: algebra_simps)
      also have "… ≤ 2 * (1 - real l) * ln (1-p)"
        using p01 ‹l>1› ln_add_one_self_le_self2 [of "-p"]
        by (intro mult_left_mono_neg) auto
      finally have "real l * (real l * p) ≤ real l * (2 * (1 - real l) * ln (1-p))"
        using mult_left_mono ‹l>1› by fastforce
      with p01 show "(1 - p)^(l choose 2) ≤ exp (- p * (real l)⇧2 / 4)"
        by (simp add: field_simps power2_eq_square powr_def choose_two_real flip: powr_realpow)
    qed (use p01 in auto)
  qed
  ultimately
  show "real (n choose k) * p^(k choose 2) + real (n choose l) * (1 - p)^(l choose 2) < 1"
    using n by auto
qed (use p01 in auto)


context Book
begin

subsection ‹Density-boost steps›

subsubsection ‹Observation 5.5›

lemma sum_Weight_ge0:
  assumes "X ⊆ V" "Y ⊆ V" "disjnt X Y"
  shows "(∑x∈X. ∑x'∈X. Weight X Y x x') ≥ 0"
proof -
  have "finite X" "finite Y"
    using assms finV finite_subset by blast+
  with Red_E have EXY: "edge_card Red X Y = (∑x∈X. card (Neighbours Red x ∩ Y))"
    by (metis ‹disjnt X Y› disjnt_sym edge_card_commute edge_card_eq_sum_Neighbours)
  have "(∑x∈X. ∑x'∈X. red_density X Y * card (Neighbours Red x ∩ Y))
       = red_density X Y * card X * edge_card Red X Y"
    using assms Red_E
    by (simp add: EXY power2_eq_square edge_card_eq_sum_Neighbours flip: sum_distrib_left)
  also have "… = red_density X Y^2 * card X^2 * card Y"
    by (simp add: power2_eq_square gen_density_def)
  also have "… = ((∑i∈Y. card (Neighbours Red i ∩ X)) / (real (card X) * real (card Y)))⇧2 * (card X)⇧2 * card Y"
    using Red_E ‹finite Y› assms
    by (simp add: psubset_eq gen_density_def edge_card_eq_sum_Neighbours)
  also have "… ≤ (∑y∈Y. real ((card (Neighbours Red y ∩ X))⇧2))"
  proof (cases "card Y = 0")
    case False
    then have "(∑x∈Y. real (card (Neighbours Red x ∩ X)))⇧2
            ≤ (∑y∈Y. (real (card (Neighbours Red y ∩ X)))⇧2) * card Y"
      using sum_squared_le_sum_of_squares by blast
    then show ?thesis 
      using assms False by (simp add: divide_simps power2_eq_square sum_nonneg)
  qed (auto simp: sum_nonneg)
  also have "… = (∑x∈X. ∑x'∈X. real (card (Neighbours Red x ∩ Neighbours Red x' ∩ Y)))"
  proof -
    define f::"'a × 'a × 'a ⇒ 'a × 'a × 'a" where "f ≡ λ(y,(x,x')). (x, (x', y))"
    have f: "bij_betw f (SIGMA y:Y. (Neighbours Red y ∩ X) × (Neighbours Red y ∩ X))
                        (SIGMA x:X. SIGMA x':X. Neighbours Red x ∩ Neighbours Red x' ∩ Y)"
      by (auto simp: f_def bij_betw_def inj_on_def image_iff in_Neighbours_iff doubleton_eq_iff insert_commute)
    have "(∑y∈Y. (card (Neighbours Red y ∩ X))⇧2) = card(SIGMA y:Y. (Neighbours Red y ∩ X) × (Neighbours Red y ∩ X))"
      by (simp add: ‹finite Y› finite_Neighbours power2_eq_square)
    also have "… = card(Sigma X (λx. Sigma X (λx'. Neighbours Red x ∩ Neighbours Red x' ∩ Y)))"
      using bij_betw_same_card f by blast
    also have "… = (∑x∈X. ∑x'∈X. card (Neighbours Red x ∩ Neighbours Red x' ∩ Y))"
      by (simp add: ‹finite X› finite_Neighbours power2_eq_square)
    finally
    have "(∑y∈Y. (card (Neighbours Red y ∩ X))⇧2) =
          (∑x∈X. ∑x'∈X. card (Neighbours Red x ∩ Neighbours Red x' ∩ Y))" .
    then show ?thesis
      by (simp flip: of_nat_sum of_nat_power)
  qed
  finally have "(∑x∈X. ∑y∈X. red_density X Y * card (Neighbours Red x ∩ Y))
      ≤ (∑x∈X. ∑y∈X. real (card (Neighbours Red x ∩ Neighbours Red y ∩ Y)))" .
  then show ?thesis
    by (simp add: Weight_def sum_subtractf inverse_eq_divide flip: sum_divide_distrib)
qed

end

subsubsection ‹Lemma 5.6›

definition "Big_Red_5_6_Ramsey ≡ 
      λc l. nat ⌈real l powr (3/4)⌉ ≥ 3
          ∧ (l powr (3/4) * (c - 1/32) ≤ -1) 
          ∧ (∀k≥l. k * (c * l powr (3/4) * ln k - k powr (7/8) / 4) ≤ -1)"

text ‹establishing the size requirements for 5.6›
lemma Big_Red_5_6_Ramsey:
  assumes "0<c" "c<1/32"
  shows "∀⇧∞l. Big_Red_5_6_Ramsey c l"
proof -
  have D34: "⋀l k. l ≤ k ⟹ c * real l powr (3/4) ≤ c * real k powr (3/4)"
    by (simp add: assms powr_mono2)
  have D0: "∀⇧∞l. l * (c * l powr (3/4) * ln l - l powr (7/8) / 4) ≤ -1"
    using ‹c>0› by real_asymp
  have "⋀l k. l ≤ k ⟹ c * real l powr (3/4) * ln k ≤ c * real k powr (3/4) * ln k"
    using D34 le_eq_less_or_eq mult_right_mono by fastforce
  then have D: "∀⇧∞l. ∀k≥l. k * (c * l powr (3/4) * ln k - real k powr (7/8) / 4) ≤ -1"
    using eventually_mono [OF eventually_all_ge_at_top [OF D0]]
    by (smt (verit, ccfv_SIG) mult_left_mono of_nat_0_le_iff)
  show ?thesis
    using assms
    unfolding Big_Red_5_6_Ramsey_def eventually_conj_iff m_of_def
    by (intro conjI eventually_all_ge_at_top D; real_asymp)
qed

lemma Red_5_6_Ramsey:
  assumes "0<c" "c<1/32" and "l≤k" and big: "Big_Red_5_6_Ramsey c l"
  shows "exp (c * l powr (3/4) * ln k) ≤ RN k (nat⌈l powr (3/4)⌉)"
proof -
  define r where "r ≡ nat ⌊exp (c * l powr (3/4) * ln k)⌋"
  define s where "s ≡ nat ⌈l powr (3/4)⌉"
  have "l≠0"
    using big by (force simp: Big_Red_5_6_Ramsey_def)
  have "3 ≤ s"
    using assms by (auto simp: Big_Red_5_6_Ramsey_def s_def)
  also have "… ≤ l"
    using powr_mono [of "3/4" 1] ‹l ≠ 0› by (simp add: s_def)
  finally have "3 ≤ l" .
  then have "k≥3" ‹k>0› ‹l>0›
    using assms by auto
  define p where "p ≡ k powr (-1/8)"
  have p01: "0 < p" "p < 1"
    using ‹k≥3› powr_less_one by (auto simp: p_def)
  have r_le: "r ≤ k powr (c * l powr (3/4))"
    using p01 ‹k≥3› unfolding r_def powr_def by force

  have left: " r^s * p powr ((real s)⇧2 / 4) < 1/2" 
  proof -
    have A: "r powr s ≤ k powr (s * c * l powr (3/4))"
      using r_le by (smt (verit) mult.commute of_nat_0_le_iff powr_mono2 powr_powr)
    have B: "p powr ((real s)⇧2 / 4) ≤ k powr (-(real s)⇧2 / 32)"
      by (simp add: powr_powr p_def power2_eq_square)
    have C: "(c * l powr (3/4) - s/32) ≤ -1"
      using big by (simp add: Big_Red_5_6_Ramsey_def s_def algebra_simps) linarith
    have " r^s * p powr ((real s)⇧2 / 4) ≤ k powr (s * (c * l powr (3/4) - s / 32))"
      using mult_mono [OF A B] ‹s≥3›
      by (simp add: power2_eq_square algebra_simps powr_realpow' flip: powr_add)
    also have "… ≤ k powr - real s"
      using C ‹s≥3› mult_left_mono ‹k≥3› by fastforce
    also have "… ≤ k powr -3"
      using ‹k≥3› ‹s≥3› by (simp add: powr_minus powr_realpow)
    also have "… ≤ 3 powr -3"
      using ‹k≥3› by (intro powr_mono2') auto
    also have "… < 1/2"
      by auto
    finally show ?thesis .
  qed
  have right: "r^k * exp (- p * (real k)⇧2 / 4) < 1/2" 
  proof -
    have A: "r^k ≤ exp (c * l powr (3/4) * ln k * k)"
      using r_le ‹0 < k› ‹0 < l› by (simp add: powr_def exp_of_nat2_mult)
    have B: "exp (- p * (real k)⇧2 / 4) ≤ exp (- k * k powr (7/8) / 4)"
      using ‹k>0› by (simp add: p_def mult_ac power2_eq_square powr_mult_base)
    have "r^k * exp (- p * (real k)⇧2 / 4) ≤ exp (k * (c * l powr (3/4) * ln k - k powr (7/8) / 4))"
      using mult_mono [OF A B] by (simp add: algebra_simps s_def flip: exp_add)
    also have "… ≤ exp (-1)"
      using assms unfolding Big_Red_5_6_Ramsey_def by blast
    also have "… < 1/2"
      by (approximation 5)
    finally show ?thesis .
  qed
  have "¬ is_Ramsey_number (nat⌈l powr (3/4)⌉) k (nat ⌊exp (c * l powr (3/4) * ln k)⌋)"
    using Ramsey_number_lower_simple [OF _ p01] left right ‹k≥3› ‹l≥3›
    unfolding r_def s_def by force
  then show ?thesis
    by (smt (verit) RN_commute is_Ramsey_number_RN le_nat_floor partn_lst_greater_resource)
qed  

definition "ineq_Red_5_6 ≡ λc l. ∀k. l ≤ k ⟶ exp (c * real l powr (3/4) * ln k) ≤ RN k (nat⌈l powr (3/4)⌉)"

definition "Big_Red_5_6 ≡ 
      λl. 6 + m_of l ≤ (1/128) * l powr (3/4) ∧ ineq_Red_5_6 (1/128) l"

text ‹establishing the size requirements for 5.6›
lemma Big_Red_5_6: "∀⇧∞l. Big_Red_5_6 l"
proof -
  define c::real where "c ≡ 1/128"
  have "0 < c" "c < 1/32"
    by (auto simp: c_def)
  then have "∀⇧∞l. ineq_Red_5_6 c l"
    unfolding ineq_Red_5_6_def using Red_5_6_Ramsey Big_Red_5_6_Ramsey exp_gt_zero
    by (smt (verit, del_insts) eventually_sequentially) 
  then show ?thesis
    unfolding Big_Red_5_6_def eventually_conj_iff m_of_def
    by (simp add: c_def; real_asymp)
qed

lemma (in Book) Red_5_6:
  assumes big: "Big_Red_5_6 l"
  shows "RN k (nat⌈l powr (3/4)⌉) ≥ k^6 * RN k (m_of l)" 
proof -
  define c::real where "c ≡ 1/128"
  have "RN k (m_of l) ≤ k^(m_of l)"
    by (metis RN_le_argpower' RN_mono diff_add_inverse diff_le_self le_refl le_trans)
  also have "… ≤ exp (m_of l * ln k)"
    using kn0 by (simp add: exp_of_nat_mult)
  finally have "RN k (m_of l) ≤ exp (m_of l * ln k)"
    by force 
  then have "k^6 * RN k (m_of l) ≤ real k^6 * exp (m_of l * ln k)"
    by (simp add: kn0)
  also have "… ≤ exp (c * l powr (3/4) * ln k)"
  proof -
    have "(6 + real (m_of l)) * ln (real k) ≤ (c * l powr (3/4)) * ln (real k)"
      unfolding mult_le_cancel_right
      using big kn0 by (auto simp: c_def Big_Red_5_6_def)
    then have "ln (real k^6 * exp (m_of l * ln k)) ≤ ln (exp (c * l powr (3/4) * ln k))"
      using kn0 by (simp add: ln_mult ln_powr algebra_simps flip: powr_numeral)
    then show ?thesis
      by (smt (verit) exp_gt_zero ln_le_cancel_iff)
  qed
  also have "… ≤ RN k (nat⌈l powr (3/4)⌉)"
    using assms l_le_k by (auto simp: ineq_Red_5_6_def Big_Red_5_6_def c_def)
  finally show "k^6 * RN k (m_of l) ≤ RN k (nat⌈l powr (3/4)⌉)"
    using of_nat_le_iff by blast
qed 

subsection ‹Lemma 5.4›

definition "Big_Red_5_4 ≡ λl. Big_Red_5_6 l ∧ (∀k≥l. real k + 2 * real k^6 ≤ real k^7)"

text ‹establishing the size requirements for 5.4›
lemma Big_Red_5_4: "∀⇧∞l. Big_Red_5_4 l"
  unfolding Big_Red_5_4_def eventually_conj_iff all_imp_conj_distrib 
  apply (simp add: Big_Red_5_6)
  apply (intro conjI eventually_all_ge_at_top; real_asymp)
  done

context Book
begin

lemma Red_5_4: 
  assumes i: "i ∈ Step_class {red_step,dboost_step}"
    and big: "Big_Red_5_4 l"
  defines "X ≡ Xseq i" and "Y ≡ Yseq i"
  shows "weight X Y (cvx i) ≥ - card X / (real k)^5"
proof -
  have "l≠1"
    using big by (auto simp: Big_Red_5_4_def)
  with ln0 l_le_k have "l>1" "k>1" by linarith+
  let ?R = "RN k (m_of l)"
  have "finite X" "finite Y"
    by (auto simp: X_def Y_def finite_Xseq finite_Yseq)
  have not_many_bluish: "¬ many_bluish X"
    using i not_many_bluish unfolding X_def by blast
  have nonterm: "¬ termination_condition X Y"
    using X_def Y_def i step_non_terminating_iff by (force simp: Step_class_def)
  moreover have "l powr (2/3) ≤ l powr (3/4)"
    using ‹l>1› by (simp add: powr_mono)
  ultimately have RNX: "?R < card X"
    unfolding termination_condition_def m_of_def
    by (meson RN_mono order.trans ceiling_mono le_refl nat_mono not_le)
  have "0 ≤ (∑x ∈ X. ∑x' ∈ X. Weight X Y x x')"
    by (simp add: X_def Y_def sum_Weight_ge0 Xseq_subset_V Yseq_subset_V Xseq_Yseq_disjnt)
  also have "… = (∑y ∈ X. weight X Y y + Weight X Y y y)"
    unfolding weight_def X_def
    by (smt (verit) sum.cong sum.infinite sum.remove)
  finally have ge0: "0 ≤ (∑y∈X. weight X Y y + Weight X Y y y)" .
  have w_maximal: "weight X Y (cvx i) ≥ weight X Y x"
    if "central_vertex X x" for x
    using X_def Y_def ‹finite X› central_vx_is_best cvx_works i that by presburger

  have "¦real (card (S ∩ Y)) * (real (card X) * real (card Y)) -
           real (edge_card Red X Y) * real (card (T ∩ Y))¦
        ≤ real (card X) * real (card Y) * real (card Y)" for S T
    using card_mono [OF _ Int_lower2] ‹finite X› ‹finite Y›
    by (smt (verit, best) of_nat_mult edge_card_le mult.commute mult_right_mono of_nat_0_le_iff of_nat_mono)
  then have W1abs: "¦Weight X Y x y¦ ≤ 1" for x y 
    using RNX edge_card_le [of X Y Red] ‹finite X› ‹finite Y›
    apply (simp add: mult_ac Weight_def divide_simps gen_density_def)
    by (metis Int_lower2 card_mono mult_of_nat_commute)
  then have W1: "Weight X Y x y ≤ 1" for x y
    by (smt (verit))
  have WW_le_cardX: "weight X Y y + Weight X Y y y ≤ card X" if "y ∈ X" for y
  proof -
    have "weight X Y y + Weight X Y y y = sum (Weight X Y y) X"
      by (simp add: ‹finite X› sum_diff1 that weight_def)
    also have "… ≤ card X"
      using W1 by (smt (verit) real_of_card sum_mono)
    finally show ?thesis .
  qed
  have "weight X Y x ≤ real (card(X ∖ {x})) * 1" for x
    unfolding weight_def by (meson DiffE abs_le_D1 sum_bounded_above W1)
  then have wgt_le_X1: "weight X Y x ≤ card X - 1" if "x ∈ X" for x
    using that card_Diff_singleton One_nat_def by (smt (verit, best)) 
  define XB where "XB ≡ {x∈X. bluish X x}"
  have card_XB: "card XB < ?R"
    using not_many_bluish by (auto simp: m_of_def many_bluish_def XB_def)
  have "XB ⊆ X" "finite XB"
    using ‹finite X› by (auto simp: XB_def)
  then have cv_non_XB: "⋀y. y ∈ X ∖ XB ⟹ central_vertex X y"
    by (auto simp: central_vertex_def XB_def bluish_def)
  have "0 ≤ (∑y∈X. weight X Y y + Weight X Y y y)"
    by (fact ge0)
  also have "… = (∑y∈XB. weight X Y y + Weight X Y y y) + (∑y∈X∖XB. weight X Y y + Weight X Y y y)"
    using sum.subset_diff [OF ‹XB⊆X›] by (smt (verit) X_def Xseq_subset_V finV finite_subset)
  also have "… ≤ (∑y∈XB. weight X Y y + Weight X Y y y) + (∑y∈X∖XB. weight X Y (cvx i) + 1)"
    by (intro add_mono sum_mono w_maximal W1 order_refl cv_non_XB)
  also have "… = (∑y∈XB. weight X Y y + Weight X Y y y) + (card X - card XB) * (weight X Y (cvx i) + 1)"
    using ‹XB⊆X› ‹finite XB› by (simp add: card_Diff_subset)
  also have "… ≤ card XB * card X + (card X - card XB) * (weight X Y (cvx i) + 1)"
    using sum_bounded_above WW_le_cardX
    by (smt (verit, ccfv_threshold) XB_def mem_Collect_eq of_nat_mult)
  also have "… = real (?R * card X) + (real (card XB) - ?R) * card X + (card X - card XB) * (weight X Y (cvx i) + 1)"
    using card_XB by (simp add: algebra_simps flip: of_nat_mult of_nat_diff)
  also have "… ≤ real (?R * card X) + (card X - ?R) * (weight X Y (cvx i) + 1)"
  proof -
    have "(real (card X) - card XB) * (weight X Y (cvx i) + 1) 
          ≤ (real (card X) - ?R) * (weight X Y (cvx i) + 1) + (real (?R) - card XB) * (weight X Y (cvx i) + 1)"
      by (simp add: algebra_simps)
    also have "… ≤ (real (card X) - ?R) * (weight X Y (cvx i) + 1) + (real (?R) - card XB) * card X"
      using RNX X_def i card_XB cvx_in_Xseq wgt_le_X1 by fastforce
    finally show ?thesis
      by (smt (verit, del_insts) RNX ‹XB ⊆ X› ‹finite X› card_mono nat_less_le of_nat_diff distrib_right)
  qed
  finally have weight_ge_0: "0 ≤ ?R * card X + (card X - ?R) * (weight X Y (cvx i) + 1)" .
  have rk61: "real k^6 > 1"
    using ‹k>1› by simp
  have k267: "real k + 2 * real k^6 ≤ (real k^7)"
    using ‹l ≤ k› big by (auto simp: Big_Red_5_4_def)
  have k_le: "real k^6 + (?R * real k + ?R * (real k^6)) ≤ 1 + ?R * (real k^7)" 
    using mult_left_mono [OF k267, of ?R] assms
    by (smt (verit, ccfv_SIG) distrib_left card_XB mult_le_cancel_right1 nat_less_real_le of_nat_0_le_iff zero_le_power)
  have [simp]: "real k^m = real k^n ⟷ m=n" "real k^m < real k^n ⟷ m<n" for m n
    using ‹1 < k› by auto
  have "RN k (nat⌈l powr (3/4)⌉) ≥ k^6 * ?R"
    using ‹l ≤ k› big Red_5_6 by (auto simp: Big_Red_5_4_def)
  then have cardX_ge: "card X ≥ k^6 * ?R"
    by (meson le_trans nat_le_linear nonterm termination_condition_def)
  have "-1 / (real k)^5 ≤ - 1 / (real k^6 - 1) + -1 / (real k^6 * ?R)"
      using rk61 card_XB mult_left_mono [OF k_le, of "real k^5"]
      by (simp add: field_split_simps eval_nat_numeral)
  also have "… ≤ - ?R / (real k^6 * ?R - ?R) + -1 / (real k^6 * ?R)"
    using card_XB rk61  by (simp add: field_split_simps)
  finally have "-1 / (real k)^5 ≤ - ?R / (real k^6 * ?R - ?R) + -1 / (real k^6 * ?R)" .
  also have "… ≤ - ?R / (real (card X) - ?R) + -1 / card X"
  proof (intro add_mono divide_left_mono_neg)
    show "real k^6 * real ?R - real ?R ≤ real (card X) - real ?R"
      using cardX_ge of_nat_mono by fastforce
    show "real k^6 * real ?R ≤ real (card X)"
      using cardX_ge of_nat_mono by fastforce
  qed (use RNX rk61 kn0 card_XB in auto)
  also have "… ≤ weight X Y (cvx i) / card X"
    using RNX mult_left_mono [OF weight_ge_0, of "card X"] by (simp add: field_split_simps)
  finally show ?thesis
    using RNX by (simp add: X_def Y_def divide_simps)
qed

lemma Red_5_7a: "ε / k ≤ alpha (hgt p)"
  by (simp add: alpha_ge hgt_gt0)

lemma Red_5_7b: 
  assumes "p ≥ qfun 0" shows "alpha (hgt p) ≤ ε * (p - qfun 0 + 1/k)"
proof -
  have qh_le_p: "qfun (hgt p - Suc 0) ≤ p"
    by (smt (verit) assms diff_Suc_less hgt_gt0 hgt_less_imp_qfun_less zero_less_iff_neq_zero)
  have "alpha (hgt p) = ε * (1 + ε)^(hgt p - 1) / k"
    using alpha_eq alpha_hgt_eq by blast
  also have "… = ε * (qfun (hgt p - 1) - qfun 0 + 1/k)"
    by (simp add: diff_divide_distrib qfun_eq)
  also have "… ≤ ε * (p - qfun 0 + 1/k)"
    by (simp add: eps_ge0 mult_left_mono qh_le_p)
  finally show ?thesis .
qed

lemma Red_5_7c: 
  assumes "p ≤ qfun 1" shows "alpha (hgt p) = ε / k"
  using alpha_hgt_eq Book_axioms assms hgt_Least by fastforce

lemma Red_5_8:
  assumes i: "i ∈ Step_class {dreg_step}" and x: "x ∈ Xseq (Suc i)" 
  shows "card (Neighbours Red x ∩ Yseq (Suc i))
         ≥ (1 - ε powr (1/2)) * pseq i * (card (Yseq (Suc i)))"
proof -
  obtain X Y A B
    where step: "stepper i = (X,Y,A,B)"
      and nonterm: "¬ termination_condition X Y"
      and "even i" 
      and Suc_i: "stepper (Suc i) = degree_reg (X,Y,A,B)"
      and XY: "X = Xseq i" "Y = Yseq i"
    using i by (auto simp: step_kind_defs split: if_split_asm prod.split_asm)
  have "Xseq (Suc i) = ((λ(X, Y, A, B). X) ∘ stepper) (Suc i)"
    by (simp add: Xseq_def)
  also have "… = X_degree_reg X Y"
    using ‹even i› step nonterm by (auto simp: degree_reg_def)
  finally have XSuc: "Xseq (Suc i) = X_degree_reg X Y" .
  have YSuc: "Yseq (Suc i) = Yseq i"
    using Suc_i step by (auto simp: degree_reg_def stepper_XYseq)
  have p_gt_invk: "(pseq i) > 1/k"
    using "XY" nonterm pseq_def termination_condition_def by auto
  have RedN: "(pseq i - ε powr -(1/2) * alpha (hgt (pseq i))) * card Y ≤ card (Neighbours Red x ∩ Y)"
    using x XY by (simp add: XSuc YSuc X_degree_reg_def pseq_def red_dense_def)
  show ?thesis
  proof (cases "pseq i ≥ qfun 0")
    case True
    have "i ∉ Step_class {halted}"
      using i by (simp add: Step_class_def)
    then have p0: "1/k < p0"
      by (metis Step_class_not_halted gr0I nat_less_le not_halted_pee_gt pee_eq_p0)
    have 0: "ε powr -(1/2) ≥ 0"
      by simp
    have "ε powr -(1/2) * alpha (hgt (pseq i)) ≤ ε powr (1/2) * ((pseq i) - qfun 0 + 1/k)"
      using mult_left_mono [OF Red_5_7b [OF True] 0]
      by (simp add: eps_def powr_mult_base flip: mult_ac)
    also have "… ≤ ε powr (1/2) * (pseq i)"
      using p0 by (intro mult_left_mono) (auto simp flip: pee_eq_p0)
    finally have "ε powr -(1/2) * alpha (hgt (pseq i)) ≤ ε powr (1/2) * (pseq i)" .
    then have "(1 - ε powr (1/2)) * (pseq i) * (card Y) ≤ ((pseq i) - ε powr -(1/2) * alpha (hgt (pseq i))) * card Y"
      by (intro mult_right_mono) (auto simp: algebra_simps)
    with XY RedN YSuc show ?thesis by fastforce
  next
    case False
    then have "pseq i ≤ qfun 1"
      by (smt (verit) One_nat_def alpha_Suc_eq alpha_ge0 q_Suc_diff)
    then have "ε powr -(1/2) * alpha (hgt (pseq i)) = ε powr (1/2) / k"
      using powr_mult_base [of "ε"] eps_gt0 by (force simp: Red_5_7c mult.commute)
    also have "… ≤ ε powr (1/2) * (pseq i)"
      using p_gt_invk 
      by (smt (verit) divide_inverse inverse_eq_divide mult_left_mono powr_ge_zero)
    finally have "ε powr -(1/2) * alpha (hgt (pseq i)) ≤ ε powr (1/2) * (pseq i)" .
    then have "(1 - ε powr (1/2)) * pseq i * card Y ≤ (pseq i - ε powr -(1/2) * alpha (hgt (pseq i))) * card Y"
      by (intro mult_right_mono) (auto simp: algebra_simps)
    with XY RedN YSuc show ?thesis by fastforce
  qed
qed

corollary Y_Neighbours_nonempty_Suc:
  assumes i: "i ∈ Step_class {dreg_step}" and x: "x ∈ Xseq (Suc i)" and "k≥2"
  shows "Neighbours Red x ∩ Yseq (Suc i) ≠ {}"
proof
  assume con: "Neighbours Red x ∩ Yseq (Suc i) = {}"
  have not_halted: "i ∉ Step_class {halted}"
    using i by (auto simp: Step_class_def)
  then have 0: "pseq i > 0"
    using not_halted_pee_gt0 by blast
  have Y': "card (Yseq (Suc i)) > 0"
    using i Yseq_gt0 [OF not_halted] stepper_XYseq
    by (auto simp: step_kind_defs degree_reg_def split: if_split_asm prod.split_asm)
  have "(1 - ε powr (1/2)) * pseq i * card (Yseq (Suc i)) ≤ 0"
    using Red_5_8 [OF i x] con by simp 
  with 0 Y' have "(1 - ε powr (1/2)) ≤ 0"
    by (simp add: mult_le_0_iff zero_le_mult_iff)
  then show False
    using ‹k≥2› powr_le_cancel_iff [of k "1/8" 0]
    by (simp add: eps_def powr_minus_divide powr_divide powr_powr)
qed

corollary Y_Neighbours_nonempty:
  assumes i: "i ∈ Step_class {red_step,dboost_step}" and x: "x ∈ Xseq i" and "k≥2"
  shows "card (Neighbours Red x ∩ Yseq i) > 0"
proof (cases i)
  case 0
  with assms show ?thesis
    by (auto simp: Step_class_def stepper_kind_def split: if_split_asm)
next
  case (Suc i')
  then have "i' ∈ Step_class {dreg_step}"
    by (metis dreg_before_step dreg_before_step i Step_class_insert Un_iff) 
  then have "Neighbours Red x ∩ Yseq (Suc i') ≠ {}"
    using Suc Y_Neighbours_nonempty_Suc assms by blast
  then show ?thesis
    by (simp add: Suc card_gt_0_iff finite_Neighbours)
qed

end

subsection ‹Lemma 5.1›

definition "Big_Red_5_1 ≡ λμ l. (1-μ) * real l > 1 ∧ l powr (5/2) ≥ 3 / (1-μ) ∧ l powr (1/4) ≥ 4 
                    ∧ Big_Red_5_4 l ∧ Big_Red_5_6 l" 

text ‹establishing the size requirements for 5.1›
lemma Big_Red_5_1:
  assumes "μ1<1" 
  shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_Red_5_1 μ l"
proof -
  have "(∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 1 < (1-μ) * real l)"
  proof (intro eventually_all_geI1)
    show "⋀l μ. ⟦1 < (1-μ1) * real l; μ ≤ μ1⟧ ⟹ 1 < (1-μ) * l"
      by (smt (verit, best) mult_right_mono of_nat_0_le_iff)
  qed (use assms in real_asymp)
  moreover have "(∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 3 / (1-μ) ≤ real l powr (5/2))"
  proof (intro eventually_all_geI1)
    show "⋀l μ. ⟦3 / (1-μ1) ≤ real l powr (5/2); μ ≤ μ1⟧
           ⟹ 3 / (1-μ) ≤ real l powr (5/2)"
      by (smt (verit, ccfv_SIG) assms frac_le)
  qed (use assms in real_asymp)
  moreover have "∀⇧∞l. 4 ≤ real l powr (1 / 4)"
    by real_asymp
  ultimately show ?thesis
  using assms Big_Red_5_6 Big_Red_5_4 by (auto simp: Big_Red_5_1_def all_imp_conj_distrib eventually_conj_iff)
qed

context Book
begin

lemma card_cvx_Neighbours:
  assumes i: "i ∈ Step_class {red_step,dboost_step}" 
  defines "x ≡ cvx i"
  defines "X ≡ Xseq i" 
  defines "NBX ≡ Neighbours Blue x ∩ X"
  defines "NRX ≡ Neighbours Red x ∩ X"
  shows "card NBX ≤ μ * card X" "card NRX ≥ (1-μ) * card X - 1"
proof -
  obtain "x∈X" "X⊆V"
    by (metis Xseq_subset_V cvx_in_Xseq X_def i x_def)
  then have card_NRBX: "card NRX + card NBX = card X - 1"
    using Neighbours_RB [of x X] disjnt_Red_Blue_Neighbours
    by (simp add: NRX_def NBX_def finite_Neighbours subsetD flip: card_Un_disjnt)
  moreover have card_NBX_le: "card NBX ≤ μ * card X"
    by (metis cvx_works NBX_def X_def central_vertex_def i x_def)
  ultimately show "card NBX ≤ μ * card X" "card NRX ≥ (1-μ) * card X - 1"
    by (auto simp: algebra_simps)
qed

lemma Red_5_1:
  assumes i: "i ∈ Step_class {red_step,dboost_step}"  
    and Big: "Big_Red_5_1 μ l"
  defines "p ≡ pseq i"
  defines "x ≡ cvx i"
  defines "X ≡ Xseq i" and "Y ≡ Yseq i"
  defines "NBX ≡ Neighbours Blue x ∩ X"
  defines "NRX ≡ Neighbours Red x ∩ X"
  defines "NRY ≡ Neighbours Red x ∩ Y"
  defines "β ≡ card NBX / card X"
  shows "red_density NRX NRY ≥ p - alpha (hgt p)
       ∨ red_density NBX NRY ≥ p + (1 - ε) * ((1-β) / β) * alpha (hgt p) ∧ β > 0"
proof -
  have Red_5_4: "weight X Y x ≥ - real (card X) / (real k)^5"
    using Big i Red_5_4 by (auto simp: Big_Red_5_1_def x_def X_def Y_def)
  have lA: "(1-μ) * l > 1" and "l≤k" and l144: "l powr (1/4) ≥ 4"
    using Big by (auto simp: Big_Red_5_1_def l_le_k)
  then have k_powr_14: "k powr (1/4) ≥ 4"
    by (smt (verit) divide_nonneg_nonneg of_nat_0_le_iff of_nat_mono powr_mono2)
  have "k ≥ 256"
    using powr_mono2 [of 4, OF _ _ k_powr_14] by (simp add: powr_powr flip: powr_numeral)
  then have "k>0" by linarith
  have k52: "3 / (1-μ) ≤ k powr (5/2)"
    using Big ‹l≤k› unfolding Big_Red_5_1_def
    by (smt (verit) of_nat_0_le_iff of_nat_mono powr_mono2 zero_le_divide_iff)
  have RN_le_RN: "k^6 * RN k (m_of l) ≤ RN k (nat ⌈l powr (3/4)⌉)"
    using Big ‹l ≤ k› Red_5_6 by (auto simp: Big_Red_5_1_def)
  have l34_ge3: "l powr (3/4) ≥ 3"
    by (smt (verit, ccfv_SIG) l144 divide_nonneg_nonneg frac_le of_nat_0_le_iff powr_le1 powr_less_cancel)
  note XY = X_def Y_def
  obtain A B
    where step: "stepper i = (X,Y,A,B)"
      and nonterm: "¬ termination_condition X Y"
      and "odd i"
      and non_mb: "¬ many_bluish X" and "card X > 0"
      and not_halted: "i ∉ Step_class {halted}"
    using i by (auto simp: XY step_kind_defs termination_condition_def split: if_split_asm prod.split_asm)
  with Yseq_gt0 XY have "card Y ≠ 0"
    by blast
  have cX_RN: "card X > RN k (nat ⌈l powr (3/4)⌉)"
    by (meson linorder_not_le nonterm termination_condition_def)
  then have X_gt_k: "card X > k"
    by (metis l34_ge3 RN_3plus' of_nat_numeral order.trans le_natceiling_iff not_less)
  have "0 < RN k (m_of l)"
    using RN_eq_0_iff m_of_def many_bluish_def non_mb by presburger
  then have "k^4 ≤ k^6 * RN k (m_of l)"
    by (simp add: eval_nat_numeral)
  also have "… < card X"
    using cX_RN RN_le_RN by linarith
  finally have "card X > k^4" .
  have "x ∈ X"
    using cvx_in_Xseq i XY x_def by blast
  have "X ⊆ V"
    by (simp add: Xseq_subset_V XY)
  have "finite NRX" "finite NBX" "finite NRY"
    by (auto simp: NRX_def NBX_def NRY_def finite_Neighbours)
  have "disjnt X Y"
    using Xseq_Yseq_disjnt step stepper_XYseq by blast  
  then have "disjnt NRX NRY" "disjnt NBX NRY"
    by (auto simp: NRX_def NBX_def NRY_def disjnt_iff)
  have card_NRBX: "card NRX + card NBX = card X - 1"
    using Neighbours_RB [of x X] ‹finite NRX› ‹x∈X› ‹X⊆V› disjnt_Red_Blue_Neighbours
    by (simp add: NRX_def NBX_def finite_Neighbours subsetD flip: card_Un_disjnt)
  obtain card_NBX_le: "card NBX ≤ μ * card X" and "card NRX ≥ (1-μ) * card X - 1"
    unfolding NBX_def NRX_def X_def x_def using card_cvx_Neighbours i by metis
  with lA ‹l≤k› X_gt_k have "card NRX > 0"
    by (smt (verit, best) of_nat_0 μ01 gr0I mult_less_cancel_left_pos nat_less_real_le of_nat_mono)
  have "card NRY > 0"
    using Y_Neighbours_nonempty [OF i] ‹k≥256› NRY_def ‹finite NRY› ‹x ∈ X› card_0_eq XY by force
  show ?thesis
  proof (cases "(∑y∈NRX. Weight X Y x y)  ≥ -alpha (hgt p) * card NRX * card NRY / card Y")
    case True
    then have "(p - alpha (hgt p)) * (card NRX * card NRY) ≤ (∑y ∈ NRX. p * card NRY + Weight X Y x y * card Y)"
      using ‹card Y ≠ 0› by (simp add: field_simps sum_distrib_left sum.distrib)
    also have "… = (∑y ∈ NRX. card (Neighbours Red x ∩ Neighbours Red y ∩ Y))"
      using ‹card Y ≠ 0› by (simp add: Weight_def pseq_def XY NRY_def field_simps p_def)
    also have "… = edge_card Red NRY NRX"
      using ‹disjnt NRX NRY› ‹finite NRX›
      by (simp add: disjnt_sym edge_card_eq_sum_Neighbours Red_E psubset_imp_subset NRY_def Int_ac)
    also have "… = edge_card Red NRX NRY"
      by (simp add: edge_card_commute)
    finally have "(p - alpha (hgt p)) * real (card NRX * card NRY) ≤ real (edge_card Red NRX NRY)" .
    then show ?thesis
      using ‹card NRX > 0› ‹card NRY > 0› 
      by (simp add: NRX_def NRY_def gen_density_def field_split_simps XY)
  next
    case False
    have "x ∈ X"
      unfolding x_def using cvx_in_Xseq i XY by blast
    with Neighbours_RB[of x X] have Xx: "X - {x} = NBX ∪ NRX"
      using Xseq_subset_V NRX_def NBX_def XY by blast
    have disjnt: "NBX ∩ NRX = {}"
      by (auto simp: Blue_eq NRX_def NBX_def disjoint_iff in_Neighbours_iff)
    then have "weight X Y x = (∑y ∈ NRX. Weight X Y x y) + (∑y ∈ NBX. Weight X Y x y)"
      by (simp add: weight_def Xx sum.union_disjoint finite_Neighbours NRX_def NBX_def)
    with False 
    have 15: "(∑y ∈ NBX. Weight X Y x y) 
        ≥ weight X Y x + alpha (hgt p) * card NRX * card NRY / card Y"
      by linarith    
    have pm1: "pseq (i-1) > 1/k"
      by (meson Step_class_not_halted diff_le_self not_halted not_halted_pee_gt)
    have β_eq: "β = card NBX / card X"
      using NBX_def β_def XY by blast
    have "β≤μ"
      by (simp add: β_eq ‹0 < card X› card_NBX_le pos_divide_le_eq)
    have im1: "i-1 ∈ Step_class {dreg_step}"
      using i ‹odd i› dreg_before_step
      by (metis Step_class_insert Un_iff One_nat_def odd_Suc_minus_one)
    have "ε ≤ 1/4"
      using ‹k>0› k_powr_14 by (simp add: eps_def powr_minus_divide)
    then have "ε powr (1/2) ≤ (1/4) powr (1/2)"
      by (simp add: eps_def powr_mono2)
    then have A: "1/2 ≤ 1 - ε powr (1/2)"
      by (simp add: powr_divide)
    have le: "1 / (2 * real k) ≤ (1 - ε powr (1/2)) * pseq (i-1)"
      using pm1 ‹k>0› mult_mono [OF A less_imp_le [OF pm1]] A by simp
    have "card Y / (2 * real k) ≤ (1 - ε powr (1/2)) * pseq (i-1) * card Y"
      using mult_left_mono [OF le] by (metis mult.commute divide_inverse inverse_eq_divide of_nat_0_le_iff)
    also have "… ≤ card NRY"
      using pm1 Red_5_8 im1 by (metis NRY_def One_nat_def ‹odd i› ‹x ∈ X› XY odd_Suc_minus_one)
    finally have Y_NRY: "card Y / (2 * real k) ≤ card NRY" .
    have "NBX ≠ {}"
    proof 
      assume empty: "NBX = {}"
      then have cNRX: "card NRX = card X - 1"
        using card_NRBX by auto
      have "card X > 3"
        using ‹k≥256› X_gt_k by linarith
      then have "2 * card X / real (card X - 1) < 3"
        by (simp add: divide_simps)
      also have "… ≤ k^2"
        using mult_mono [OF ‹k≥256› ‹k≥256›] by (simp add: power2_eq_square flip: of_nat_mult)
      also have "… ≤ ε * k^3"
        using ‹k≥256› by (simp add: eps_def flip: powr_numeral powr_add)
      finally have "(real (2 * card X) / real (card X - 1)) * k^2 < ε * real (k^3) * k^2"
        using ‹k>0› by (intro mult_strict_right_mono) auto
      then have "real (2 * card X) / real (card X - 1) * k^2 < ε * real (k^5)"
        by (simp add: mult.assoc flip: of_nat_mult)
      then have "0 < - real (card X) / (real k)^5 + (ε / k) * real (card X - 1) * (1 / (2 * real k))"
        using ‹k>0› X_gt_k by (simp add: field_simps power2_eq_square)
      also have "- real (card X) / (real k)^5 + (ε / k) * real (card X - 1) * (1 / (2 * real k)) 
               ≤ - real (card X) / (real k)^5 + (ε / k) * real (card NRX) * (card NRY / card Y)"
        using Y_NRY ‹k>0› ‹card Y ≠ 0›
        by (intro add_mono mult_mono) (auto simp: cNRX eps_def divide_simps)
      also have "… = - real (card X) / (real k)^5 + (ε / k) * real (card NRX) * card NRY / card Y"
        by simp
      also have "… ≤ - real (card X) / (real k)^5 + alpha (hgt p) * real (card NRX) * card NRY / card Y"
        using alpha_ge [OF hgt_gt0]
        by (intro add_mono mult_right_mono divide_right_mono) auto
      also have "… ≤ 0"
        using empty 15 Red_5_4 by auto
      finally show False
        by simp
    qed
    have "card NBX > 0"
      by (simp add: ‹NBX ≠ {}› ‹finite NBX› card_gt_0_iff)
    then have "0 < β"
      by (simp add: β_eq ‹0 < card X›)
    have "β ≤ μ"
      using X_gt_k card_NBX_le by (simp add: β_eq NBX_def divide_simps)
    have cNRX: "card NRX = (1-β) * card X - 1"
      using X_gt_k card_NRBX  by (simp add: β_eq divide_simps)
    have cNBX: "card NBX = β * card X"
      using ‹0 < card X› by (simp add: β_eq)
    let ?E16 = "p + ((1-β)/β) * alpha (hgt p) - alpha (hgt p) / (β * card X) + weight X Y x * card Y / (β * card X * card NRY)"
    have "p * card NBX * card NRY + alpha (hgt p) * card NRX * card NRY + weight X Y x * card Y
            ≤ (∑y ∈ NBX. p * card NRY + Weight X Y x y * card Y)"
      using 15 ‹card Y ≠ 0› apply (simp add: sum_distrib_left sum.distrib)
      by (simp only: sum_distrib_right divide_simps split: if_split_asm)
    also have "… ≤ (∑y ∈ NBX. card (Neighbours Red x ∩ Neighbours Red y ∩ Y))"
      using ‹card Y ≠ 0› by (simp add: Weight_def pseq_def XY NRY_def field_simps p_def)
    also have "… = edge_card Red NRY NBX"
      using ‹disjnt NBX NRY› ‹finite NBX›
      by (simp add: disjnt_sym edge_card_eq_sum_Neighbours Red_E psubset_imp_subset NRY_def Int_ac)
    also have "… = edge_card Red NBX NRY"
      by (simp add: edge_card_commute)
    finally have Red_bound: 
      "p * card NBX * card NRY + alpha (hgt p) * card NRX * card NRY + weight X Y x * card Y ≤ edge_card Red NBX NRY" .
    then have "(p * card NBX * card NRY + alpha (hgt p) * card NRX * card NRY + weight X Y x * card Y)
             / (card NBX * card NRY) ≤ red_density NBX NRY"
      by (metis divide_le_cancel gen_density_def of_nat_less_0_iff)
    then have "p + alpha (hgt p) * card NRX / card NBX + weight X Y x * card Y / (card NBX * card NRY) ≤ red_density NBX NRY" 
      using ‹card NBX > 0› ‹card NRY > 0› by (simp add: add_divide_distrib)
    then have 16: "?E16 ≤ red_density NBX NRY" 
      using ‹β>0› ‹card X > 0›
      by (simp add: cNRX cNBX algebra_simps add_divide_distrib diff_divide_distrib)
    consider "qfun 0 ≤ p" | "p ≤ qfun 1"
      by (smt (verit) alpha_Suc_eq alpha_ge0 One_nat_def q_Suc_diff)
    then have alpha_le_1: "alpha (hgt p) ≤ 1"
    proof cases
      case 1
      have "p * ε + ε / real k ≤ 1 + ε * p0"
      proof (intro add_mono)
        show "p * ε ≤ 1"
          by (simp add: assms(3) eps_ge0 eps_le1 mult_le_one pee_le1)
        have "p0 > 1/k"
          by (metis Step_class_not_halted diff_le_self not_halted not_halted_pee_gt diff_is_0_eq' pee_eq_p0)
        then show "ε / real k ≤ ε * p0"
          by (metis divide_inverse eps_ge0 mult_left_mono less_eq_real_def mult_cancel_right1)
      qed
      then show ?thesis
        using Red_5_7b [OF 1] by (simp add: algebra_simps)
    next
      case 2
      show ?thesis
        using Red_5_7c [OF 2] ‹k≥256› eps_less1 by simp
    qed
    have B: "- (3 / (real k^4)) ≤ (-2 / real k^4) - alpha (hgt p) / card X"
      using ‹card X > k^4› ‹card Y ≠ 0› ‹0 < k› alpha_le_1 by (simp add: algebra_simps frac_le)
    have "- (3 / (β * real k^4)) ≤ (-2 / real k^4) / β - alpha (hgt p) / (β * card X)"
      using ‹β>0› divide_right_mono [OF B, of β] ‹k>0› by (simp add: field_simps)
    also have "… = (- real (card X) / real k^5) * card Y / (β * real (card X) * (card Y / (2 * real k))) - alpha (hgt p) / (β * card X)"
      using ‹card Y ≠ 0› ‹0 < card X› 
      by (simp add: field_split_simps eval_nat_numeral)
    also have "…  ≤ (- real (card X) / real k^5) * card Y / (β * real (card X) * card NRY) - alpha (hgt p) / (β * card X)"
      using Y_NRY ‹k>0› ‹card NRY > 0› ‹card X > 0› ‹card Y ≠ 0› ‹β>0›
      by (intro diff_mono divide_right_mono mult_left_mono divide_left_mono_neg) auto
    also have "…  ≤ weight X Y x * card Y / (β * real (card X) * card NRY) - alpha (hgt p) / (β * card X)"
      using Red_5_4 ‹k>0› ‹0 < β›
      by (intro diff_mono divide_right_mono mult_right_mono) auto
    finally have "- (3 / (β * real k^4)) ≤ weight X Y x * card Y / (β * real (card X) * card NRY) - alpha (hgt p) / (β * card X)" .
    then have 17: "p + ((1-β)/β) * alpha (hgt p) - 3 / (β * real k^4) ≤ ?E16"
      by simp
    have "3 / real k^4 ≤ (1-μ) * ε^2 / k"
      using ‹k>0› μ01 mult_left_mono [OF k52, of k] 
      by (simp add: field_simps eps_def powr_powr powr_mult_base flip: powr_numeral powr_add)
    also have "… ≤ (1-β) * ε^2 / k"
      using ‹β≤μ›
      by (intro divide_right_mono mult_right_mono) auto
    also have "… ≤ (1-β) * ε * alpha (hgt p)"
      using Red_5_7a [of p] eps_ge0 ‹β≤μ› μ01
      unfolding power2_eq_square divide_inverse mult.assoc
      by (intro mult_mono) auto
    finally have †: "3 / real k^4 ≤ (1-β) * ε * alpha (hgt p)" .
    have "p + (1 - ε) * ((1-β) / β) * alpha (hgt p) + 3 / (β * real k^4) ≤ p + ((1-β)/β) * alpha (hgt p)"
      using ‹0<β› ‹k>0› mult_left_mono [OF †, of β] by (simp add: field_simps)
    with 16 17 have "p + (1 - ε) * ((1 - β) / β) * alpha (hgt p) ≤ red_density NBX NRY"
      by linarith
    then show ?thesis
      using ‹0 < β› NBX_def NRY_def XY by fastforce
  qed
qed

text ‹This and the previous result are proved under the assumption of a sufficiently large @{term l}›
corollary Red_5_2:
  assumes i: "i ∈ Step_class {dboost_step}" 
    and Big: "Big_Red_5_1 μ l"
  shows "pseq (Suc i) - pseq i ≥ (1 - ε) * ((1 - beta i) / beta i) * alpha (hgt (pseq i)) ∧
         beta i > 0"
proof -
  let ?x = "cvx i"
  obtain X Y A B
    where step: "stepper i = (X,Y,A,B)"
      and nonterm: "¬ termination_condition X Y"
      and "odd i"
      and non_mb: "¬ many_bluish X"
      and nonredd: "¬ reddish k X Y (red_density X Y) (choose_central_vx (X,Y,A,B))"
      and Xeq: "X = Xseq i" and Yeq: "Y = Yseq i"
    using i
    by (auto simp: step_kind_defs split: if_split_asm prod.split_asm)
  then have "?x ∈ Xseq i"
    by (simp add: choose_central_vx_X cvx_def finite_Xseq)
  then have "central_vertex (Xseq i) (cvx i)"
    by (metis Xeq choose_central_vx_works cvx_def finite_Xseq step non_mb nonterm)
  with Xeq have "card (Neighbours Blue (cvx i) ∩ Xseq i) ≤ μ * card (Xseq i)"
    by (simp add: central_vertex_def)
  then have βeq: "card (Neighbours Blue (cvx i) ∩ Xseq i) = beta i * card (Xseq i)"
    using Xeq step by (auto simp: beta_def)
  have SUC: "stepper (Suc i) = (Neighbours Blue ?x ∩ X, Neighbours Red ?x ∩ Y, A, insert ?x B)"
    using step nonterm ‹odd i› non_mb nonredd
    by (simp add: stepper_def next_state_def Let_def cvx_def)
  have pseq: "pseq i = red_density X Y"
    by (simp add: pseq_def Xeq Yeq)
  have "choose_central_vx (X,Y,A,B) = cvx i"
    by (simp add: cvx_def step)
  with nonredd have "red_density (Neighbours Red (cvx i) ∩ X) (Neighbours Red (cvx i) ∩ Y)
                   < pseq i - alpha (hgt (red_density X Y))"
    using nonredd by (simp add: reddish_def pseq)
  then have "pseq i + (1 - ε) * ((1 - beta i) / beta i) * alpha (hgt (pseq i))
          ≤ red_density (Neighbours Blue (cvx i) ∩ Xseq i)
              (Neighbours Red (cvx i) ∩ Yseq i) ∧ beta i > 0"
    using Red_5_1 Un_iff Xeq Yeq assms gen_density_ge0 pseq Step_class_insert
    by (smt (verit, ccfv_threshold) βeq divide_eq_eq)
  moreover have "red_density (Neighbours Blue (cvx i) ∩ Xseq i)
                             (Neighbours Red (cvx i) ∩ Yseq i) ≤ pseq (Suc i)"
    using SUC Xeq Yeq stepper_XYseq by (simp add: pseq_def)
  ultimately show ?thesis
    by linarith
qed

end

subsection ‹Lemma 5.3›

text ‹This is a weaker consequence of the previous results›

definition 
  "Big_Red_5_3 ≡ 
    λμ l. Big_Red_5_1 μ l
        ∧ (∀k≥l. k>1 ∧ 1 / (real k)⇧2 ≤ μ ∧ 1 / (real k)⇧2 ≤ 1 / (k / eps k / (1 - eps k) + 1))"

text ‹establishing the size requirements for 5.3. The one involving @{term μ},
namely @{term "1 / (real k)⇧2 ≤ μ"}, will be useful later with "big beta".›
lemma Big_Red_5_3:
  assumes "0<μ0" "μ1<1" 
  shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_Red_5_3 μ l"
  using assms Big_Red_5_1
  apply (simp add: Big_Red_5_3_def eps_def eventually_conj_iff all_imp_conj_distrib)  
  apply (intro conjI strip eventually_all_geI0 eventually_all_ge_at_top)
  apply (real_asymp|force)+
  done

context Book
begin

corollary Red_5_3:
  assumes i: "i ∈ Step_class {dboost_step}"
    and big: "Big_Red_5_3 μ l" 
  shows "pseq (Suc i) ≥ pseq i ∧ beta i ≥ 1 / (real k)⇧2"
proof 
  have "k>1" and big51: "Big_Red_5_1 μ l"
    using l_le_k big by (auto simp: Big_Red_5_3_def)
  let ?h = "hgt (pseq i)"
  have "?h > 0"
    by (simp add: hgt_gt0 kn0 pee_le1)
  then obtain α: "alpha ?h ≥ 0" and *: "alpha ?h ≥ ε / k"
    using alpha_ge0 ‹k>1› alpha_ge by auto
  moreover have "-5/4 = -1/4 - (1::real)"
    by simp
  ultimately have α54: "alpha ?h ≥ k powr (-5/4)"
    unfolding eps_def by (metis powr_diff of_nat_0_le_iff powr_one)
  have β: "beta i ≤ μ"
    by (metis Step_class_insert Un_iff beta_le i)
  have "(1 - ε) * ((1 - beta i) / beta i) * alpha ?h ≥ 0"
    using beta_ge0[of i] eps_le1 α β μ01 ‹k>1›
    by (simp add: zero_le_mult_iff zero_le_divide_iff)
  then show "pseq (Suc i) ≥ pseq i"
    using Red_5_2 [OF i big51] by linarith 
  have "pseq (Suc i) - pseq i ≤ 1"
    by (smt (verit) pee_ge0 pee_le1)
  with Red_5_2 [OF i big51] 
  have "(1 - ε) * ((1 - beta i) / beta i) * alpha ?h ≤ 1" and beta_gt0: "beta i > 0"
    by linarith+
  with * have "(1 - ε) * ((1 - beta i) / beta i) * ε / k ≤ 1"
    by (smt (verit, best) mult.commute eps_ge0 mult_mono mult_nonneg_nonpos of_nat_0_le_iff times_divide_eq_right zero_le_divide_iff)
  then have "(1 - ε) * ((1 - beta i) / beta i) ≤ k / ε"
    using beta_ge0 [of i] eps_gt0 kn0
    by (auto simp: divide_simps mult_less_0_iff mult_of_nat_commute split: if_split_asm)
  then have "(1 - beta i) / beta i ≤ k / ε / (1 - ε)"
    by (smt (verit) eps_less1 mult.commute pos_le_divide_eq ‹1 < k›)
  then have "1 / beta i ≤ k / ε / (1 - ε) + 1"
    using beta_gt0 by (simp add: diff_divide_distrib)
  then have "1 / (k / ε / (1 - ε) + 1) ≤ beta i"
    using beta_gt0 eps_gt0 eps_less1 [OF ‹k>1›] kn0
    apply (simp add: divide_simps split: if_split_asm)
    by (smt (verit, ccfv_SIG) mult.commute mult_less_0_iff)
  moreover have "1 / k^2 ≤ 1 / (k / ε / (1 - ε) + 1)"
    using Big_Red_5_3_def l_le_k big eps_def by (metis (no_types, lifting) of_nat_power)
  ultimately show "beta i ≥ 1 / (real k)⇧2"
    by auto
qed

corollary beta_gt0:
  assumes "i ∈ Step_class {dboost_step}"
    and "Big_Red_5_3 μ l" 
  shows "beta i > 0"
  by (meson Big_Red_5_3_def Book.Red_5_2 Book_axioms assms)

end (*context Book*)

end