Theory Zigzag
section ‹The Zigzag Lemma›
theory Zigzag imports Bounding_X
begin
subsection ‹Lemma 8.1 (the actual Zigzag Lemma)›
definition "Big_ZZ_8_2 ≡ λk. (1 + eps k powr (1/2)) ≥ (1 + eps k) powr (eps k powr (-1/4))"
text ‹An inequality that pops up in the proof of (39)›
definition "Big39 ≡ λk. 1/2 ≤ (1 + eps k) powr (-2 * eps k powr (-1/2))"
text ‹Two inequalities that pops up in the proof of (42)›
definition "Big42a ≡ λk. (1 + eps k)⇧2 / (1 - eps k powr (1/2)) ≤ 1 + 2 * k powr (-1/16)"
definition "Big42b ≡ λk. 2 * k powr (-1/16) * k
+ (1 + 2 * ln k / eps k + 2 * k powr (7/8)) / (1 - eps k powr (1/2))
≤ real k powr (19/20)"
definition "Big_ZZ_8_1 ≡
λμ l. Big_Blue_4_1 μ l ∧ Big_Red_5_1 μ l ∧ Big_Red_5_3 μ l ∧ Big_Y_6_5_Bblue l
∧ (∀k. k≥l ⟶ Big_height_upper_bound k ∧ Big_ZZ_8_2 k ∧ k≥16 ∧ Big39 k
∧ Big42a k ∧ Big42b k)"
text ‹@{term "k≥16"} is for @{text Y_6_5_Red}›
lemma Big_ZZ_8_1:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_1 μ l"
using assms Big_Blue_4_1 Big_Red_5_1 Big_Red_5_3 Big_Y_6_5_Bblue
unfolding Big_ZZ_8_1_def Big_ZZ_8_2_def Big39_def Big42a_def Big42b_def
eventually_conj_iff all_imp_conj_distrib eps_def
apply (simp add: eventually_conj_iff eventually_frequently_const_simps)
apply (intro conjI strip eventually_all_ge_at_top Big_height_upper_bound; real_asymp)
done
lemma (in Book) ZZ_8_1:
assumes big: "Big_ZZ_8_1 μ l"
defines "ℛ ≡ Step_class {red_step}"
defines "sum_SS ≡ (∑i∈dboost_star. (1 - beta i) / beta i)"
shows "sum_SS ≤ card ℛ + k powr (19/20)"
proof -
define pp where "pp ≡ λi h. if h=1 then min (pseq i) (qfun 1)
else if pseq i ≤ qfun (h-1) then qfun (h-1)
else if pseq i ≥ qfun h then qfun h
else pseq i"
define Δ where "Δ ≡ λi. pseq (Suc i) - pseq i"
define ΔΔ where "ΔΔ ≡ λi h. pp (Suc i) h - pp i h"
have pp_eq: "pp i h = (if h=1 then min (pseq i) (qfun 1)
else max (qfun (h-1)) (min (pseq i) (qfun h)))" for i h
using qfun_mono [of "h-1" h] by (auto simp: pp_def max_def)
define maxh where "maxh ≡ nat⌊2 * ln k / ε⌋ + 1"
have maxh: "⋀pseq. pseq≤1 ⟹ hgt pseq ≤ 2 * ln k / ε" and "k≥16"
using big l_le_k by (auto simp: Big_ZZ_8_1_def height_upper_bound)
then have "1 ≤ 2 * ln k / ε"
using hgt_gt0 [of 1] by force
then have "maxh > 1"
by (simp add: maxh_def eps_gt0)
have "hgt pseq < maxh" if "pseq≤1"for pseq
using that kn0 maxh[of "pseq"] unfolding maxh_def by linarith
then have hgt_le_maxh: "hgt (pseq i) < maxh" for i
using pee_le1 by auto
have pp_eq_hgt [simp]: "pp i (hgt (pseq i)) = pseq i" for i
using hgt_less_imp_qfun_less [of "hgt (pseq i) - 1" "pseq i"]
using hgt_works [of "pseq i"] hgt_gt0 [of "pseq i"] kn0 pp_eq by force
have pp_less_hgt [simp]: "pp i h = qfun h" if "0<h" "h < hgt (pseq i)" for h i
proof (cases "h=1")
case True
then show ?thesis
using hgt_less_imp_qfun_less pp_def that by auto
next
case False
with that show ?thesis
using alpha_def alpha_ge0 hgt_less_imp_qfun_less pp_eq by force
qed
have pp_gt_hgt [simp]: "pp i h = qfun (h-1)" if "h > hgt (pseq i)" for h i
using hgt_gt0 [of "pseq i"] kn0 that
by (simp add: pp_def hgt_le_imp_qfun_ge)
have Δ0: "Δ i ≥ 0 ⟷ (∀h>0. ΔΔ i h ≥ 0)" for i
proof (intro iffI strip)
fix h::nat
assume "0 ≤ Δ i" "0 < h" then show "0 ≤ ΔΔ i h"
using qfun_mono [of "h-1" h] kn0 by (auto simp: Δ_def ΔΔ_def pp_def)
next
assume "∀h>0. 0 ≤ ΔΔ i h"
then have "pseq i ≤ pp (Suc i) (hgt (pseq i))"
unfolding ΔΔ_def
by (smt (verit, best) hgt_gt0 pp_eq_hgt)
then show "0 ≤ Δ i"
using hgt_less_imp_qfun_less [of "hgt (pseq i) - 1" "pseq i"]
using hgt_gt0 [of "pseq i"] kn0
by (simp add: Δ_def pp_def split: if_split_asm)
qed
have sum_pp_aux: "(∑h=Suc 0..n. pp i h)
= (if hgt (pseq i) ≤ n then pseq i + (∑h=1..<n. qfun h) else (∑h=1..n. qfun h))"
if "n>0" for n i
using that
proof (induction n)
case (Suc n)
show ?case
proof (cases "n=0")
case True
then show ?thesis
using kn0 hgt_Least [of 1 "pseq i"]
by (simp add: pp_def hgt_le_imp_qfun_ge min_def)
next
case False
with Suc show ?thesis
by (simp split: if_split_asm) (smt (verit) le_Suc_eq not_less_eq pp_eq_hgt sum.head_if)
qed
qed auto
have sum_pp: "(∑h=Suc 0..maxh. pp i h) = pseq i + (∑h=1..<maxh. qfun h)" for i
using ‹1 < maxh› by (simp add: hgt_le_maxh less_or_eq_imp_le sum_pp_aux)
have 33: "Δ i = (∑h=1..maxh. ΔΔ i h)" for i
by (simp add: ΔΔ_def Δ_def sum_subtractf sum_pp)
have "(∑i<halted_point. ΔΔ i h) = 0"
if "⋀i. i≤halted_point ⟹ h > hgt (pseq i)" for h
using that by (simp add: sum.neutral ΔΔ_def)
then have B: "(∑i<halted_point. ΔΔ i h) = 0" if "h ≥ maxh" for h
by (meson hgt_le_maxh le_simps le_trans not_less_eq that)
have "(∑h=Suc 0..maxh. ∑i<halted_point. ΔΔ i h / alpha h) ≤ (∑h=Suc 0..maxh. 1)"
proof (intro sum_mono)
fix h
assume "h ∈ {Suc 0..maxh}"
have "(∑i<halted_point. ΔΔ i h) ≤ alpha h"
using qfun_mono [of "h-1" h] kn0
unfolding ΔΔ_def alpha_def sum_lessThan_telescope [where f = "λi. pp i h"]
by (auto simp: pp_def pee_eq_p0)
then show "(∑i<halted_point. ΔΔ i h / alpha h) ≤ 1"
using alpha_ge0 [of h] by (simp add: divide_simps flip: sum_divide_distrib)
qed
also have "… ≤ 1 + 2 * ln k / ε"
using ‹maxh > 1› by (simp add: maxh_def)
finally have 34: "(∑h=Suc 0..maxh. ∑i<halted_point. ΔΔ i h / alpha h) ≤ 1 + 2 * ln k / ε" .
define 𝒟 where "𝒟 ≡ Step_class {dreg_step}"
define ℬ where "ℬ ≡ Step_class {bblue_step}"
define 𝒮 where "𝒮 ≡ Step_class {dboost_step}"
have "dboost_star ⊆ 𝒮"
unfolding dboost_star_def 𝒮_def dboost_star_def by auto
have BD_disj: "ℬ∩𝒟 = {}" and disj: "ℛ∩ℬ = {}" "𝒮∩ℬ = {}" "ℛ∩𝒟 = {}" "𝒮∩𝒟 = {}" "ℛ∩𝒮 = {}"
by (auto simp: 𝒟_def ℛ_def ℬ_def 𝒮_def Step_class_def)
have [simp]: "finite 𝒟" "finite ℬ" "finite ℛ" "finite 𝒮"
using finite_components assms
by (auto simp: 𝒟_def ℬ_def ℛ_def 𝒮_def Step_class_insert_NO_MATCH)
have "card ℛ < k"
using red_step_limit by (auto simp: ℛ_def)
have R52: "pseq (Suc i) - pseq i ≥ (1 - ε) * ((1 - beta i) / beta i) * alpha (hgt (pseq i))"
and beta_gt0: "beta i > 0"
and R53: "pseq (Suc i) ≥ pseq i ∧ beta i ≥ 1 / (real k)⇧2"
if "i ∈ 𝒮" for i
using big Red_5_2 that by (auto simp: Big_ZZ_8_1_def Red_5_3 ℬ_def 𝒮_def)
have cardℬ: "card ℬ ≤ l powr (3/4)" and bigY65B: "Big_Y_6_5_Bblue l"
using big bblue_step_limit by (auto simp: Big_ZZ_8_1_def ℬ_def)
have ΔΔ_ge0: "ΔΔ i h ≥ 0" if "i ∈ 𝒮" "h ≥ 1" for i h
using that R53 [OF ‹i ∈ 𝒮›] by (fastforce simp: ΔΔ_def pp_eq)
have ΔΔ_eq_0: "ΔΔ i h = 0" if "hgt (pseq i) ≤ hgt (pseq (Suc i))" "hgt (pseq (Suc i)) < h" for h i
using ΔΔ_def that by fastforce
define oneminus where "oneminus ≡ 1 - ε powr (1/2)"
have 35: "oneminus * ((1 - beta i) / beta i)
≤ (∑h=1..maxh. ΔΔ i h / alpha h)" (is "?L ≤ ?R")
if "i ∈ dboost_star" for i
proof -
have "i ∈ 𝒮"
using ‹dboost_star ⊆ 𝒮› that by blast
have [simp]: "real (hgt x - Suc 0) = real (hgt x) - 1" for x
using hgt_gt0 [of x] by linarith
have 36: "(1 - ε) * ((1 - beta i) / beta i) ≤ Δ i / alpha (hgt (pseq i))"
using R52 alpha_gt0 [OF hgt_gt0] beta_gt0 that ‹dboost_star ⊆ 𝒮› by (force simp: Δ_def divide_simps)
have k_big: "(1 + ε powr (1/2)) ≥ (1 + ε) powr (ε powr (-1/4))"
using big l_le_k by (auto simp: Big_ZZ_8_1_def Big_ZZ_8_2_def)
have *: "⋀x::real. x > 0 ⟹ (1 - x powr (1/2)) * (1 + x powr (1/2)) = 1 - x"
by (simp add: algebra_simps flip: powr_add)
have "?L = (1 - ε) * ((1 - beta i) / beta i) / (1 + ε powr (1/2))"
using beta_gt0 [OF ‹i ∈ 𝒮›] eps_gt0 k_big
by (force simp: oneminus_def divide_simps *)
also have "… ≤ Δ i / alpha (hgt (pseq i)) / (1 + ε powr (1/2))"
by (intro 36 divide_right_mono) auto
also have "… ≤ Δ i / alpha (hgt (pseq i)) / (1 + ε) powr (real (hgt (pseq (Suc i))) - hgt (pseq i))"
proof (intro divide_left_mono mult_pos_pos)
have "real (hgt (pseq (Suc i))) - hgt (pseq i) ≤ ε powr (-1/4)"
using that by (simp add: dboost_star_def)
then show "(1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i))) ≤ 1 + ε powr (1/2)"
using k_big by (smt (verit) eps_ge0 powr_mono)
show "0 ≤ Δ i / alpha (hgt (pseq i))"
by (simp add: Δ0 ΔΔ_ge0 ‹i ∈ 𝒮› alpha_ge0)
show "0 < (1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i)))"
using eps_gt0 by auto
qed (auto simp: add_strict_increasing)
also have "… ≤ Δ i / alpha (hgt (pseq (Suc i)))"
proof -
have "alpha (hgt (pseq (Suc i))) ≤ alpha (hgt (pseq i)) * (1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i)))"
using eps_gt0 hgt_gt0
by (simp add: alpha_eq divide_right_mono flip: powr_realpow powr_add)
moreover have "0 ≤ Δ i"
by (simp add: Δ0 ΔΔ_ge0 ‹i ∈ 𝒮›)
moreover have "0 < alpha (hgt (pseq (Suc i)))"
by (simp add: alpha_gt0 hgt_gt0 kn0)
ultimately show ?thesis
by (simp add: divide_left_mono)
qed
also have "… ≤ ?R"
unfolding 33 sum_divide_distrib
proof (intro sum_mono)
fix h
assume h: "h ∈ {1..maxh}"
show "ΔΔ i h / alpha (hgt (pseq (Suc i))) ≤ ΔΔ i h / alpha h"
proof (cases "hgt (pseq i) ≤ hgt (pseq (Suc i)) ∧ hgt (pseq (Suc i)) < h")
case False
then consider "hgt (pseq i) > hgt (pseq (Suc i))" | "hgt (pseq (Suc i)) ≥ h"
by linarith
then show ?thesis
proof cases
case 1
then show ?thesis
using R53 ‹i ∈ 𝒮› hgt_mono' kn0 by force
next
case 2
have "alpha h ≤ alpha (hgt (pseq (Suc i)))"
using "2" alpha_mono h by auto
moreover have "0 ≤ ΔΔ i h"
using ΔΔ_ge0 ‹i ∈ 𝒮› h by presburger
moreover have "0 < alpha h"
using h kn0 by (simp add: alpha_gt0 hgt_gt0)
ultimately show ?thesis
by (simp add: divide_left_mono)
qed
qed (auto simp: ΔΔ_eq_0)
qed
finally show ?thesis .
qed
have "oneminus * sum_SS = (∑i∈dboost_star. oneminus * ((1 - beta i) / beta i))"
using sum_distrib_left sum_SS_def by blast
also have "… ≤ (∑i∈dboost_star. ∑h=1..maxh. ΔΔ i h / alpha h)"
by (intro sum_mono 35)
also have "… = (∑h=1..maxh. ∑i∈dboost_star. ΔΔ i h / alpha h)"
using sum.swap by fastforce
also have "… ≤ (∑h=1..maxh. ∑i∈𝒮. ΔΔ i h / alpha h)"
by (intro sum_mono sum_mono2) (auto simp: ‹dboost_star ⊆ 𝒮› ΔΔ_ge0 alpha_ge0)
finally have 82: "oneminus * sum_SS
≤ (∑h=1..maxh. ∑i∈𝒮. ΔΔ i h / alpha h)" .
have Δalpha: "- 1 ≤ Δ i / alpha (hgt (pseq i))" if "i ∈ ℛ" for i
using Y_6_4_Red [of i] ‹i ∈ ℛ›
unfolding Δ_def ℛ_def
by (smt (verit, best) hgt_gt0 alpha_gt0 divide_minus_left less_divide_eq_1_pos)
have "(∑i∈ℛ. - (1 + ε)⇧2) ≤ (∑i∈ℛ. ∑h=1..maxh. ΔΔ i h / alpha h)"
proof (intro sum_mono)
fix i :: nat
assume "i ∈ ℛ"
show "- (1 + ε)⇧2 ≤ (∑h = 1..maxh. ΔΔ i h / alpha h)"
proof (cases "Δ i < 0")
case True
have "(1 + ε)⇧2 * -1 ≤ (1 + ε)⇧2 * (Δ i / alpha (hgt (pseq i)))"
using Δalpha
by (smt (verit, best) power2_less_0 ‹i ∈ ℛ› mult_le_cancel_left2 mult_minus_right)
also have "… ≤ (∑h = 1..maxh. ΔΔ i h / alpha h)"
proof -
have le0: "ΔΔ i h ≤ 0" for h
using True by (auto simp: ΔΔ_def Δ_def pp_eq)
have eq0: "ΔΔ i h = 0" if "1 ≤ h" "h < hgt (pseq i) - 2" for h
proof -
have "hgt (pseq i) - 2 ≤ hgt (pseq (Suc i))"
using Y_6_5_Red ‹16 ≤ k› ‹i ∈ ℛ› unfolding ℛ_def by blast
then show ?thesis
using that pp_less_hgt[of h] by (auto simp: ΔΔ_def pp_def)
qed
show ?thesis
unfolding 33 sum_distrib_left sum_divide_distrib
proof (intro sum_mono)
fix h :: nat
assume "h ∈ {1..maxh}"
then have "1 ≤ h" "h ≤ maxh" by auto
show "(1 + ε)⇧2 * (ΔΔ i h / alpha (hgt (pseq i))) ≤ ΔΔ i h / alpha h"
proof (cases "h < hgt (pseq i) - 2")
case True
then show ?thesis
using ‹1 ≤ h› eq0 by force
next
case False
have *: "(1 + ε) ^ (hgt (pseq i) - Suc 0) ≤ (1 + ε)⇧2 * (1 + ε) ^ (h - Suc 0)"
using False eps_ge0 unfolding power_add [symmetric]
by (intro power_increasing) auto
have **: "(1 + ε)⇧2 * alpha h ≥ alpha (hgt (pseq i))"
using ‹1 ≤ h› mult_left_mono [OF *, of "ε"] eps_ge0
by (simp add: alpha_eq hgt_gt0 mult_ac divide_right_mono)
show ?thesis
using le0 alpha_gt0 ‹h≥1› hgt_gt0 mult_left_mono_neg [OF **, of "ΔΔ i h"]
by (simp add: divide_simps mult_ac)
qed
qed
qed
finally show ?thesis
by linarith
next
case False
then have "ΔΔ i h ≥ 0" for h
using ΔΔ_def Δ_def pp_eq by auto
then have "(∑h = 1..maxh. ΔΔ i h / alpha h) ≥ 0"
by (simp add: alpha_ge0 sum_nonneg)
then show ?thesis
by (smt (verit, ccfv_SIG) sum_power2_ge_zero)
qed
qed
then have 83: "- (1 + ε)⇧2 * card ℛ ≤ (∑h=1..maxh. ∑i∈ℛ. ΔΔ i h / alpha h)"
by (simp add: mult.commute sum.swap [of _ ℛ])
have Δ0: "Δ i ≥ 0" if "i ∈ 𝒟" for i
using Y_6_4_DegreeReg that unfolding 𝒟_def Δ_def by auto
have 39: "-2 * ε powr(-1/2) ≤ (∑h = 1..maxh. (ΔΔ (i-1) h + ΔΔ i h) / alpha h)" (is "?L ≤ ?R")
if "i ∈ ℬ" for i
proof -
have "odd i"
using step_odd that by (force simp: Step_class_insert_NO_MATCH ℬ_def)
then have "i>0"
using odd_pos by auto
show ?thesis
proof (cases "Δ (i-1) + Δ i ≥ 0")
case True
with ‹i>0› have "ΔΔ (i-1) h + ΔΔ i h ≥ 0" if "h≥1" for h
by (fastforce simp: ΔΔ_def Δ_def pp_eq)
then have "(∑h = 1..maxh. (ΔΔ (i-1) h + ΔΔ i h) / alpha h) ≥ 0"
by (force simp: alpha_ge0 intro: sum_nonneg)
then show ?thesis
by (smt (verit, ccfv_SIG) powr_ge_zero)
next
case False
then have ΔΔ_le0: "ΔΔ (i-1) h + ΔΔ i h ≤ 0" if "h≥1" for h
by (smt (verit, best) One_nat_def ΔΔ_def Δ_def ‹odd i› odd_Suc_minus_one pp_eq)
have hge: "hgt (pseq (Suc i)) ≥ hgt (pseq (i-1)) - 2 * ε powr (-1/2)"
using bigY65B that Y_6_5_Bblue by (fastforce simp: ℬ_def)
have ΔΔ0: "ΔΔ (i-1) h + ΔΔ i h = 0" if "0<h" "h < hgt (pseq (i-1)) - 2 * ε powr (-1/2)" for h
using ‹odd i› that hge unfolding ΔΔ_def One_nat_def
by (smt (verit) of_nat_less_iff odd_Suc_minus_one powr_non_neg pp_less_hgt)
have big39: "1/2 ≤ (1 + ε) powr (-2 * ε powr (-1/2))"
using big l_le_k by (auto simp: Big_ZZ_8_1_def Big39_def)
have "?L * alpha (hgt (pseq (i-1))) * (1 + ε) powr (-2 * ε powr (-1/2))
≤ - (ε powr (-1/2)) * alpha (hgt (pseq (i-1)))"
using mult_left_mono_neg [OF big39, of "- (ε powr (-1/2)) * alpha (hgt (pseq (i-1))) / 2"]
using alpha_ge0 [of "hgt (pseq (i-1))"] eps_ge0
by (simp add: mult_ac)
also have "… ≤ Δ (i-1) + Δ i"
proof -
have "pseq (Suc i) ≥ pseq (i-1) - (ε powr (-1/2)) * alpha (hgt (pseq (i-1)))"
using Y_6_4_Bblue that ℬ_def by blast
with ‹i>0› show ?thesis
by (simp add: Δ_def)
qed
finally have "?L * alpha (hgt (pseq (i-1))) * (1 + ε) powr (-2 * ε powr (-1/2)) ≤ Δ (i-1) + Δ i" .
then have "?L ≤ (1 + ε) powr (2 * ε powr (-1/2)) * (Δ (i-1) + Δ i) / alpha (hgt (pseq (i-1)))"
using alpha_ge0 [of "hgt (pseq (i-1))"] eps_ge0
by (simp add: powr_minus divide_simps mult_ac)
also have "… ≤ ?R"
proof -
have "(1 + ε) powr (2 * ε powr(-1/2)) * (ΔΔ (i - Suc 0) h + ΔΔ i h) / alpha (hgt (pseq (i - Suc 0)))
≤ (ΔΔ (i - Suc 0) h + ΔΔ i h) / alpha h"
if h: "Suc 0 ≤ h" "h ≤ maxh" for h
proof (cases "h < hgt (pseq (i-1)) - 2 * ε powr(-1/2)")
case False
then have "hgt (pseq (i-1)) - 1 ≤ 2 * ε powr(-1/2) + (h - 1)"
using hgt_gt0 by (simp add: nat_less_real_le)
then have *: "(1 + ε) powr (2 * ε powr(-1/2)) / alpha (hgt (pseq (i-1))) ≥ 1 / alpha h"
using that eps_gt0 kn0 hgt_gt0
by (simp add: alpha_eq divide_simps flip: powr_realpow powr_add)
show ?thesis
using mult_left_mono_neg [OF * ΔΔ_le0] that by (simp add: Groups.mult_ac)
qed (use h ΔΔ0 in auto)
then show ?thesis
by (force simp: 33 sum_distrib_left sum_divide_distrib simp flip: sum.distrib intro: sum_mono)
qed
finally show ?thesis .
qed
qed
have B34: "card ℬ ≤ k powr (3/4)"
by (smt (verit) cardℬ l_le_k of_nat_0_le_iff of_nat_mono powr_mono2 zero_le_divide_iff)
have "-2 * k powr (7/8) ≤ -2 * ε powr(-1/2) * k powr (3/4)"
by (simp add: eps_def powr_powr flip: powr_add)
also have "… ≤ -2 * ε powr(-1/2) * card ℬ"
using B34 by (intro mult_left_mono_neg powr_mono2) auto
also have "… = (∑i∈ℬ. -2 * ε powr(-1/2))"
by simp
also have "… ≤ (∑h = 1..maxh. ∑i∈ℬ. (ΔΔ (i-1) h + ΔΔ i h) / alpha h)"
unfolding sum.swap [of _ ℬ] by (intro sum_mono 39)
also have "… ≤ (∑h=1..maxh. ∑i∈ℬ∪𝒟. ΔΔ i h / alpha h)"
proof (intro sum_mono)
fix h
assume "h ∈ {1..maxh}"
have "ℬ ⊆ {0<..}"
using odd_pos [OF step_odd] by (auto simp: ℬ_def Step_class_insert_NO_MATCH)
with inj_on_diff_nat [of ℬ 1] have inj_pred: "inj_on (λi. i - Suc 0) ℬ"
by (simp add: Suc_leI subset_eq)
have "(∑i∈ℬ. ΔΔ (i - Suc 0) h) = (∑i ∈ (λi. i-1) ` ℬ. ΔΔ i h)"
by (simp add: sum.reindex [OF inj_pred])
also have "… ≤ (∑i∈𝒟. ΔΔ i h)"
proof (intro sum_mono2)
show "(λi. i - 1) ` ℬ ⊆ 𝒟"
by (force simp: 𝒟_def ℬ_def Step_class_insert_NO_MATCH intro: dreg_before_step')
show "0 ≤ ΔΔ i h" if "i ∈ 𝒟 ∖ (λi. i - 1) ` ℬ" for i
using that Δ0 ΔΔ_def Δ_def pp_eq by fastforce
qed auto
finally have "(∑i∈ℬ. ΔΔ (i - Suc 0) h) ≤ (∑i∈𝒟. ΔΔ i h)" .
with alpha_ge0 [of h]
show "(∑i∈ℬ. (ΔΔ (i - 1) h + ΔΔ i h) / alpha h) ≤ (∑i ∈ ℬ∪𝒟. ΔΔ i h / alpha h)"
by (simp add: BD_disj divide_right_mono sum.distrib sum.union_disjoint flip: sum_divide_distrib)
qed
finally have 84: "-2 * k powr (7/8) ≤ (∑h=1..maxh. ∑i∈ℬ∪𝒟. ΔΔ i h / alpha h)" .
have m_eq: "{..<halted_point} = ℛ ∪ 𝒮 ∪ (ℬ ∪ 𝒟)"
using before_halted_eq by (auto simp: ℬ_def 𝒟_def 𝒮_def ℛ_def Step_class_insert_NO_MATCH)
have "- (1 + ε)⇧2 * real (card ℛ)
+ oneminus * sum_SS
- 2 * real k powr (7/8) ≤ (∑h = Suc 0..maxh. ∑i∈ℛ. ΔΔ i h / alpha h)
+ (∑h = Suc 0..maxh. ∑i∈𝒮. ΔΔ i h / alpha h)
+ (∑h = Suc 0..maxh. ∑i ∈ ℬ ∪ 𝒟. ΔΔ i h / alpha h) "
using 82 83 84 by simp
also have "… = (∑h = Suc 0..maxh. ∑i ∈ ℛ ∪ 𝒮 ∪ (ℬ ∪ 𝒟). ΔΔ i h / alpha h)"
by (simp add: sum.distrib disj sum.union_disjoint Int_Un_distrib Int_Un_distrib2)
also have "… ≤ 1 + 2 * ln (real k) / ε"
using 34 by (simp add: m_eq)
finally
have 41: "oneminus * sum_SS - (1 + ε)⇧2 * card ℛ - 2 * k powr (7/8)
≤ 1 + 2 * ln k / ε"
by simp
have big42: "(1 + ε)⇧2 / oneminus ≤ 1 + 2 * k powr (-1/16)"
"2 * k powr (-1/16) * k
+ (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus
≤ real k powr (19/20)"
using big l_le_k by (auto simp: Big_ZZ_8_1_def Big42a_def Big42b_def oneminus_def)
have "oneminus > 0"
using ‹16 ≤ k› eps_gt0 eps_less1 powr01_less_one by (auto simp: oneminus_def)
with 41 have "sum_SS
≤ (1 + 2 * ln k / ε + (1 + ε)⇧2 * card ℛ + 2 * k powr (7/8)) / oneminus"
by (simp add: mult_ac pos_le_divide_eq diff_le_eq)
also have "… ≤ card ℛ * (((1 + ε)⇧2) / oneminus)
+ (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
by (simp add: field_simps add_divide_distrib)
also have "… ≤ card ℛ * (1 + 2 * k powr (-1/16))
+ (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
using big42 ‹oneminus > 0› by (intro add_mono mult_mono) auto
also have "… ≤ card ℛ + 2 * k powr (-1/16) * k
+ (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
using ‹card ℛ < k› by (intro add_mono mult_mono) (auto simp: algebra_simps)
also have "… ≤ real (card ℛ) + real k powr (19/20)"
using big42 by force
finally show ?thesis .
qed
subsection ‹Lemma 8.5›
text ‹An inequality that pops up in the proof of (39)›
definition "inequality85 ≡ λk. 3 * eps k powr (1/4) * k ≤ k powr (19/20)"
definition "Big_ZZ_8_5 ≡
λμ l. Big_X_7_5 μ l ∧ Big_ZZ_8_1 μ l ∧ Big_Red_5_3 μ l
∧ (∀k≥l. inequality85 k)"
lemma Big_ZZ_8_5:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_5 μ l"
using assms Big_Red_5_3 Big_X_7_5 Big_ZZ_8_1
unfolding Big_ZZ_8_5_def inequality85_def eps_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_ge_at_top; real_asymp)
done
lemma (in Book) ZZ_8_5:
assumes big: "Big_ZZ_8_5 μ l"
defines "ℛ ≡ Step_class {red_step}" and "𝒮 ≡ Step_class {dboost_step}"
shows "card 𝒮 ≤ (bigbeta / (1 - bigbeta)) * card ℛ
+ (2 / (1-μ)) * k powr (19/20)"
proof -
have [simp]: "finite 𝒮"
by (simp add: 𝒮_def)
moreover have "dboost_star ⊆ 𝒮"
by (auto simp: dboost_star_def 𝒮_def)
ultimately have "real (card 𝒮) - real (card dboost_star) = card (𝒮∖dboost_star)"
by (metis card_Diff_subset card_mono finite_subset of_nat_diff)
also have "… ≤ 3 * ε powr (1/4) * k"
using μ01 big X_7_5 by (auto simp: Big_ZZ_8_5_def dboost_star_def 𝒮_def)
also have "… ≤ k powr (19/20)"
using big l_le_k by (auto simp: Big_ZZ_8_5_def inequality85_def)
finally have *: "real (card 𝒮) - card dboost_star ≤ k powr (19/20)" .
have bigbeta_lt1: "bigbeta < 1" and bigbeta_gt0: "0 < bigbeta" and beta_gt0: "⋀i. i ∈ 𝒮 ⟹ beta i > 0"
using bigbeta_ge0 big by (auto simp: Big_ZZ_8_5_def 𝒮_def beta_gt0 bigbeta_gt0 bigbeta_less1)
then have ge0: "bigbeta / (1 - bigbeta) ≥ 0"
by auto
show ?thesis
proof (cases "dboost_star = {}")
case True
with * have "card 𝒮 ≤ k powr (19/20)"
by simp
also have "… ≤ (2 / (1-μ)) * k powr (19/20)"
using μ01 kn0 by (simp add: divide_simps)
finally show ?thesis
by (smt (verit, ccfv_SIG) mult_nonneg_nonneg of_nat_0_le_iff ge0)
next
case False
have bb_le: "bigbeta ≤ μ"
using big bigbeta_le by (auto simp: Big_ZZ_8_5_def)
have "(card 𝒮 - k powr (19/20)) / bigbeta ≤ card dboost_star / bigbeta"
by (smt (verit) "*" bigbeta_ge0 divide_right_mono)
also have "… = (∑i∈dboost_star. 1 / beta i)"
proof (cases "card dboost_star = 0")
case False
then show ?thesis
by (simp add: bigbeta_def Let_def inverse_eq_divide)
qed (simp add: False card_eq_0_iff)
also have "… ≤ real(card dboost_star) + card ℛ + k powr (19/20)"
proof -
have "(∑i∈dboost_star. (1 - beta i) / beta i)
≤ real (card ℛ) + k powr (19/20)"
using ZZ_8_1 big unfolding Big_ZZ_8_5_def ℛ_def by blast
moreover have "(∑i∈dboost_star. beta i / beta i) = (∑i∈dboost_star. 1)"
using ‹dboost_star ⊆ 𝒮› beta_gt0 by (intro sum.cong) force+
ultimately show ?thesis
by (simp add: field_simps diff_divide_distrib sum_subtractf)
qed
also have "… ≤ real(card 𝒮) + card ℛ + k powr (19/20)"
by (simp add: ‹dboost_star ⊆ 𝒮› card_mono)
finally have "(card 𝒮 - k powr (19/20)) / bigbeta ≤ real (card 𝒮) + card ℛ + k powr (19/20)" .
then have "card 𝒮 - k powr (19/20) ≤ (real (card 𝒮) + card ℛ + k powr (19/20)) * bigbeta"
using bigbeta_gt0 by (simp add: field_simps)
then have "card 𝒮 * (1 - bigbeta) ≤ bigbeta * card ℛ + (1 + bigbeta) * k powr (19/20)"
by (simp add: algebra_simps)
then have "card 𝒮 ≤ (bigbeta * card ℛ + (1 + bigbeta) * k powr (19/20)) / (1 - bigbeta)"
using bigbeta_lt1 by (simp add: field_simps)
also have "… = (bigbeta / (1 - bigbeta)) * card ℛ
+ ((1 + bigbeta) / (1 - bigbeta)) * k powr (19/20)"
using bigbeta_gt0 bigbeta_lt1 by (simp add: divide_simps)
also have "… ≤ (bigbeta / (1 - bigbeta)) * card ℛ + (2 / (1-μ)) * k powr (19/20)"
using μ01 bb_le by (intro add_mono order_refl mult_right_mono frac_le) auto
finally show ?thesis .
qed
qed
subsection ‹Lemma 8.6›
text ‹For some reason this was harder than it should have been.
It does require a further small limit argument.›
definition "Big_ZZ_8_6 ≡
λμ l. Big_ZZ_8_5 μ l ∧ (∀k≥l. 2 / (1-μ) * k powr (19/20) < k powr (39/40))"
lemma Big_ZZ_8_6:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_6 μ l"
using assms Big_ZZ_8_5
unfolding Big_ZZ_8_6_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_ge_at_top eventually_all_geI1 [where L=1])
apply real_asymp
by (smt (verit, ccfv_SIG) frac_le powr_ge_zero)
lemma (in Book) ZZ_8_6:
assumes big: "Big_ZZ_8_6 μ l"
defines "ℛ ≡ Step_class {red_step}" and "𝒮 ≡ Step_class {dboost_step}"
and "a ≡ 2 / (1-μ)"
assumes s_ge: "card 𝒮 ≥ k powr (39/40)"
shows "bigbeta ≥ (1 - a * k powr (-1/40)) * (card 𝒮 / (card 𝒮 + card ℛ))"
proof -
have bigbeta_lt1: "bigbeta < 1" and bigbeta_gt0: "0 < bigbeta"
using bigbeta_ge0 big
by (auto simp: Big_ZZ_8_6_def Big_ZZ_8_5_def bigbeta_less1 bigbeta_gt0 𝒮_def)
have "a > 0"
using μ01 by (simp add: a_def)
have s_gt_a: "a * k powr (19/20) < card 𝒮"
and 85: "card 𝒮 ≤ (bigbeta / (1 - bigbeta)) * card ℛ + a * k powr (19/20)"
using big l_le_k assms
unfolding ℛ_def 𝒮_def a_def Big_ZZ_8_6_def by (fastforce intro: ZZ_8_5)+
then have t_non0: "card ℛ ≠ 0"
using mult_eq_0_iff by fastforce
then have "(card 𝒮 - a * k powr (19/20)) / card ℛ ≤ bigbeta / (1 - bigbeta)"
using 85 bigbeta_gt0 bigbeta_lt1 t_non0 by (simp add: pos_divide_le_eq)
then have "bigbeta ≥ (1 - bigbeta) * (card 𝒮 - a * k powr (19/20)) / card ℛ"
by (smt (verit, ccfv_threshold) bigbeta_lt1 mult.commute le_divide_eq times_divide_eq_left)
then have *: "bigbeta * (card ℛ + card 𝒮 - a * k powr (19/20)) ≥ card 𝒮 - a * k powr (19/20)"
using t_non0 by (simp add: field_simps)
have "(1 - a * k powr - (1/40)) * card 𝒮 ≤ card 𝒮 - a * k powr (19/20)"
using s_ge kn0 ‹a>0› t_non0 by (simp add: powr_minus field_simps flip: powr_add)
then have "(1 - a * k powr (-1/40)) * (card 𝒮 / (card 𝒮 + card ℛ))
≤ (card 𝒮 - a * k powr (19/20)) / (card 𝒮 + card ℛ)"
by (force simp: divide_right_mono)
also have "… ≤ (card 𝒮 - a * k powr (19/20)) / (card ℛ + card 𝒮 - a * k powr (19/20))"
using s_gt_a ‹a>0› t_non0 by (intro divide_left_mono) auto
also have "… ≤ bigbeta"
using * s_gt_a
by (simp add: divide_simps split: if_split_asm)
finally show ?thesis .
qed
end