Theory Far_From_Diagonal
section ‹An exponential improvement far from the diagonal›
theory Far_From_Diagonal
imports Zigzag "Stirling_Formula.Stirling_Formula"
begin
subsection ‹An asymptotic form for binomial coefficients via Stirling's formula›
text ‹From Appendix D.3, page 56›
lemma const_smallo_real: "(λn. x) ∈ o(real)"
by real_asymp
lemma o_real_shift:
assumes "f ∈ o(real)"
shows "(λi. f(i+j)) ∈ o(real)"
unfolding smallo_def
proof clarify
fix c :: real
assume "(0::real) < c"
then have *: "∀⇩F i in sequentially. norm (f i) ≤ c/2 * norm i"
using assms half_gt_zero landau_o.smallD by blast
have "∀⇩F i in sequentially. norm (f (i + j)) ≤ c/2 * norm (i + j)"
using eventually_all_ge_at_top [OF *]
by (metis (mono_tags, lifting) eventually_sequentially le_add1)
then have "∀⇩F i in sequentially. i≥j ⟶ norm (f (i + j)) ≤ c * norm i"
apply eventually_elim
apply clarsimp
by (smt (verit, best) ‹0 < c› mult_left_mono nat_distrib(2) of_nat_mono)
then show "∀⇩F i in sequentially. norm (f (i + j)) ≤ c * norm i"
using eventually_mp by fastforce
qed
lemma tendsto_zero_imp_o1:
fixes a :: "nat ⇒ real"
assumes "a ⇢ 0"
shows "a ∈ o(1)"
proof -
have "∀⇩F n in sequentially. ¦a n¦ ≤ c" if "c>0" for c
using assms order_tendstoD(2) tendsto_rabs_zero_iff eventually_sequentially less_eq_real_def that
by metis
then show ?thesis
by (auto simp: smallo_def)
qed
subsection ‹Fact D.3 from the Appendix›
text ‹And hence, Fact 9.4›
definition "stir ≡ λn. fact n / (sqrt (2*pi*n) * (n / exp 1) ^ n) - 1"
text ‹Generalised to the reals to allow derivatives›
definition "stirG ≡ λn. Gamma (n+1) / (sqrt (2*pi*n) * (n / exp 1) powr n) - 1"
lemma stir_eq_stirG: "n>0 ⟹ stir n = stirG (real n)"
by (simp add: stirG_def stir_def add.commute powr_realpow Gamma_fact)
lemma stir_ge0: "n>0 ⟹ stir n ≥ 0"
using fact_bounds[of n] by (simp add: stir_def)
lemma stir_to_0: "stir ⇢ 0"
using fact_asymp_equiv by (simp add: asymp_equiv_def stir_def LIM_zero)
lemma stir_o1: "stir ∈ o(1)"
using stir_to_0 tendsto_zero_imp_o1 by presburger
lemma fact_eq_stir_times: "n ≠ 0 ⟹ fact n = (1 + stir n) * (sqrt (2*pi*n) * (n / exp 1) ^ n)"
by (simp add: stir_def)
definition "logstir ≡ λn. if n=0 then 0 else log 2 ((1 + stir n) * sqrt (2*pi*n))"
lemma logstir_o_real: "logstir ∈ o(real)"
proof -
have "∀⇧∞n. 0 < n ⟶ ¦log 2 ((1 + stir n) * sqrt (2*pi*n))¦ ≤ c * real n" if "c>0" for c
proof -
have "∀⇧∞n. 2 powr (c*n) / sqrt (2*pi*n) ≥ c+1"
using that by real_asymp
moreover have "∀⇧∞n. ¦stir n¦ ≤ c"
using stir_o1 that by (auto simp: smallo_def)
ultimately have "∀⇧∞n. ((1 + stir n) * sqrt (2*pi*n)) ≤ 2 powr (c * n)"
proof eventually_elim
fix n
assume c1: "c+1 ≤ 2 powr (c * n) / sqrt (2*pi*n)" and lec: "¦stir n¦ ≤ c"
then have "stir n ≤ c"
by auto
then show "(1 + stir n) * sqrt (2*pi*n) ≤ 2 powr (c*n)"
using mult_right_mono [OF c1, of "sqrt (2*pi*n)"] lec
by (smt (verit, ccfv_SIG) c1 mult_right_mono nonzero_eq_divide_eq pos_prod_le powr_gt_zero)
qed
then show ?thesis
proof (eventually_elim, clarify)
fix n
assume n: "(1 + stir n) * sqrt (2 * pi * n) ≤ 2 powr (c * n)"
and "n>0"
have "(1 + stir n) * sqrt (2 * pi * real n) ≥ 1"
using stir_ge0 ‹0 < n› mult_ge1_I pi_ge_two by auto
with n show "¦log 2 ((1 + stir n) * sqrt (2 * pi * n))¦ ≤ c * n"
by (simp add: abs_if le_powr_iff)
qed
qed
then show ?thesis
by (auto simp: smallo_def logstir_def)
qed
lemma logfact_eq_stir_times:
"fact n = 2 powr (logstir n) * (n / exp 1) ^ n"
proof-
have "1 + stir n > 0" if "n≠0"
using that by (simp add: stir_def)
then show ?thesis
by (simp add: logstir_def fact_eq_stir_times)
qed
lemma mono_G:
defines "G ≡ (λx::real. Gamma (x + 1) / (x / exp 1) powr x)"
shows "mono_on {0<..} G"
unfolding monotone_on_def
proof (intro strip)
fix x y::real
assume x: "x ∈ {0<..}" "x ≤ y"
define GD where "GD ≡ λu::real. Gamma(u+1) * (Digamma(u+1) - ln(u)) / (u / exp 1) powr u"
have *: "∃D. (G has_real_derivative D) (at u) ∧ D > 0" if "0 < u" for u
proof (intro exI conjI)
show "(G has_real_derivative GD u) (at u)"
unfolding G_def GD_def
using that
by (force intro!: derivative_eq_intros has_real_derivative_powr' simp: ln_div pos_prod_lt field_simps)
show "GD u > 0"
using that by (auto simp: GD_def Digamma_plus_1_gt_ln)
qed
show "G x ≤ G y"
using x DERIV_pos_imp_increasing [OF _ *] by (force simp: less_eq_real_def)
qed
lemma mono_logstir: "mono logstir"
unfolding monotone_on_def
proof (intro strip)
fix i j::nat
assume "i≤j"
show "logstir i ≤ logstir j"
proof (cases "j=0")
case True
with ‹i≤j› show ?thesis
by auto
next
case False
with pi_ge_two have "1 * 1 ≤ 2 * pi * j"
by (intro mult_mono) auto
with False stir_ge0 [of j] have *: "1 * 1 ≤ (1 + stir j) * sqrt (2 * pi * real j)"
by (intro mult_mono) auto
with ‹i ≤ j› mono_G show ?thesis
by (auto simp: logstir_def stir_eq_stirG stirG_def monotone_on_def)
qed
qed
definition "ok_fun_94 ≡ λk. - logstir k"
lemma ok_fun_94: "ok_fun_94 ∈ o(real)"
unfolding ok_fun_94_def
using logstir_o_real by simp
lemma fact_9_4:
assumes l: "0 < l" "l ≤ k"
defines "γ ≡ l / (real k + real l)"
shows "k+l choose l ≥ 2 powr ok_fun_94 k * γ powr (-l) * (1-γ) powr (-k)"
proof -
have *: "ok_fun_94 k ≤ logstir (k+l) - (logstir k + logstir l)"
using mono_logstir by (auto simp: ok_fun_94_def monotone_def)
have "2 powr ok_fun_94 k * γ powr (- real l) * (1-γ) powr (- real k)
= (2 powr ok_fun_94 k) * (k+l) powr(k+l) / (k powr k * l powr l)"
by (simp add: γ_def powr_minus powr_add powr_divide divide_simps)
also have "… ≤ (2 powr (logstir (k+l)) / (2 powr (logstir k) * 2 powr (logstir l)))
* (k+l) powr (k+l) / (k powr k * l powr l)"
by (smt (verit, del_insts) * divide_right_mono mult_less_0_iff mult_right_mono powr_add powr_diff powr_ge_pzero powr_mono)
also have "… = fact(k+l) / (fact k * fact l)"
using l by (simp add: logfact_eq_stir_times powr_add divide_simps flip: powr_realpow)
also have "… = real (k+l choose l)"
by (simp add: binomial_fact)
finally show ?thesis .
qed
subsection ‹Fact D.2›
text ‹For Fact 9.6›
lemma D2:
fixes k l
assumes t: "0<t" "t ≤ k"
defines "γ ≡ l / (real k + real l)"
shows "(k+l-t choose l) ≤ exp (- γ * (t-1)^2 / (2*k)) * (k / (k+l))^t * (k+l choose l)"
proof -
have "(k+l-t choose l) * inverse (k+l choose l) = (∏i<t. (k-i) / (k+l-i))"
using ‹t ≤ k›
proof (induction t)
case (Suc t)
then have "t ≤ k"
by simp
have "(k + l - t) * (k + l - Suc t choose l) = (k - t) * (k + l - t choose l)"
by (metis binomial_absorb_comp diff_Suc_eq_diff_pred diff_add_inverse2 diff_commute)
with Suc.IH [symmetric] Suc(2) show ?case
by (simp add: field_simps flip: of_nat_mult of_nat_diff)
qed auto
also have "… = (real k / (k+l))^t * (∏i<t. 1 - real i * real l / (real k * (k+l-i)))"
proof -
have "1 - i * real l / (real k * (k+l-i)) = ((k-i)/(k+l-i)) * ((k+l) / k)"
if "i<t" for i
using that ‹t ≤ k› by (simp add: divide_simps) argo
then have *: "(∏i<t. 1 - real i * real l / (real k * (k+l-i))) = (∏i<t. ((k-i)/(k+l-i)) * ((k+l) / k))"
by auto
show ?thesis
unfolding * prod.distrib by (simp add: power_divide)
qed
also have "… ≤ (real k / (k+l))^t * exp (- (∑i<t. real i * real l / (real k * (k+l))))"
proof (intro mult_left_mono)
have "real i * real l / (real k * real (k+l-i)) ≤ 1"
if "i < t" for i
using that ‹t ≤ k› by (simp add: divide_simps mult_mono)
moreover have "1 - i * l / (k * real (k+l-i)) ≤ exp (- (i * real l / (k * (k + real l))))" (is "_ ≤ ?R")
if "i < t" for i
proof -
have "exp (- (i*l / (k * real (k+l-i)))) ≤ ?R"
using that ‹t ≤ k› by (simp add: frac_le_eq divide_le_0_iff mult_mono)
with exp_minus_ge show ?thesis
by (smt (verit, best))
qed
ultimately show "(∏i<t. 1 - i * real l / (k * real (k+l-i))) ≤ exp (- (∑i<t. i * real l / (k * real (k+l))))"
by (force simp: exp_sum simp flip: sum_negf intro!: prod_mono)
qed auto
finally have 1: "(k+l-t choose l) * inverse (k+l choose l)
≤ (real k / (k+l))^t * exp (- (∑i<t. i * γ / k))"
by (simp add: γ_def mult.commute)
have **: "γ * (t - 1)^2 / (2*k) ≤ (∑i<t. i * γ / k)"
proof -
have g: "(∑i<t. real i) = real (t*(t-1)) / 2"
by (induction t) (auto simp: algebra_simps eval_nat_numeral)
have "γ * (t-1)^2 / (2*k) ≤ real(t*(t-1)) / 2 * γ/k"
by (simp add: field_simps eval_nat_numeral divide_right_mono mult_mono γ_def)
also have "… = (∑i<t. i * γ / k)"
unfolding g [symmetric] by (simp add: sum_distrib_right sum_divide_distrib)
finally show ?thesis .
qed
have 0: "0 ≤ real (k + l choose l)"
by simp
have *: "(k+l-t choose l) ≤ (k / (k+l))^t * exp (- (∑i<t. i * γ / k)) * (k+l choose l)"
using order_trans [OF _ mult_right_mono [OF 1 0]]
by (simp add: less_eq_real_def)
also have "… ≤ (k / (k+l))^t * exp (- γ * (t-1)^2 / (2*k)) *(k+l choose l)"
using ** by (intro mult_mono) auto
also have "… ≤ exp (- γ * (t-1)^2 / (2 * real k)) * (k / (k+l))^t * (k+l choose l)"
by (simp add: mult_ac)
finally show ?thesis
using t by simp
qed
text ‹Statement borrowed from Bhavik; no o(k) function›
corollary Far_9_6:
fixes k l
assumes t: "0<t" "t ≤ k"
defines "γ ≡ l / (k + real l)"
shows "exp (-1) * (1-γ) powr (- real t) * exp (γ * (real t)⇧2 / real(2*k)) * (k-t+l choose l) ≤ (k+l choose l)"
proof -
have kkl: "k / (k + real l) = 1 - γ" "k+l-t = k-t+l"
using t by (auto simp: γ_def divide_simps)
have [simp]: "t + t ≤ Suc (t * t)"
using t
by (metis One_nat_def Suc_leI mult_2 mult_right_mono nle_le not_less_eq_eq numeral_2_eq_2 mult_1_right)
have "0 ≤ γ" "γ < 1"
using t by (auto simp: γ_def)
then have "γ * (real t * 2) ≤ γ + real k * 2"
using t by (smt (verit, best) mult_less_cancel_right2 of_nat_0_less_iff of_nat_mono)
then have *: "γ * t^2 / (2*k) - 1 ≤ γ * (t-1)^2 / (2*k)"
using t
apply (simp add: power2_eq_square pos_divide_le_eq divide_simps)
apply (simp add: algebra_simps)
done
then have *: "exp (-1) * exp (γ * t^2 / (2*k)) ≤ exp (γ * (t-1)^2 / (2*k))"
by (metis exp_add exp_le_cancel_iff uminus_add_conv_diff)
have 1: "exp (γ * (t-1)^2 / (2*k)) * (k+l-t choose l) ≤ (k / (k+l))^t * (k+l choose l)"
using mult_right_mono [OF D2 [OF t], of "exp (γ * (t-1)^2 / (2*k))" l] t
by (simp add: γ_def exp_minus field_simps)
have 2: "(k / (k+l)) powr (- real t) * exp (γ * (t-1)^2 / (2*k)) * (k+l-t choose l) ≤ (k+l choose l)"
using mult_right_mono [OF 1, of "(1-γ) powr (- real t)"] t
by (simp add: powr_minus γ_def powr_realpow mult_ac divide_simps)
then have 3: "(1-γ) powr (- real t) * exp (γ * (t-1)^2 / (2*k)) * (k-t+l choose l) ≤ (k+l choose l)"
by (simp add: kkl)
show ?thesis
apply (rule order_trans [OF _ 3])
using "*" less_eq_real_def by fastforce
qed
subsection ‹Lemma 9.3›
definition "ok_fun_93g ≡ λγ k. (nat ⌈k powr (3/4)⌉) * log 2 k - (ok_fun_71 γ k + ok_fun_94 k) + 1"
lemma ok_fun_93g:
assumes "0 < γ" "γ < 1"
shows "ok_fun_93g γ ∈ o(real)"
proof -
have "(λk. (nat ⌈k powr (3/4)⌉) * log 2 k) ∈ o(real)"
by real_asymp
then show ?thesis
unfolding ok_fun_93g_def
by (intro ok_fun_71 [OF assms] ok_fun_94 sum_in_smallo const_smallo_real)
qed
definition "ok_fun_93h ≡ λγ k. (2 / (1-γ)) * k powr (19/20) * (ln γ + 2 * ln k)
+ ok_fun_93g γ k * ln 2"
lemma ok_fun_93h:
assumes "0 < γ" "γ < 1"
shows "ok_fun_93h γ ∈ o(real)"
proof -
have "(λk. (2 / (1-γ)) * k powr (19/20) * (ln γ + 2 * ln k)) ∈ o(real)"
by real_asymp
then show ?thesis
unfolding ok_fun_93h_def by (metis (mono_tags) ok_fun_93g assms sum_in_smallo(1) cmult_in_smallo_iff')
qed
lemma ok_fun_93h_uniform:
assumes μ01: "0<μ0" "μ1<1"
assumes "e>0"
shows "∀⇧∞k. ∀μ. μ ∈ {μ0..μ1} ⟶ ¦ok_fun_93h μ k¦ / k ≤ e"
proof -
define f where "f ≡ λk. ok_fun_73 k + ok_fun_74 k + ok_fun_76 k + ok_fun_94 k"
define g where "g ≡ λμ k. 2 * real k powr (19/20) * (ln μ + 2 * ln k) / (1-μ)"
have g: "∀⇧∞k. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ ¦g μ k¦ / k ≤ e" if "e>0" for e
proof (intro eventually_all_geI1 [where L = "nat⌈1 / μ0⌉"])
show "∀⇧∞k. ¦g μ1 k¦ / real k ≤ e"
using assms that unfolding g_def by real_asymp
next
fix k μ
assume le_e: "¦g μ1 k¦ / k ≤ e" and μ: "μ0 ≤ μ" "μ ≤ μ1" and k: "nat ⌈1/μ0⌉ ≤ k"
then have "k>0"
using assms gr0I by force
have ln_k: "ln k ≥ ln (1/μ0)"
using k ‹0<μ0› ln_mono by fastforce
with μ μ01
have "¦ln μ + 2 * ln (real k)¦ ≤ ¦ln μ1 + 2 * ln (real k)¦"
by (smt (verit) ln_div ln_mono ln_one)
with μ k ‹μ1 < 1›
have "¦g μ k¦ ≤ ¦g μ1 k¦"
by (simp add: g_def abs_mult frac_le mult_mono)
then show "¦g μ k¦ / real k ≤ e"
by (smt (verit, best) divide_right_mono le_e of_nat_less_0_iff)
qed
have eq93: "ok_fun_93h μ k = g μ k +
⌈k powr (3/4)⌉ * ln k - ((ok_fun_72 μ k + f k) - 1) * ln 2" for μ k
by (simp add: ok_fun_93h_def g_def ok_fun_71_def ok_fun_93g_def f_def log_def field_simps)
have ln2: "ln 2 ≥ (0::real)"
by simp
have le93: "¦ok_fun_93h μ k¦
≤ ¦g μ k¦ + ¦⌈k powr (3/4)⌉ * ln k¦ + (¦ok_fun_72 μ k¦ + ¦f k¦ + 1) * ln 2" for μ k
unfolding eq93
by (smt (verit, best) mult.commute ln_gt_zero_iff mult_le_cancel_left_pos mult_minus_left)
define e5 where "e5 ≡ e/5"
have "e5 > 0"
by (simp add: ‹e>0› e5_def)
then have A: "∀⇧∞k. ∀μ. μ ∈ {μ0..μ1} ⟶ ¦g μ k¦ / k ≤ e5"
using g by simp
have B: "∀⇧∞k. ¦⌈k powr (3/4)⌉ * ln k¦ / k ≤ e5"
using ‹0 < e5› by real_asymp
have C: "∀⇧∞k. ∀μ. μ ∈ {μ0..μ1} ⟶ ¦ok_fun_72 μ k¦ * ln 2 / k ≤ e5"
using ln2 assms ok_fun_72_uniform[OF μ01, of "e5 / ln 2"] ‹e5 > 0›
by (simp add: divide_simps)
have "f ∈ o(real)"
by (simp add: f_def ok_fun_73 ok_fun_74 ok_fun_76 ok_fun_94 sum_in_smallo(1))
then have D: "∀⇧∞k. ¦f k¦ * ln 2 / k ≤ e5"
using ‹e5 > 0› ln2
by (force simp: smallo_def field_simps eventually_at_top_dense dest!: spec [where x="e5 / ln 2"])
have E: "∀⇧∞k. ln 2 / k ≤ e5"
using ‹e5 > 0› ln2 by real_asymp
have "∀⇧∞k. ∀μ. μ ∈ {μ0..μ1} ⟶ ¦ok_fun_93h μ k¦ / real k ≤ e5+e5+e5+e5+e5"
using A B C D E
apply eventually_elim
by (fastforce simp: add_divide_distrib distrib_right
intro!: order_trans [OF divide_right_mono [OF le93]])
then show ?thesis
by (simp add: e5_def)
qed
context P0_min
begin
definition "Big_Far_9_3 ≡
λμ l. Big_ZZ_8_5 μ l ∧ Big_X_7_1 μ l ∧ Big_Y_6_2 μ l ∧ Big_Red_5_3 μ l
∧ (∀k≥l. p0_min - 3 * eps k > 1/k ∧ k≥2
∧ ¦ok_fun_93h μ k / (μ * (1 + 1 / (exp 1 * (1-μ))))¦ / k ≤ 0.667 - 2/3)"
lemma Big_Far_9_3:
assumes "0<μ0" "μ0≤μ1" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_Far_9_3 μ l"
proof -
define d where "d ≡ λμ::real. μ * (1 + 1 / (exp 1 * (1-μ)))"
have "d μ0 > 0"
using assms by (auto simp: d_def divide_simps add_pos_pos)
then have dgt: "d μ ≥ d μ0" if "μ ∈ {μ0..μ1}" for μ
using that assms by (auto simp: d_def frac_le mult_mono)
define e::real where "e ≡ 0.667 - 2/3"
have "e>0"
by (simp add: e_def)
have *: "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ (∀k≥l. ¦ok_fun_93h μ k / d μ¦ / k ≤ e)"
proof -
have "∀⇧∞l. ∀k≥l. (∀μ. μ ∈ {μ0..μ1} ⟶ ¦ok_fun_93h μ k¦ / k ≤ d μ0 * e)"
using mult_pos_pos[OF ‹d μ0 > 0› ‹e>0›] assms
using ok_fun_93h_uniform eventually_all_ge_at_top
by blast
then show ?thesis
apply eventually_elim
using dgt ‹0 < d μ0› ‹0 < e›
by (auto simp: mult_ac divide_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
(smt (verit) mult_less_cancel_left nat_neq_iff of_nat_0_le_iff)
qed
with p0_min show ?thesis
unfolding Big_Far_9_3_def eps_def d_def e_def
using assms Big_ZZ_8_5 Big_X_7_1 Big_Y_6_2 Big_Red_5_3
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_ge_at_top; real_asymp)
done
qed
end
lemma "(λk. (nat ⌈real k powr (3/4)⌉) * log 2 k) ∈ o(real)"
by real_asymp
lemma RN34_le_2powr_ok:
fixes l k::nat
assumes "l ≤ k" "0<k"
defines "l34 ≡ nat ⌈real l powr (3/4)⌉"
shows "RN k l34 ≤ 2 powr (⌈k powr (3/4)⌉ * log 2 k)"
proof -
have §: "⌈l powr (3/4)⌉ ≤ ⌈k powr (3/4)⌉"
by (simp add: assms(1) ceiling_mono powr_mono2)
have "RN k l34 ≤ k powr (l34-1)"
using RN_le_argpower' ‹k>0› powr_realpow by auto
also have "… ≤ k powr l34"
using ‹k>0› powr_mono by force
also have "… ≤ 2 powr (l34 * log 2 k)"
by (smt (verit, best) mult.commute ‹k>0› of_nat_0_less_iff powr_log_cancel powr_powr)
also have "… ≤ 2 powr (⌈real k powr (3/4)⌉ * log 2 k)"
unfolding l34_def
proof (intro powr_mono powr_mono2 mult_mono ceiling_mono of_nat_mono nat_mono ‹l ≤ k›)
show "0 ≤ real_of_int ⌈k powr (3/4)⌉"
by (meson le_of_int_ceiling order.trans powr_ge_pzero)
qed (use assms § in auto)
finally show ?thesis .
qed
text ‹Here @{term n} really refers to the cardinality of @{term V},
so actually @{term nV}›
lemma (in Book') Far_9_3:
defines "δ ≡ min (1/200) (γ/20)"
defines "ℛ ≡ Step_class {red_step}"
defines "t ≡ card ℛ"
assumes γ15: "γ ≤ 1/5" and p0: "p0 ≥ 1/4"
and nge: "n ≥ exp (-δ * real k) * (k+l choose l)"
and X0ge: "card X0 ≥ n/2"
assumes big: "Big_Far_9_3 γ l"
shows "t ≥ 2*k / 3"
proof -
define 𝒮 where "𝒮 ≡ Step_class {dboost_step}"
have "k≥2" and big85: "Big_ZZ_8_5 γ l" and big71: "Big_X_7_1 γ l"
and big62: "Big_Y_6_2 γ l" and big53: "Big_Red_5_3 γ l"
using big l_le_k by (auto simp: Big_Far_9_3_def)
define l34 where "l34 ≡ nat ⌈real l powr (3/4)⌉"
have "l34 > 0"
using l34_def ln0 by fastforce
have γ01: "0 < γ" "γ < 1"
using ln0 l_le_k by (auto simp: γ_def)
then have bigbeta01: "0 < bigbeta" "bigbeta < 1"
using big53 assms bigbeta_gt0 bigbeta_less1 by (auto simp: bigbeta_def)
have one_minus: "1-γ = real k / (real k + real l)"
using ln0 by (simp add: γ_def divide_simps)
have "t < k"
using red_step_limit by (auto simp: ℛ_def t_def)
have f: "2 powr ok_fun_94 k * γ powr (- real l) * (1-γ) powr (- real k)
≤ k+l choose l"
unfolding γ_def using fact_9_4 l_le_k ln0 by blast
have powr_combine_right: "x powr a * (x powr b * y) = x powr (a+b) * y" for x y a b::real
by (simp add: powr_add)
have "(2 powr ok_fun_71 γ k * 2 powr ok_fun_94 k) * (bigbeta/γ) ^ card 𝒮 * (exp (-δ*k) * (1-γ) powr (- real k + t) / 2)
≤ 2 powr ok_fun_71 γ k * γ^l * (1-γ) ^ t * (bigbeta/γ) ^ card 𝒮 * (exp (-δ*k) * (k+l choose l) / 2)"
using γ01 ‹0<bigbeta› mult_right_mono [OF f, of "2 powr ok_fun_71 γ k * γ^l * (1-γ) ^ t * (bigbeta/γ) ^ card 𝒮 * (exp (-δ*k)) / 2"]
by (simp add: mult_ac zero_le_mult_iff powr_minus powr_diff divide_simps powr_realpow)
also have "… ≤ 2 powr ok_fun_71 γ k * γ^l * (1-γ) ^ t * (bigbeta/γ) ^ card 𝒮 * card X0"
proof (intro mult_left_mono order_refl)
show "exp (-δ * k) * real (k+l choose l) / 2 ≤ real (card X0)"
using X0ge nge by force
show "0 ≤ 2 powr ok_fun_71 γ k * γ ^ l * (1-γ) ^ t * (bigbeta/γ) ^ card 𝒮"
using γ01 bigbeta_ge0 by (force simp: bigbeta_def)
qed
also have "… ≤ card (Xseq halted_point)"
unfolding ℛ_def 𝒮_def t_def using big
by (intro X_7_1) (auto simp: Big_Far_9_3_def)
also have "… ≤ RN k l34"
proof -
have "p0 - 3 * eps k > 1/k" and "pee halted_point ≥ p0 - 3 * eps k"
using l_le_k big p0_ge Y_6_2_halted by (auto simp: Big_Far_9_3_def γ_def)
then show ?thesis
using halted_point_halted γ01
by (fastforce simp: step_terminating_iff termination_condition_def pee_def l34_def)
qed
also have "… ≤ 2 powr (⌈k powr (3/4)⌉ * log 2 k)"
using RN34_le_2powr_ok l34_def l_le_k ln0 by blast
finally have "2 powr (ok_fun_71 γ k + ok_fun_94 k) * (bigbeta/γ) ^ card 𝒮
* exp (-δ*k) * (1-γ) powr (- real k + t) / 2
≤ 2 powr (⌈k powr (3/4)⌉ * log 2 k)"
by (simp add: powr_add)
then have le_2_powr_g: "exp (-δ*k) * (1-γ) powr (- real k + t) * (bigbeta/γ) ^ card 𝒮
≤ 2 powr ok_fun_93g γ k"
using ‹k≥2› by (simp add: ok_fun_93g_def field_simps powr_add powr_diff flip: powr_realpow)
let ?ξ = "bigbeta * t / (1-γ) + (2 / (1-γ)) * k powr (19/20)"
have bigbeta_le: "bigbeta ≤ γ" and bigbeta_ge: "bigbeta ≥ 1 / (real k)⇧2"
using bigbeta_def γ01 big53 bigbeta_le bigbeta_ge_square by blast+
define φ where "φ ≡ λu. (u / (1-γ)) * ln (γ/u)"
have ln_eq: "ln (γ / (γ / exp 1)) / (1-γ) = 1/(1-γ)"
using γ01 by simp
have φ: "φ (γ / exp 1) ≥ φ bigbeta"
proof (cases "γ / exp 1 ≤ bigbeta")
case True
show ?thesis
proof (intro DERIV_nonpos_imp_nonincreasing [where f = φ])
fix x
assume x: "γ / exp 1 ≤ x" "x ≤ bigbeta"
with γ01 have "x>0"
by (smt (verit, best) divide_pos_pos exp_gt_zero)
with γ01 x have "ln (γ/x) / (1-γ) - 1 / (1-γ) ≤ 0"
by (smt (verit, ccfv_SIG) divide_pos_pos exp_gt_zero frac_le ln_eq ln_mono)
with x ‹x>0› γ01 show "∃D. (φ has_real_derivative D) (at x) ∧ D ≤ 0"
unfolding φ_def by (intro exI conjI derivative_eq_intros | force)+
qed (simp add: True)
next
case False
show ?thesis
proof (intro DERIV_nonneg_imp_nondecreasing [where f = φ])
fix x
assume x: "bigbeta ≤ x" "x ≤ γ / exp 1"
with bigbeta01 γ01 have "x>0" by linarith
with γ01 x have "ln (γ/x) / (1-γ) - 1 / (1-γ) ≥ 0"
by (smt (verit, best) frac_le ln_eq ln_mono zero_less_divide_iff)
with x ‹x>0› γ01 show "∃D. (φ has_real_derivative D) (at x) ∧ D ≥ 0"
unfolding φ_def
by (intro exI conjI derivative_eq_intros | force)+
qed (use False in force)
qed
define c where "c ≡ λx::real. 1 + 1 / (exp 1 * (1-x))"
have mono_c: "mono_on {0<..<1} c"
by (auto simp: monotone_on_def c_def field_simps)
have cgt0: "c x > 0" if "x<1" for x
using that by (simp add: add_pos_nonneg c_def)
have "card 𝒮 ≤ bigbeta * t / (1-bigbeta) + (2 / (1-γ)) * k powr (19/20)"
using ZZ_8_5 [OF big85] by (auto simp: ℛ_def 𝒮_def t_def)
also have "… ≤ ?ξ"
using bigbeta_le by (simp add: γ01 bigbeta_ge0 frac_le)
finally have "card 𝒮 ≤ ?ξ" .
with bigbeta_le bigbeta01 have "?ξ * ln (bigbeta/γ) ≤ card 𝒮 * ln (bigbeta/γ)"
by (simp add: mult_right_mono_neg)
then have "-?ξ * ln (γ/bigbeta) ≤ card 𝒮 * ln (bigbeta/γ)"
using bigbeta01 γ01 by (smt (verit) ln_div minus_mult_minus)
then have "γ * (real k - t) - δ*k - ?ξ * ln (γ/bigbeta) ≤ γ * (real k - t) - δ*k + card 𝒮 * ln (bigbeta/γ)"
by linarith
also have "… ≤ (t - real k) * ln (1-γ) - δ*k + card 𝒮 * ln (bigbeta/γ)"
using ‹t < k› γ01 mult_right_mono [OF ln_add_one_self_le_self2 [of "-γ"], of "real k - t"]
by (simp add: algebra_simps)
also have "… = ln (exp (-δ*k) * (1-γ) powr (- real k + t) * (bigbeta/γ) ^ card 𝒮)"
using γ01 bigbeta01 by (simp add: ln_mult ln_div ln_realpow ln_powr)
also have "… ≤ ln (2 powr ok_fun_93g γ k)"
using le_2_powr_g γ01 bigbeta01 by simp
also have "… = ok_fun_93g γ k * ln 2"
by (auto simp: ln_powr)
finally have "γ * (real k - t) - δ*k - ?ξ * ln (γ/bigbeta) ≤ ok_fun_93g γ k * ln 2" .
then have "γ * (real k - t) ≤ ?ξ * ln (γ/bigbeta) + δ*k + ok_fun_93g γ k * ln 2"
by simp
also have "… ≤ (bigbeta * t / (1-γ)) * ln (γ/bigbeta) + δ*k + ok_fun_93h γ k"
proof -
have "γ/bigbeta ≤ γ * (real k)⇧2"
using kn0 bigbeta_le bigbeta_ge ‹bigbeta>0› by (simp add: field_simps)
then have X: "ln (γ/bigbeta) ≤ ln γ + 2 * ln k"
using ‹bigbeta>0› ‹γ>0› kn0
by (metis divide_pos_pos ln_mono ln_mult mult_2 mult_pos_pos of_nat_0_less_iff power2_eq_square)
show ?thesis
using mult_right_mono [OF X, of "2 * k powr (19/20) / (1-γ)"] ‹γ<1›
by (simp add: ok_fun_93h_def algebra_simps)
qed
also have "… ≤ ((γ / exp 1) * t / (1-γ)) + δ*k + ok_fun_93h γ k"
using γ01 mult_right_mono [OF φ, of t] by (simp add: φ_def mult_ac)
finally have "γ * (real k - t) ≤ ((γ / exp 1) * t / (1-γ)) + δ*k + ok_fun_93h γ k" .
then have "(γ-δ) * k - ok_fun_93h γ k ≤ t * γ * c γ"
by (simp add: c_def algebra_simps)
then have "((γ-δ) * k - ok_fun_93h γ k) / (γ * c γ) ≤ t"
using γ01 cgt0 by (simp add: pos_divide_le_eq)
then have *: "t ≥ (1-δ / γ) * inverse (c γ) * k - ok_fun_93h γ k / (γ * c γ)"
using γ01 cgt0[of γ] by (simp add: divide_simps)
define f47 where "f47 ≡ λx. (1 - 1/(200*x)) * inverse (c x)"
have "concave_on {1/10..1/5} f47"
unfolding f47_def
proof (intro concave_on_mul)
show "concave_on {1/10..1/5} (λx. 1 - 1/(200*x))"
proof (intro f''_le0_imp_concave)
fix x::real
assume "x ∈ {1/10..1/5}"
then have x01: "0<x" "x<1" by auto
show "((λx. (1 - 1/(200*x))) has_real_derivative 1/(200*x^2)) (at x)"
using x01 by (intro derivative_eq_intros | force simp: eval_nat_numeral)+
show "((λx. 1/(200*x^2)) has_real_derivative -1/(100*x^3)) (at x)"
using x01 by (intro derivative_eq_intros | force simp: eval_nat_numeral)+
show "-1/(100*x^3) ≤ 0"
using x01 by (simp add: divide_simps)
qed auto
show "concave_on {1/10..1/5} (λx. inverse (c x))"
proof (intro f''_le0_imp_concave)
fix x::real
assume "x ∈ {1/10..1/5}"
then have x01: "0<x" "x<1" by auto
have swap: "u * (x-1) = (-u) * (1-x)" for u
by (metis minus_diff_eq minus_mult_commute)
have §: "exp 1 * (x - 1) < 0"
using x01 by (meson exp_gt_zero less_iff_diff_less_0 mult_less_0_iff)
then have non0: "1 + 1 / (exp 1 * (1-x)) ≠ 0"
using x01 by (smt (verit) exp_gt_zero mult_pos_pos zero_less_divide_iff)
let ?f1 = "λx. -exp 1 /(- 1 + exp 1 * (- 1 + x))⇧2"
let ?f2 = "λx. 2*exp(1)^2/(-1 + exp(1)*(-1 + x))^3"
show "((λx. inverse (c x)) has_real_derivative ?f1 x) (at x)"
unfolding c_def power2_eq_square
using x01 § non0
apply (intro exI conjI derivative_eq_intros | force)+
apply (simp add: divide_simps square_eq_iff swap)
done
show "(?f1 has_real_derivative ?f2 x) (at x)"
using x01 §
by (intro derivative_eq_intros | force simp: divide_simps eval_nat_numeral)+
show "?f2 (x::real) ≤ 0"
using x01 § by (simp add: divide_simps)
qed auto
show "mono_on {(1::real)/10..1/5} (λx. 1 - 1 / (200 * x))"
by (auto simp: monotone_on_def frac_le)
show "monotone_on {1/10..1/5} (≤) (λx y. y ≤ x) (λx. inverse (c x))"
using mono_c cgt0 by (auto simp: monotone_on_def divide_simps)
qed (auto simp: c_def)
moreover have "f47(1/10) > 0.667"
unfolding f47_def c_def by (approximation 15)
moreover have "f47(1/5) > 0.667"
unfolding f47_def c_def by (approximation 15)
ultimately have 47: "f47 x > 0.667" if "x ∈ {1/10..1/5}" for x
using concave_on_ge_min that by fastforce
define f48 where "f48 ≡ λx. (1 - 1/20) * inverse (c x)"
have 48: "f48 x > 0.667" if "x ∈ {0<..<1/10}" for x
proof -
have "(0.667::real) < (1 - 1/20) * inverse(c(1/10))"
unfolding c_def by (approximation 15)
also have "… ≤ f48 x"
using that unfolding f48_def c_def
by (intro mult_mono le_imp_inverse_le add_mono divide_left_mono) (auto simp: add_pos_pos)
finally show ?thesis .
qed
define e::real where "e ≡ 0.667 - 2/3"
have BIGH: "abs (ok_fun_93h γ k / (γ * c γ)) / k ≤ e"
using big l_le_k unfolding Big_Far_9_3_def all_imp_conj_distrib e_def [symmetric] c_def
by auto
consider "γ ∈ {0<..<1/10}" | "γ ∈ {1/10..1/5}"
using δ_def ‹γ ≤ 1/5› γ01 by fastforce
then show ?thesis
proof cases
case 1
then have δγ: "δ / γ = 1/20"
by (auto simp: δ_def)
have "(2/3::real) ≤ f48 γ - e"
using 48[OF 1] e_def by force
also have "… ≤ (1-δ / γ) * inverse (c γ) - ok_fun_93h γ k / (γ * c γ) / k"
unfolding f48_def δγ using BIGH
by (smt (verit, best) divide_nonneg_nonneg of_nat_0_le_iff zero_less_divide_iff)
finally
have A: "2/3 ≤ (1-δ / γ) * inverse (c γ) - ok_fun_93h γ k / (γ * c γ) / k" .
have "real (2 * k) / 3 ≤ (1 - δ / γ) * inverse (c γ) * k - ok_fun_93h γ k / (γ * c γ)"
using mult_left_mono [OF A, of k] cgt0 [of γ] γ01 kn0
by (simp add: divide_simps mult_ac)
with * show ?thesis
by linarith
next
case 2
then have δγ: "δ / γ = 1/(200*γ)"
by (auto simp: δ_def)
have "(2/3::real) ≤ f47 γ - e"
using 47[OF 2] e_def by force
also have "… ≤ (1 - δ / γ) * inverse (c γ) - ok_fun_93h γ k / (γ * c γ) / k"
unfolding f47_def δγ using BIGH
by (smt (verit, best) divide_right_mono of_nat_0_le_iff)
finally
have "2/3 ≤ (1 - δ / γ) * inverse (c γ) - ok_fun_93h γ k / (γ * c γ) / k" .
from mult_left_mono [OF this, of k] cgt0 [of γ] γ01 kn0
have "real (2 * k) / 3 ≤ (1 - δ / γ) * inverse (c γ) * k - ok_fun_93h γ k / (γ * c γ)"
by (simp add: divide_simps mult_ac)
with * show ?thesis
by linarith
qed
qed
subsection ‹Lemma 9.5›
context P0_min
begin
text ‹Again stolen from Bhavik: cannot allow a dependence on @{term γ}›
definition "ok_fun_95a ≡ λk. ok_fun_61 k - (2 + 4 * k powr (19/20))"
definition "ok_fun_95b ≡ λk. ln 2 * ok_fun_95a k - 1"
lemma ok_fun_95a: "ok_fun_95a ∈ o(real)"
proof -
have "(λk. 2 + 4 * k powr (19/20)) ∈ o(real)"
by real_asymp
then show ?thesis
unfolding ok_fun_95a_def using ok_fun_61 sum_in_smallo by blast
qed
lemma ok_fun_95b: "ok_fun_95b ∈ o(real)"
using ok_fun_95a by (auto simp: ok_fun_95b_def sum_in_smallo const_smallo_real)
definition "Big_Far_9_5 ≡ λμ l. Big_Red_5_3 μ l ∧ Big_Y_6_1 μ l ∧ Big_ZZ_8_5 μ l"
lemma Big_Far_9_5:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ Big_Far_9_5 μ l"
using assms Big_Red_5_3 Big_Y_6_1 Big_ZZ_8_5
unfolding Big_Far_9_5_def eps_def
by (simp add: eventually_conj_iff all_imp_conj_distrib)
end
text ‹Y0 is an additional assumption found in Bhavik's version. (He had a couple of others).
The first $o(k)$ function adjusts for the error in $n/2$›
lemma (in Book') Far_9_5:
fixes δ η::real
defines "ℛ ≡ Step_class {red_step}"
defines "t ≡ card ℛ"
assumes nV: "real nV ≥ exp (-δ * k) * (k+l choose l)" and Y0: "card Y0 ≥ nV div 2"
assumes p0: "1/2 ≤ 1-γ-η" "1-γ-η ≤ p0" and "0≤η"
assumes big: "Big_Far_9_5 γ l"
shows "card (Yseq halted_point) ≥
exp (-δ * k + ok_fun_95b k) * (1-γ-η) powr (γ*t / (1-γ)) * ((1-γ-η)/(1-γ))^t
* exp (γ * (real t)⇧2 / (2*k)) * (k-t+l choose l)" (is "_ ≥ ?rhs")
proof -
define 𝒮 where "𝒮 ≡ Step_class {dboost_step}"
define s where "s ≡ card 𝒮"
have γ01: "0 < γ" "γ < 1"
using ln0 l_le_k by (auto simp: γ_def)
have big85: "Big_ZZ_8_5 γ l" and big61: "Big_Y_6_1 γ l" and big53: "Big_Red_5_3 γ l"
using big by (auto simp: Big_Far_9_5_def)
have "bigbeta ≤ γ"
using bigbeta_def γ01 big53 bigbeta_le by blast
have 85: "s ≤ (bigbeta / (1-bigbeta)) * t + (2 / (1-γ)) * k powr (19/20)"
unfolding s_def t_def ℛ_def 𝒮_def using ZZ_8_5 γ01 big85 by blast
also have "… ≤ (γ / (1-γ)) * t + (2 / (1-γ)) * k powr (19/20)"
using γ01 ‹bigbeta ≤ γ› by (intro add_mono mult_right_mono frac_le) auto
finally have D85: "s ≤ γ*t / (1-γ) + (2 / (1-γ)) * k powr (19/20)"
by auto
have "t<k"
unfolding t_def ℛ_def using γ01 red_step_limit by blast
have st: "card (Step_class {red_step,dboost_step}) = t + s"
using γ01
by (simp add: s_def t_def ℛ_def 𝒮_def Step_class_insert_NO_MATCH card_Un_disjnt disjnt_Step_class)
then have 61: "2 powr (ok_fun_61 k) * p0 ^ (t+s) * card Y0 ≤ card (Yseq halted_point)"
using Y_6_1[OF big61] card_XY0 γ01 by (simp add: divide_simps)
have "(1-γ-η) powr (t + γ*t / (1-γ)) * nV ≤ (1-γ-η) powr (t+s - 4 * k powr (19/20)) * (4 * card Y0)"
proof (intro mult_mono)
show "(1-γ-η) powr (t + γ*t / (1-γ)) ≤ (1-γ-η) powr (t+s - 4 * k powr (19/20))"
proof (intro powr_mono')
have "γ ≤ 1/2"
using ‹0≤η› p0 by linarith
then have 22: "1 / (1 - γ) ≤ 2"
using divide_le_eq_1 by fastforce
show "real (t + s) - 4 * real k powr (19 / 20) ≤ real t + γ * real t / (1 - γ)"
using mult_left_mono [OF 22, of "2 * real k powr (19 / 20)"] D85
by (simp add: algebra_simps)
next
show "0 ≤ 1 - γ - η" "1 - γ - η ≤ 1"
using assms γ01 by linarith+
qed
have "nV ≥ 2"
by (metis nontriv wellformed two_edges card_mono ex_in_conv finV)
then have "nV ≤ 4 * (nV div 2)" by linarith
also have "… ≤ 4 * card Y0"
using Y0 mult_le_mono2 by presburger
finally show "real nV ≤ real (4 * card Y0)"
by force
qed (use Y0 in auto)
also have "… ≤ (1-γ-η) powr (t+s) / (1-γ-η) powr (4 * k powr (19/20)) * (4 * card Y0)"
by (simp add: divide_powr_uminus powr_diff)
also have "… ≤ (1-γ-η) powr (t+s) / (1/2) powr (4 * k powr (19/20)) * (4 * card Y0)"
proof (intro mult_mono divide_left_mono)
show "(1/2) powr (4 * k powr (19/20)) ≤ (1-γ-η) powr (4 * k powr (19/20))"
using γ01 p0 ‹0≤η› by (intro powr_mono_both') auto
qed (use p0 in auto)
also have "… ≤ p0 powr (t+s) / (1/2) powr (4 * k powr (19/20)) * (4 * card Y0)"
using p0 powr_mono2 by (intro mult_mono divide_right_mono) auto
also have "… = (2 powr (2 + 4 * k powr (19/20))) * p0 ^ (t+s) * card Y0"
using p0_01 by (simp add: powr_divide powr_add power_add powr_realpow)
finally have "2 powr (ok_fun_95a k) * (1-γ-η) powr (t + γ*t / (1-γ)) * nV ≤ 2 powr (ok_fun_61 k) * p0 ^ (t+s) * card Y0"
by (simp add: ok_fun_95a_def powr_diff field_simps)
with 61 have *: "card (Yseq halted_point) ≥ 2 powr (ok_fun_95a k) * (1-γ-η) powr (t + γ*t / (1-γ)) * nV"
by linarith
have F: "exp (ok_fun_95b k) = 2 powr ok_fun_95a k * exp (- 1)"
by (simp add: ok_fun_95b_def exp_diff exp_minus powr_def field_simps)
have "?rhs
≤ exp (-δ * k) * 2 powr (ok_fun_95a k) * exp (-1) * (1-γ-η) powr (γ*t / (1-γ))
* (((1-γ-η)/(1-γ)) ^t * exp (γ * (real t)⇧2 / real(2*k)) * (k-t+l choose l))"
unfolding exp_add F by simp
also have "… ≤ exp (-δ * k) * 2 powr (ok_fun_95a k) * (1-γ-η) powr (γ*t / (1-γ))
* (exp (-1) * ((1-γ-η)/(1-γ)) ^t * exp (γ * (real t)⇧2 / real(2*k)) * (k-t+l choose l))"
by (simp add: mult.assoc)
also have "… ≤ 2 powr (ok_fun_95a k) * (1-γ-η) powr (t + γ*t / (1-γ)) * exp (-δ * k)
* (exp (-1) * (1-γ) powr (- real t) * exp (γ * (real t)⇧2 / real(2*k)) * (k-t+l choose l))"
using p0 γ01
unfolding powr_add powr_minus by (simp add: mult_ac divide_simps flip: powr_realpow)
also have "… ≤ 2 powr (ok_fun_95a k) * (1-γ-η) powr (t + γ*t / (1-γ)) * exp (-δ * k) * (k+l choose l)"
proof (cases "t=0")
case False
then show ?thesis
unfolding γ_def using ‹t<k› by (intro mult_mono order_refl Far_9_6) auto
qed auto
also have "… ≤ 2 powr (ok_fun_95a k) * (1-γ-η) powr (t + γ*t / (1-γ)) * nV"
using nV mult_left_mono by fastforce
also have "… ≤ card (Yseq halted_point)"
by (rule *)
finally show ?thesis .
qed
subsection ‹Lemma 9.2 actual proof›
context P0_min
begin
lemma error_9_2:
assumes "μ>0" "d > 0"
shows "∀⇧∞k. ok_fun_95b k + μ * real k / d ≥ 0"
proof -
have "∀⇧∞k. ¦ok_fun_95b k¦ ≤ (μ/d) * k"
using ok_fun_95b assms unfolding smallo_def
by (auto dest!: spec [where x = "μ/d"])
then show ?thesis
by eventually_elim force
qed
definition "Big_Far_9_2 ≡ λμ l. Big_Far_9_3 μ l ∧ Big_Far_9_5 μ l ∧ (∀k≥l. ok_fun_95b k + μ*k/60 ≥ 0)"
lemma Big_Far_9_2:
assumes "0<μ0" "μ0≤μ1" "μ1<1"
shows "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ Big_Far_9_2 μ l"
proof -
have "∀⇧∞l. ∀k≥l. (∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 0 ≤ ok_fun_95b k + μ * k / 60)"
using assms
apply (intro eventually_all_ge_at_top eventually_all_geI0 error_9_2)
apply (auto simp: divide_right_mono mult_right_mono elim!: order_trans)
done
then show ?thesis
using assms Big_Far_9_3 Big_Far_9_5
unfolding Big_Far_9_2_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
by (smt (verit, ccfv_threshold) eventually_sequentially)
qed
end
lemma (in Book') Far_9_2_conclusion:
defines "ℛ ≡ Step_class {red_step}"
defines "t ≡ card ℛ"
assumes Y: "(k-t+l choose l) ≤ card (Yseq halted_point)"
shows False
proof -
have "t<k"
unfolding t_def ℛ_def using red_step_limit by blast
have "RN (k-t) l ≤ card (Yseq halted_point)"
by (metis Y add.commute RN_commute RN_le_choose le_trans)
then obtain K
where Ksub: "K ⊆ Yseq halted_point"
and K: "card K = k-t ∧ clique K Red ∨ card K = l ∧ clique K Blue"
by (meson Red_Blue_RN Yseq_subset_V size_clique_def)
show False
using K
proof
assume K: "card K = k - t ∧ clique K Red"
have "clique (K ∪ Aseq halted_point) Red"
proof (intro clique_Un)
show "clique (Aseq halted_point) Red"
by (meson A_Red_clique valid_state_seq)
have "all_edges_betw_un (Aseq halted_point) (Yseq halted_point) ⊆ Red"
using valid_state_seq Ksub
by (auto simp: valid_state_def RB_state_def all_edges_betw_un_Un2)
then show "all_edges_betw_un K (Aseq halted_point) ⊆ Red"
using Ksub all_edges_betw_un_commute all_edges_betw_un_mono2 by blast
show "K ⊆ V"
using Ksub Yseq_subset_V by blast
qed (use K Aseq_subset_V in auto)
moreover have "card (K ∪ Aseq halted_point) = k"
proof -
have eqt: "card (Aseq halted_point) = t"
using red_step_eq_Aseq ℛ_def t_def by simp
have "card (K ∪ Aseq halted_point) = card K + card (Aseq halted_point) "
proof (intro card_Un_disjoint)
show "finite K"
by (meson Ksub Yseq_subset_V finV finite_subset)
have "disjnt (Yseq halted_point) (Aseq halted_point)"
using valid_state_seq by (auto simp: valid_state_def disjoint_state_def)
with Ksub show "K ∩ Aseq halted_point = {}"
by (auto simp: disjnt_def)
qed (simp add: finite_Aseq)
also have "… = k"
using eqt K ‹t < k› by simp
finally show ?thesis .
qed
moreover have "K ∪ Aseq halted_point ⊆ V"
using Aseq_subset_V Ksub Yseq_subset_V by blast
ultimately show False
using no_Red_clique size_clique_def by blast
next
assume "card K = l ∧ clique K Blue"
then show False
using Ksub Yseq_subset_V no_Blue_clique size_clique_def by blast
qed
qed
text ‹A little tricky to express since the Book locale assumes that
there are no cliques in the original graph (page 9). So it's a contrapositive›
lemma (in Book') Far_9_2_aux:
fixes δ η::real
defines "δ ≡ γ/20"
assumes 0: "real (card X0) ≥ nV/2" "card Y0 ≥ nV div 2" "p0 ≥ 1-γ-η"
assumes γ: "γ ≤ 1/10" and η: "0≤η" "η ≤ γ/15"
assumes nV: "real nV ≥ exp (-δ * k) * (k+l choose l)"
assumes big: "Big_Far_9_2 γ l"
shows False
proof -
define ℛ where "ℛ ≡ Step_class {red_step}"
define t where "t ≡ card ℛ"
have γ01: "0 < γ" "γ < 1"
using ln0 l_le_k by (auto simp: γ_def)
have big93: "Big_Far_9_3 γ l"
using big by (auto simp: Big_Far_9_2_def)
have t23: "t ≥ 2*k / 3"
unfolding t_def ℛ_def
proof (rule Far_9_3)
show "γ ≤ 1/5"
using γ unfolding γ_def by linarith
have "min (1/200) (γ / 20) ≥ δ"
unfolding δ_def using γ ln0 by (simp add: γ_def)
then show "exp (- min (1/200) (γ / 20) * k) * (k+l choose l) ≤ nV"
using δ_def γ_def nV by force
show "1/4 ≤ p0"
using η γ 0 by linarith
show "Big_Far_9_3 (γ) l"
using γ_def big93 by blast
qed (use assms in auto)
have "t<k"
unfolding t_def ℛ_def using γ01 red_step_limit by blast
have ge_half: "1/2 ≤ 1-γ-η"
using γ η by linarith
have "exp (-1/3 + (1/5::real)) ≤ exp (10/9 * ln (134/150))"
by (approximation 9)
also have "… ≤ exp (1 / (1-γ) * ln (134/150))"
using γ by (auto simp: divide_simps)
also have "… ≤ exp (1 / (1-γ) * ln (1-γ-η))"
using γ η by (auto simp: divide_simps)
also have "… = (1-γ-η) powr (1 / (1-γ))"
using ge_half by (simp add: powr_def)
finally have A: "exp (-1/3 + 1/5) ≤ (1-γ-η) powr (1 / (1-γ))" .
have "3*t / (10*k) ≤ (-1/3 + 1/5) + t/(2*k)"
using t23 kn0 by (simp add: divide_simps)
from mult_right_mono [OF this, of "γ*t"] γ01
have "3*γ*t⇧2 / (10*k) ≤ γ*t*(-1/3 + 1/5) + γ*t⇧2/(2*k)"
by (simp add: eval_nat_numeral algebra_simps)
then have "exp (3*γ*t⇧2 / (10*k)) ≤ exp (-1/3 + 1/5) powr (γ*t) * exp (γ*t⇧2/(2*k))"
by (simp add: mult_exp_exp exp_powr_real)
also have "… ≤ (1-γ-η) powr ((γ*t) / (1-γ)) * exp (γ*t⇧2/(2*k))"
using γ01 powr_powr powr_mono2 [of "γ*t" "exp (-1/3 + 1/5)", OF _ _ A]
by (intro mult_right_mono) auto
finally have B: "exp (3*γ*t⇧2 / (10*k)) ≤ (1-γ-η) powr ((γ*t) / (1-γ)) * exp (γ*t⇧2/(2*k))" .
have "(2*k / 3)^2 ≤ t⇧2"
using t23 by auto
from kn0 γ01 mult_right_mono [OF this, of "γ/(80*k)"]
have C: "δ*k + γ*k/60 ≤ 3*γ*t⇧2 / (20*k)"
by (simp add: field_simps δ_def eval_nat_numeral)
have "exp (- 3*γ*t / (20*k)) ≤ exp (-3 * η/2)"
proof -
have "1 ≤ 3/2 * t/k"
using t23 kn0 by (auto simp: divide_simps)
from mult_right_mono [OF this, of "γ/15"] γ01 η
show ?thesis
by simp
qed
also have "… ≤ 1 - η / (1-γ)"
proof -
have §: "2/3 ≤ (1 - γ - η)"
using γ η by linarith
have "1 / (1-η / (1-γ)) = 1 + η / (1-γ-η)"
using ge_half η by (simp add: divide_simps split: if_split_asm)
also have "… ≤ 1 + 3 * η / 2"
using mult_right_mono [OF §, of η] η ge_half by (simp add: field_simps)
also have "… ≤ exp (3 * η / 2)"
using exp_minus_ge [of "-3*η/2"] by simp
finally show ?thesis
using γ01 ge_half
by (simp add: exp_minus divide_simps mult.commute split: if_split_asm)
qed
also have "… = (1-γ-η) / (1-γ)"
using γ01 by (simp add: divide_simps)
finally have "exp (- 3*γ*t / (20*k)) ≤ (1-γ-η) / (1-γ)" .
from powr_mono2 [of t, OF _ _ this] ge_half γ01
have D: "exp (- 3*γ*t⇧2 / (20*k)) ≤ ((1-γ-η) / (1-γ))^t"
by (simp add: eval_nat_numeral powr_powr exp_powr_real mult_ac flip: powr_realpow)
have "(k-t+l choose l) ≤ card (Yseq halted_point)"
proof -
have "1 * real(k-t+l choose l)
≤ exp (ok_fun_95b k + γ*k/60) * (k-t+l choose l)"
using big l_le_k unfolding Big_Far_9_2_def
by (intro mult_right_mono mult_ge1_I) auto
also have "… ≤ exp (3*γ*t⇧2 / (20*k) + -δ * k + ok_fun_95b k) * (k-t+l choose l)"
using C by simp
also have "… = exp (3*γ*t⇧2 / (10*k)) * exp (-δ * k + ok_fun_95b k) * exp (- 3*γ*t⇧2 / (20*k))
* (k-t+l choose l)"
by (simp flip: exp_add)
also have "… ≤ exp (3*γ*t⇧2 / (10*k)) * exp (-δ * k + ok_fun_95b k) * ((1-γ-η)/(1-γ))^t
* (k-t+l choose l)"
using γ01 ge_half D by (intro mult_right_mono) auto
also have "… ≤ (1-γ-η) powr (γ*t / (1-γ)) * exp (γ * t⇧2 / (2*k)) * exp (-δ * k + ok_fun_95b k)
* ((1-γ-η)/(1-γ))^t * (k-t+l choose l)"
using γ01 ge_half by (intro mult_right_mono B) auto
also have "… = exp (-δ * k + ok_fun_95b k) * (1-γ-η) powr (γ*t / (1-γ)) * ((1-γ-η)/(1-γ))^t
* exp (γ * (real t)⇧2 / (2*k)) * (k-t+l choose l)"
by (simp add: mult_ac)
also have 95: "… ≤ real (card (Yseq halted_point))"
unfolding t_def ℛ_def
proof (rule Far_9_5)
show "1/2 ≤ 1 - γ - η"
using ge_half γ_def by blast
show "Big_Far_9_5 (γ) l"
using Big_Far_9_2_def big unfolding γ_def by presburger
qed (use assms in auto)
finally show ?thesis by simp
qed
then show False
using Far_9_2_conclusion by (simp flip: ℛ_def t_def)
qed
text ‹Mediation of 9.2 (and 10.2) from locale @{term Book_Basis} to the book locales
with the starting sets of equal size›
lemma (in No_Cliques) Basis_imp_Book:
assumes gd: "p0_min ≤ graph_density Red"
assumes μ01: "0 < μ" "μ < 1"
obtains X0 Y0 where "l≥2" "card X0 ≥ real nV / 2" "card Y0 = gorder div 2"
and "X0 = V ∖ Y0" "Y0⊆V"
and "graph_density Red ≤ gen_density Red X0 Y0"
and "Book V E p0_min Red Blue l k μ X0 Y0"
proof -
have "Red ≠ {}"
using gd p0_min by (auto simp: graph_density_def)
then have "gorder ≥ 2"
by (metis Red_E card_mono equals0I finV subset_empty two_edges wellformed)
then have div2: "0 < gorder div 2" "gorder div 2 < gorder"
by auto
then obtain Y0 where Y0: "card Y0 = gorder div 2" "Y0⊆V"
"graph_density Red ≤ gen_density Red (V∖Y0) Y0"
by (metis complete Red_E exists_density_edge_density gen_density_commute)
define X0 where "X0 ≡ V ∖ Y0"
interpret Book V E p0_min Red Blue l k μ X0 Y0
proof
show "X0⊆V" "disjnt X0 Y0"
by (auto simp: X0_def disjnt_iff)
show "p0_min ≤ gen_density Red X0 Y0"
using X0_def Y0 gd gen_density_commute p0_min by auto
qed (use assms ‹Y0⊆V› in auto)
have False if "l<2"
using that unfolding less_2_cases_iff
proof
assume "l = Suc 0"
with Y0 div2 show False
by (metis RN_1' no_Red_clique no_Blue_clique Red_Blue_RN Suc_leI kn0)
qed (use ln0 in auto)
with l_le_k have "l≥2"
by force
have card_X0: "card X0 ≥ nV/2"
using Y0 ‹Y0⊆V› unfolding X0_def
by (simp add: card_Diff_subset finite_Y0)
then show thesis
using Book_axioms X0_def Y0 ‹2 ≤ l› that by blast
qed
text ‹Material that needs to be proved \textbf{outside} the book locales›
text ‹As above, for @{term Book'}›
lemma (in No_Cliques) Basis_imp_Book':
assumes gd: "p0_min ≤ graph_density Red"
assumes l: "0<l" "l≤k"
obtains X0 Y0 where "l≥2" "card X0 ≥ real nV / 2" "card Y0 = gorder div 2" and "X0 = V ∖ Y0" "Y0⊆V"
and "graph_density Red ≤ gen_density Red X0 Y0"
and "Book' V E p0_min Red Blue l k (real l / (real k + real l)) X0 Y0"
proof -
define γ where "γ ≡ real l / (real k + real l)"
have "0 < γ" "γ < 1"
using l by (auto simp: γ_def)
with assms Basis_imp_Book [of γ]
obtain X0 Y0 where *: "l≥2" "card X0 ≥ real nV / 2" "card Y0 = gorder div 2" "X0 = V ∖ Y0" "Y0⊆V"
"graph_density Red ≤ gen_density Red X0 Y0" "Book V E p0_min Red Blue l k γ X0 Y0"
by blast
then interpret Book V E p0_min Red Blue l k γ X0 Y0
by blast
have "Book' V E p0_min Red Blue l k γ X0 Y0"
using Book' γ_def by auto
with * assms show ?thesis
using γ_def that by blast
qed
lemma (in No_Cliques) Far_9_2:
fixes δ γ η::real
defines "γ ≡ l / (real k + real l)"
defines "δ ≡ γ/20"
assumes nV: "real nV ≥ exp (-δ * k) * (k+l choose l)"
assumes gd: "graph_density Red ≥ 1-γ-η" and p0_min_OK: "p0_min ≤ 1-γ-η"
assumes big: "Big_Far_9_2 γ l"
assumes "γ ≤ 1/10" and η: "0≤η" "η ≤ γ/15"
shows False
proof -
obtain X0 Y0 where "l≥2" and card_X0: "card X0 ≥ real nV / 2"
and card_Y0: "card Y0 = gorder div 2"
and X0_def: "X0 = V ∖ Y0" and "Y0⊆V"
and gd_le: "graph_density Red ≤ gen_density Red X0 Y0"
and "Book' V E p0_min Red Blue l k γ X0 Y0"
using Basis_imp_Book' assms p0_min no_Red_clique no_Blue_clique ln0 by auto
then interpret Book' V E p0_min Red Blue l k γ X0 Y0
by blast
show False
proof (intro Far_9_2_aux [of η])
show "1 - γ - η ≤ p0"
using X0_def γ_def gd gd_le gen_density_commute p0_def by auto
qed (use assms card_X0 card_Y0 in auto)
qed
subsection ‹Theorem 9.1›
text ‹An arithmetical lemma proved outside of the locales›
lemma kl_choose:
fixes l k::nat
assumes "m<l" "k>0"
defines "PM ≡ ∏i<m. (l - real i) / (k+l-real i)"
shows "(k+l choose l) = (k+l-m choose (l-m)) / PM"
proof -
have inj: "inj_on (λi. i-m) {m..<l}"
by (auto simp: inj_on_def)
have "(∏i<l. (k+l-i) / (l-i)) / (∏i<m. (k+l-i) / (l-i))
= (∏i = m..<l. (k+l-i) / (l-i))"
using prod_divide_nat_ivl [of 0 m l "λi. (k+l-i) / (l-i)"] ‹m < l›
by (simp add: atLeast0LessThan)
also have "… = (∏i<l - m. (k+l-m - i) / (l-m-i))"
apply (intro prod.reindex_cong [OF inj, symmetric])
by (auto simp: image_minus_const_atLeastLessThan_nat)
finally
have "(∏i < l-m. (k+l-m - i) / (l-m-i))
= (∏i < l. (k+l-i) / (l-i)) / (∏i<m. (k+l-i) / (l-i))"
by linarith
also have "… = (k+l choose l) * inverse (∏i<m. (k+l-i) / (l-i))"
by (simp add: field_simps atLeast0LessThan binomial_altdef_of_nat)
also have "… = (k+l choose l) * PM"
unfolding PM_def using ‹m < l› ‹k>0›
by (simp add: atLeast0LessThan flip: prod_inversef)
finally have "(k+l-m choose (l-m)) = (k+l choose l) * PM"
by (simp add: atLeast0LessThan binomial_altdef_of_nat)
then show "real(k+l choose l) = (k+l-m choose (l-m)) / PM"
by auto
qed
context P0_min
begin
text ‹The proof considers a smaller graph, so @{term l} needs to be so big
that the smaller @{term l'} will be big enough.›
definition Big_Far_9_1 :: "real ⇒ nat ⇒ bool" where
"Big_Far_9_1 ≡ λμ l. l≥3 ∧ (∀l' γ. real l' ≥ (10/11) * μ * real l ⟶ μ⇧2 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_2 γ l')"
text ‹The proof of theorem 10.1 requires a range of values›
lemma Big_Far_9_1:
assumes "0<μ0" "μ0≤1/10"
shows "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ 1/10 ⟶ Big_Far_9_1 μ l"
proof -
have "μ0⇧2 ≤ 1/10"
using assms by (smt (verit, ccfv_threshold) le_divide_eq_1 mult_left_le power2_eq_square)
then have "∀⇧∞l. ∀γ. μ0⇧2 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_2 γ l"
using assms by (intro Big_Far_9_2) auto
then obtain N where N: "∀l≥N. ∀γ. μ0⇧2 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_2 γ l"
using eventually_sequentially by auto
define M where "M ≡ nat⌈11*N / (10*μ0)⌉"
have "(10/11) * μ0 * l ≥ N" if "l ≥ M" for l
using that by (simp add: M_def ‹μ0>0› mult_of_nat_commute pos_divide_le_eq)
with N have "∀l≥M. ∀l' γ. (10/11) * μ0 * l ≤ l' ⟶ μ0⇧2 ≤ γ ∧ γ ≤ 1 / 10 ⟶ Big_Far_9_2 γ l'"
by (smt (verit, ccfv_SIG) of_nat_le_iff)
then have "∀⇧∞l. ∀l' γ. (10/11) * μ0 * l ≤ l' ⟶ μ0⇧2 ≤ γ ∧ γ ≤ 1 / 10 ⟶ Big_Far_9_2 γ l'"
by (auto simp: eventually_sequentially)
moreover have "∀⇧∞l. l≥3"
by simp
ultimately show ?thesis
unfolding Big_Far_9_1_def
apply eventually_elim
by (smt (verit) ‹0<μ0› mult_left_mono mult_right_mono of_nat_less_0_iff power_mono zero_less_mult_iff)
qed
text ‹The text claims the result for all @{term k} and @{term l}, not just those sufficiently large,
but the $o(k)$ function allowed in the exponent provides a fudge factor›
theorem Far_9_1:
fixes l k::nat
fixes δ γ::real
defines "γ ≡ real l / (real k + real l)"
defines "δ ≡ γ/20"
assumes γ: "γ ≤ 1/10"
assumes big: "Big_Far_9_1 γ l"
assumes p0_min_91: "p0_min ≤ 1 - (1/10) * (1 + 1/15)"
shows "RN k l ≤ exp (-δ*k + 1) * (k+l choose l)"
proof (rule ccontr)
assume non: "¬ RN k l ≤ exp (-δ * k + 1) * (k+l choose l)"
with RN_eq_0_iff have "l>0" by force
with γ have l9k: "9*l ≤ k"
by (auto simp: γ_def divide_simps)
have "l≤k"
using γ_def γ nat_le_real_less by fastforce
with ‹l>0› have "k>0" by linarith
define ξ::real where "ξ ≡ 1/15"
define U_lower_bound_ratio where
"U_lower_bound_ratio ≡ λm. (1+ξ)^m * (∏i<m. (l - real i) / (k+l - real i))"
define n where "n ≡ RN k l - 1"
have "l≥3"
using big by (auto simp: Big_Far_9_1_def)
have "k≥27"
using l9k ‹l≥3› by linarith
have "exp 1 / (exp 1 - 2) < (27::real)"
by (approximation 5)
also have RN27: "… ≤ RN k l"
by (meson RN_3plus' ‹l≥3› ‹k≥27› le_trans numeral_le_real_of_nat_iff)
finally have "exp 1 / (exp 1 - 2) < RN k l" .
moreover have "n < RN k l"
using RN27 by (simp add: n_def)
moreover have "2 < exp (1::real)"
by (approximation 5)
ultimately have nRNe: "n/2 > RN k l / exp 1"
by (simp add: n_def field_split_simps)
have "(k+l choose l) / exp (-1 + δ*k) < RN k l"
by (smt (verit) divide_inverse exp_minus mult_minus_left mult_of_nat_commute non)
then have "(RN k l / exp 1) * exp (δ*k) > (k+l choose l)"
unfolding exp_add exp_minus by (simp add: field_simps)
with nRNe have n2exp_gt: "(n/2) * exp (δ*k) > (k+l choose l)"
by (smt (verit, best) exp_gt_zero mult_le_cancel_right_pos)
then have nexp_gt: "n * exp (δ*k) > (k+l choose l)"
by simp
define V where "V ≡ {..<n}"
define E where "E ≡ all_edges V"
interpret Book_Basis V E
proof qed (auto simp: V_def E_def comp_sgraph.wellformed comp_sgraph.two_edges)
have [simp]: "nV = n"
by (simp add: V_def)
then obtain Red Blue
where Red_E: "Red ⊆ E" and Blue_def: "Blue = E-Red"
and no_Red_K: "¬ (∃K. size_clique k K Red)"
and no_Blue_K: "¬ (∃K. size_clique l K Blue)"
by (metis ‹n < RN k l› less_RN_Red_Blue)
have Blue_E: "Blue ⊆ E" and disjnt_Red_Blue: "disjnt Red Blue"
and Blue_eq: "Blue = all_edges V - Red"
using complete by (auto simp: Blue_def disjnt_iff E_def)
define is_good_clique where
"is_good_clique ≡ λi K. clique K Blue ∧ K ⊆ V ∧
card (V ∩ (⋂w∈K. Neighbours Blue w))
≥ real i * U_lower_bound_ratio (card K) - card K"
have is_good_card: "card K < l" if "is_good_clique i K" for i K
using no_Blue_K that unfolding is_good_clique_def
by (metis nat_neq_iff size_clique_def size_clique_smaller)
define GC where "GC ≡ {C. is_good_clique n C}"
have "GC ≠ {}"
by (auto simp: GC_def is_good_clique_def U_lower_bound_ratio_def E_def V_def)
have "GC ⊆ Pow V"
by (auto simp: is_good_clique_def GC_def)
then have "finite GC"
by (simp add: finV finite_subset)
then obtain W where "W ∈ GC" and MaxW: "Max (card ` GC) = card W"
using ‹GC ≠ {}› obtains_MAX by blast
then have 49: "is_good_clique n W"
using GC_def by blast
have max49: "¬ is_good_clique n (insert x W)" if "x∈V∖W" for x
proof
assume x: "is_good_clique n (insert x W)"
then have "card (insert x W) = Suc (card W)"
using finV is_good_clique_def finite_subset that by fastforce
with x ‹finite GC› have "Max (card ` GC) ≥ Suc (card W)"
by (simp add: GC_def rev_image_eqI)
then show False
by (simp add: MaxW)
qed
have "W⊆V"
using 49 by (auto simp: is_good_clique_def)
define m where "m ≡ card W"
define γ' where "γ' ≡ (l - real m) / (k+l-real m)"
define η where "η ≡ ξ * γ'"
have Red_Blue_RN: "∃K ⊆ X. size_clique m K Red ∨ size_clique n K Blue"
if "card X ≥ RN m n" "X⊆V" for m n and X
using partn_lst_imp_is_clique_RN [OF is_Ramsey_number_RN [of m n]] finV that
unfolding is_clique_RN_def size_clique_def clique_indep_def Blue_eq
by (metis clique_iff_indep finite_subset subset_trans)
define U where "U ≡ V ∩ (⋂w∈W. Neighbours Blue w)"
define EU where "EU ≡ E ∩ Pow U"
define RedU where "RedU ≡ Red ∩ Pow U"
define BlueU where "BlueU ≡ Blue ∩ Pow U"
have "RN k l > 0"
using ‹n < RN k l› by auto
have "γ' > 0"
using is_good_card [OF 49] by (simp add: γ'_def m_def)
then have "η > 0"
by (simp add: η_def ξ_def)
have "finite W"
using ‹W ⊆ V› finV finite_subset by (auto simp: V_def)
have "U ⊆ V" and VUU: "V ∩ U = U"
by (force simp: U_def)+
have "disjnt U W"
using Blue_E not_own_Neighbour unfolding E_def V_def U_def disjnt_iff by blast
have "m<l"
using 49 is_good_card m_def by blast
then have γ1516: "γ' ≤ 15/16"
using γ_def γ by (simp add: γ'_def divide_simps)
then have γ'_le1: "(1+ξ) * γ' ≤ 1"
by (simp add: ξ_def)
have cardU: "n * U_lower_bound_ratio m ≤ m + card U"
using 49 VUU unfolding is_good_clique_def U_def m_def by force
obtain [iff]: "finite RedU" "finite BlueU" "RedU ⊆ EU"
using BlueU_def EU_def RedU_def E_def V_def Red_E Blue_E fin_edges finite_subset by blast
have card_RedU_le: "card RedU ≤ card EU"
by (metis EU_def E_def ‹RedU ⊆ EU› card_mono fin_all_edges finite_Int)
interpret UBB: Book_Basis U "E ∩ Pow U" p0_min
proof
fix e
assume "e ∈ E ∩ Pow U"
with two_edges show "e ⊆ U" "card e = 2" by auto
next
show "finite U"
using ‹U ⊆ V› by (simp add: V_def finite_subset)
have "x ∈ E" if "x ∈ all_edges U" for x
using ‹U ⊆ V› all_edges_mono that complete E_def by blast
then show "E ∩ Pow U = all_edges U"
using comp_sgraph.wellformed ‹U ⊆ V› by (auto intro: e_in_all_edges_ss)
qed auto
have clique_W: "size_clique m W Blue"
using 49 is_good_clique_def size_clique_def V_def m_def by blast
define PM where "PM ≡ ∏i<m. (l - real i) / (k+l-real i)"
then have U_lower_m: "U_lower_bound_ratio m = (1+ξ)^m * PM"
using U_lower_bound_ratio_def by blast
have prod_gt0: "PM > 0"
unfolding PM_def using ‹m<l› by (intro prod_pos) auto
have kl_choose: "real(k+l choose l) = (k+l-m choose (l-m)) / PM"
unfolding PM_def using kl_choose ‹0 < k› ‹m < l› by blast
define ekl20 where "ekl20 ≡ exp (k / (20*(k+l)))"
have ekl20_eq: "exp (δ*k) = ekl20^l"
by (simp add: δ_def γ_def ekl20_def field_simps flip: exp_of_nat2_mult)
have "ekl20 ≤ exp(1/20)"
unfolding ekl20_def using ‹m < l› by fastforce
also have "… ≤ (1+ξ)"
unfolding ξ_def by (approximation 10)
finally have exp120: "ekl20 ≤ 1 + ξ" .
have ekl20_gt0: "0 < ekl20"
by (simp add: ekl20_def)
have "3*l + Suc l - q ≤ (k+q choose q) / exp(δ*k) * (1+ξ) ^ (l - q)"
if "1≤q" "q≤l" for q
using that
proof (induction q rule: nat_induct_at_least)
case base
have "ekl20^l = ekl20^(l-1) * ekl20"
by (metis ‹0 < l› power_minus_mult)
also have "… ≤ (1+ξ) ^ (l-1) * ekl20"
using ekl20_def exp120 power_mono by fastforce
also have "… ≤ 2 * (1+ξ) ^ (l-1)"
proof -
have §: "ekl20 ≤ 2"
using ξ_def exp120 by linarith
from mult_right_mono [OF this, of "(1+ξ) ^ (l-1)"]
show ?thesis by (simp add: mult_ac ξ_def)
qed
finally have "ekl20^l ≤ 2 * (1+ξ) ^ (l-1)"
by argo
then have "1/2 ≤ (1+ξ) ^ (l-1) / ekl20^l"
using ekl20_def by auto
moreover have "4 * real l / (1 + real k) ≤ 1/2"
using l9k by (simp add: divide_simps)
ultimately have "4 * real l / (1 + real k) ≤ (1+ξ) ^ (l-1) / ekl20^l"
by linarith
then show ?case
by (simp add: field_simps ekl20_eq)
next
case (Suc q)
then have ‡: "(1+ξ) ^ (l - q) = (1+ξ) * (1+ξ) ^ (l - Suc q)"
by (metis Suc_diff_le diff_Suc_Suc power.simps(2))
have "real(k + q choose q) ≤ real(k + q choose Suc q)" "0 ≤ (1+ξ) ^ (l - Suc q)"
using ‹Suc q ≤ l› l9k by (auto simp: ξ_def binomial_mono)
from mult_right_mono [OF this]
have "(k + q choose q) * (1+ξ) ^ (l - q) / exp (δ * k) - 1
≤ (real (k + q choose q) + (k + q choose Suc q)) * (1+ξ) ^ (l - Suc q) / exp (δ * k)"
unfolding ‡ by (simp add: ξ_def field_simps add_increasing)
with Suc show ?case by force
qed
from ‹m<l› this [of "l-m"]
have "1 + 3*l + real m ≤ (k+l-m choose (l-m)) / exp δ ^ k * (1+ξ) ^ m"
by (simp add: Suc_leI exp_of_nat2_mult)
also have "… ≤ (k+l-m choose (l-m)) / exp (δ * k) * (1+ξ) ^ m"
by (simp add: exp_of_nat2_mult)
also have "… < PM * (real n * (1+ξ) ^ m)"
proof -
have §: "(k+l choose l) / exp (δ * k) < n"
by (simp add: less_eq_real_def nexp_gt pos_divide_less_eq)
show ?thesis
using mult_strict_left_mono [OF §, of "PM * (1+ξ) ^ m"] kl_choose prod_gt0
by (auto simp: field_simps ξ_def)
qed
also have "… = real n * U_lower_bound_ratio m"
by (simp add: U_lower_m)
finally have U_MINUS_M: "3*l + 1 < real n * U_lower_bound_ratio m - m"
by linarith
then have cardU_gt: "card U > 3*l + 1"
using cardU by linarith
with UBB.complete have "card EU > 0" "card U > 1"
by (simp_all add: EU_def UBB.finV card_all_edges)
have BlueU_eq: "BlueU = EU ∖ RedU"
using Blue_eq complete by (fastforce simp: BlueU_def RedU_def EU_def V_def E_def)
have [simp]: "UBB.graph_size = card EU"
using EU_def by blast
have "γ' ≤ γ"
using ‹m<l› ‹k>0› by (simp add: γ_def γ'_def field_simps)
have False if "UBB.graph_density RedU < 1 - γ' - η"
proof -
have §: "UBB.graph_density BlueU ≥ γ' + η"
using that ‹card EU > 0› card_RedU_le
by (simp add: BlueU_eq UBB.graph_density_def diff_divide_distrib card_Diff_subset)
have Nx: "Neighbours BlueU x ∩ (U ∖ {x}) = Neighbours BlueU x" for x
using that by (auto simp: BlueU_eq EU_def Neighbours_def)
have "BlueU ⊆ E ∩ Pow U"
using BlueU_eq EU_def by blast
with UBB.exists_density_edge_density [of 1 BlueU]
obtain x where "x∈U" and x: "UBB.graph_density BlueU ≤ UBB.gen_density BlueU {x} (U∖{x})"
by (metis UBB.complete ‹1 < UBB.gorder› card_1_singletonE insertI1 zero_less_one subsetD)
with § have "γ' + η ≤ UBB.gen_density BlueU (U∖{x}) {x}"
using UBB.gen_density_commute by auto
then have *: "(γ' + η) * (card U - 1) ≤ card (Neighbours BlueU x)"
using ‹BlueU ⊆ E ∩ Pow U› ‹card U > 1› ‹x ∈ U›
by (simp add: UBB.gen_density_def UBB.edge_card_eq_sum_Neighbours UBB.finV divide_simps Nx)
have x: "x ∈ V∖W"
using ‹x ∈ U› ‹U ⊆ V› ‹disjnt U W› by (auto simp: U_def disjnt_iff)
moreover
have "is_good_clique n (insert x W)"
unfolding is_good_clique_def
proof (intro conjI)
show "clique (insert x W) Blue"
proof (intro clique_insert)
show "clique W Blue"
using 49 is_good_clique_def by blast
show "all_edges_betw_un {x} W ⊆ Blue"
using ‹x∈U› by (auto simp: U_def all_edges_betw_un_def insert_commute in_Neighbours_iff)
qed (use ‹W ⊆ V› ‹x ∈ V∖W› in auto)
next
show "insert x W ⊆ V"
using ‹W ⊆ V› ‹x ∈ V∖W› by auto
next
have NB_Int_U: "Neighbours Blue x ∩ U = Neighbours BlueU x"
using ‹x ∈ U› by (auto simp: BlueU_def U_def Neighbours_def)
have ulb_ins: "U_lower_bound_ratio (card (insert x W)) = U_lower_bound_ratio m * (1+ξ) * γ'"
using ‹x ∈ V∖W› ‹finite W› by (simp add: U_lower_bound_ratio_def γ'_def m_def)
have "n * U_lower_bound_ratio (card (insert x W)) = n * U_lower_bound_ratio m * (1+ξ) * γ'"
by (simp add: ulb_ins)
also have "… ≤ real (m + card U) * (1+ξ) * γ'"
using mult_right_mono [OF cardU, of "(1+ξ) * γ'"] ‹0 < η› ‹0 < γ'› η_def by argo
also have "… ≤ m + card U * (1+ξ) * γ'"
using mult_left_mono [OF γ'_le1, of m] by (simp add: algebra_simps)
also have "… ≤ Suc m + (γ' + η) * (UBB.gorder - Suc 0)"
using * ‹x ∈ V∖W› ‹finite W› cardU_gt γ1516
apply (simp add: U_lower_bound_ratio_def ξ_def η_def)
by (simp add: algebra_simps)
also have "… ≤ Suc m + card (V ∩ ⋂ (Neighbours Blue ` insert x W))"
using * NB_Int_U finV by (simp add: U_def Int_ac)
also have "… = real (card (insert x W) + card (V ∩ ⋂ (Neighbours Blue ` insert x W)))"
using x ‹finite W› VUU by (auto simp: U_def m_def)
finally show "n * U_lower_bound_ratio (card(insert x W)) - card(insert x W)
≤ card (V ∩ ⋂ (Neighbours Blue ` insert x W))"
by simp
qed
ultimately show False
using max49 by blast
qed
then have gd_RedU_ge: "UBB.graph_density RedU ≥ 1 - γ' - η" by force
have γ'γ2: "γ' < γ⇧2 ⟷ (real k * real l) + (real l * real l) < (real k * real m) + (real l * (real m * 2))"
using ‹m < l›
apply (simp add: γ'_def γ_def eval_nat_numeral divide_simps; simp add: algebra_simps)
by (metis ‹k>0› mult_less_cancel_left_pos of_nat_0_less_iff distrib_left)
also have "… ⟷ (l * (k+l)) / (k + 2 * l) < m"
using ‹m < l› by (simp add: field_simps)
finally have γ'γ2_iff: "γ' < γ⇧2 ⟷ (l * (k+l)) / (k + 2 * l) < m" .
have extend_Blue_clique: "∃K'. size_clique l K' Blue"
if "K ⊆ U" "size_clique (l-m) K Blue" for K
proof -
have K: "card K = l-m" "clique K Blue"
using that by (auto simp: size_clique_def)
define K' where "K' ≡ K ∪ W"
have "card K' = l"
unfolding K'_def
proof (subst card_Un_disjnt)
show "finite K" "finite W"
using UBB.finV ‹K ⊆ U› finite_subset ‹finite W› by blast+
show "disjnt K W"
using ‹disjnt U W› ‹K ⊆ U› disjnt_subset1 by blast
show "card K + card W = l"
using K ‹m < l› m_def by auto
qed
moreover have "clique K' Blue"
using ‹clique K Blue› clique_W ‹K ⊆ U›
unfolding K'_def size_clique_def U_def
by (force simp: in_Neighbours_iff insert_commute intro: Ramsey.clique_Un)
ultimately show ?thesis
unfolding K'_def size_clique_def using ‹K ⊆ U› ‹U ⊆ V› ‹W ⊆ V› by auto
qed
show False
proof (cases "γ' < γ⇧2")
case True
with γ'γ2 have YKK: "γ*k ≤ m"
using ‹0<k› ‹m < l›
apply (simp add: γ_def field_simps)
by (smt (verit, best) distrib_left mult_left_mono of_nat_0_le_iff)
have ln1ξ: "ln (1+ξ) * 20 ≥ 1"
unfolding ξ_def by (approximation 10)
with YKK have §: "m * ln (1+ξ) ≥ δ * k"
unfolding δ_def using zero_le_one mult_mono by fastforce
have powerm: "(1+ξ)^m ≥ exp (δ * k)"
using exp_mono [OF §]
by (smt (verit) η_def ‹0 < η› ‹0 < γ'› exp_ln_iff exp_of_nat_mult zero_le_mult_iff)
have "n * (1+ξ)^m ≥ (k+l choose l)"
by (smt (verit, best) mult_left_mono nexp_gt of_nat_0_le_iff powerm)
then have **: "n * U_lower_bound_ratio m ≥ (k+l-m choose (l-m))"
using ‹m<l› prod_gt0 kl_choose by (auto simp: U_lower_m field_simps)
have m_le_choose: "m ≤ (k+l-m-1 choose (l-m))"
proof (cases "m=0")
case False
have "m ≤ (k+l-m-1 choose 1)"
using ‹l≤k› ‹m<l› by simp
also have "… ≤ (k+l-m-1 choose (l-m))"
using False ‹l≤k› ‹m<l› by (intro binomial_mono) auto
finally have m_le_choose: "m ≤ (k+l-m-1 choose (l-m))" .
then show ?thesis .
qed auto
have "RN k (l-m) ≤ k + (l-m) - 2 choose (k - 1)"
by (rule RN_le_choose_strong)
also have "… ≤ (k+l-m-1 choose k)"
using ‹l≤k› ‹m<l› choose_reduce_nat by simp
also have "… = (k+l-m-1 choose (l-m-1))"
using ‹m<l› by (simp add: binomial_symmetric [of k])
also have "… = (k+l-m choose (l-m)) - (k+l-m-1 choose (l-m))"
using ‹l≤k› ‹m<l› choose_reduce_nat by simp
also have "… ≤ (k+l-m choose (l-m)) - m"
using m_le_choose by linarith
finally have "RN k (l-m) ≤ (k+l-m choose (l-m)) - m" .
then have "card U ≥ RN k (l-m)"
using 49 ** VUU by (force simp: is_good_clique_def U_def m_def)
with Red_Blue_RN no_Red_K ‹U ⊆ V›
obtain K where "K ⊆ U" "size_clique (l-m) K Blue" by meson
then show False
using no_Blue_K extend_Blue_clique by blast
next
case False
have YMK: "γ-γ' ≤ m/k"
using ln0 ‹m<l›
apply (simp add: γ_def γ'_def divide_simps)
apply (simp add: algebra_simps)
by (smt (verit, best) mult_left_mono mult_right_mono nat_less_real_le of_nat_0_le_iff)
define δ' where "δ' ≡ γ'/20"
have no_RedU_K: "¬ (∃K. UBB.size_clique k K RedU)"
unfolding UBB.size_clique_def RedU_def
by (metis Int_subset_iff VUU all_edges_subset_iff_clique no_Red_K size_clique_def)
have "(∃K. UBB.size_clique k K RedU) ∨ (∃K. UBB.size_clique (l-m) K BlueU)"
proof (rule ccontr)
assume neg: "¬ ((∃K. UBB.size_clique k K RedU) ∨ (∃K. UBB.size_clique (l-m) K BlueU))"
interpret UBB_NC: No_Cliques U "E ∩ Pow U" p0_min RedU BlueU "l-m" k
proof
show "BlueU = E ∩ Pow U ∖ RedU"
using BlueU_eq EU_def by fastforce
qed (use neg EU_def ‹RedU ⊆ EU› no_RedU_K ‹l≤k› in auto)
show False
proof (intro UBB_NC.Far_9_2)
have "exp (δ*k) * exp (-δ'*k) = exp (γ*k/20 - γ'*k/20)"
unfolding δ_def δ'_def by (simp add: mult_exp_exp)
also have "… ≤ exp (m/20)"
using YMK ‹0 < k› by (simp add: left_diff_distrib divide_simps)
also have "… ≤ (1+ξ)^m"
proof -
have "ln (16 / 15) * 20 ≥ (1::real)"
by (approximation 5)
from mult_left_mono [OF this]
show ?thesis
by (simp add: ξ_def powr_def mult_ac flip: powr_realpow)
qed
finally have expexp: "exp (δ*k) * exp (-δ'*k) ≤ (1+ξ) ^ m" .
have "exp (-δ'*k) * (k + (l-m) choose (l-m)) = exp (-δ'*k) * PM * (k+l choose l)"
using ‹m < l› kl_choose by force
also have "… < (n/2) * exp (δ*k) * exp (-δ'*k) * PM"
using n2exp_gt prod_gt0 by auto
also have "… ≤ (n/2) * (1+ξ) ^ m * PM"
using expexp less_eq_real_def prod_gt0 by fastforce
also have "… ≤ n * U_lower_bound_ratio m - m"
using PM_def U_MINUS_M U_lower_bound_ratio_def ‹m < l› by fastforce
finally have "exp (-δ'*k) * (k + (l-m) choose (l-m)) ≤ n * U_lower_bound_ratio m - m"
by linarith
also have "… ≤ UBB.nV"
using cardU by linarith
finally have "exp (-δ'*k) * (k + (l-m) choose (l-m)) ≤ UBB.nV" .
then show "exp (- ((l-m) / (k + real (l-m)) / 20) * k) * (k + (l-m) choose (l-m)) ≤ UBB.nV"
using ‹m < l› by (simp add: δ'_def γ'_def) argo
next
show "1 - real (l-m) / (real k + real (l-m)) - η ≤ UBB.graph_density RedU"
using gd_RedU_ge ‹γ' ≤ γ› ‹m < l› unfolding γ_def γ'_def
by (smt (verit) less_or_eq_imp_le of_nat_add of_nat_diff)
have "p0_min ≤ 1 - γ - η"
using ‹γ' ≤ γ› γ p0_min_91 by (auto simp: η_def ξ_def)
also have "… ≤ 1 - (l-m) / (real k + real (l-m)) - η"
using ‹γ' ≤ γ› ‹m<l› by (simp add: γ_def γ'_def algebra_simps)
finally show "p0_min ≤ 1 - (l-m) / (real k + real (l-m)) - η" .
next
have "m ≤ l * (k + real l) / (k + 2 * real l)"
using False γ'γ2_iff by auto
also have "… ≤ l * (1 - (10/11)*γ)"
using γ ‹l>0› by (simp add: γ_def field_split_simps)
finally have "m ≤ real l * (1 - (10/11)*γ)"
by force
then have "real l - real m ≥ (10/11) * γ * l"
by (simp add: algebra_simps)
then have "Big_Far_9_2 γ' (l-m)"
using False big ‹γ' ≤ γ› γ ‹m<l›
by (simp add: Big_Far_9_1_def)
then show "Big_Far_9_2 ((l-m) / (real k + real (l-m))) (l-m)"
by (simp add: γ'_def ‹m < l› add_diff_eq less_or_eq_imp_le)
show "(l-m) / (real k + real (l-m)) ≤ 1/10"
using γ γ_def ‹m < l› by fastforce
show "0 ≤ η"
using ‹0 < η› by linarith
show "η ≤ (l-m) / (real k + real (l-m)) / 15"
using mult_right_mono [OF ‹γ' ≤ γ›, of ξ]
by (simp add: η_def γ'_def ‹m < l› ξ_def add_diff_eq less_or_eq_imp_le mult.commute)
qed
qed
with no_RedU_K obtain K where "K ⊆ U" "UBB.size_clique (l-m) K BlueU"
by (meson UBB.size_clique_def)
then show False
using no_Blue_K extend_Blue_clique VUU
unfolding UBB.size_clique_def size_clique_def BlueU_def
by (metis Int_subset_iff all_edges_subset_iff_clique)
qed
qed
end
end