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 ‹finite Y› assms by (intro sum_squared_le_sum_of_squares) auto 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 (smt (verit) eps_le1 ‹0 < k› mult_left_le p_def pee_ge0 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