Theory Bounding_X
section ‹Bounding the Size of @{term X}›
theory Bounding_X imports Bounding_Y
begin
subsection ‹Preliminaries›
lemma sum_odds_even:
fixes f :: "nat ⇒ 'a :: ab_group_add"
assumes "even m"
shows "(∑i ∈ {i. i<m ∧ odd i}. f (Suc i) - f (i -Suc 0)) = f m - f 0"
using assms
proof (induction m rule: less_induct)
case (less m)
show ?case
proof (cases "m<2")
case True
with ‹even m› show ?thesis
by fastforce
next
case False
have eq: "{i. i<m ∧ odd i} = insert (m-1) {i. i<m-2 ∧ odd i}"
proof
show "{i. i < m ∧ odd i} ⊆ insert (m - 1) {i. i < m - 2 ∧ odd i}"
using ‹even m› by clarify presburger
qed (use False less in auto)
have [simp]: "¬ (m - Suc 0 < m - 2)"
by linarith
show ?thesis
using False by (simp add: eq less flip: numeral_2_eq_2)
qed
qed
lemma sum_odds_odd:
fixes f :: "nat ⇒ 'a :: ab_group_add"
assumes "odd m"
shows "(∑i ∈ {i. i<m ∧ odd i}. f (Suc i) - f (i - Suc 0)) = f (m-1) - f 0"
proof -
have eq: "{i. i<m ∧ odd i} = {i. i<m-1 ∧ odd i}"
using assms not_less_iff_gr_or_eq by fastforce
show ?thesis
by (simp add: sum_odds_even eq assms)
qed
context Book
begin
text ‹the set of moderate density-boost steps (page 20)›
definition dboost_star where
"dboost_star ≡ {i ∈ Step_class {dboost_step}. real (hgt (pseq (Suc i))) - hgt (pseq i) ≤ ε powr (-1/4)}"
definition bigbeta where
"bigbeta ≡ let S = dboost_star in if S = {} then μ else (card S) * inverse (∑i∈S. inverse (beta i))"
lemma dboost_star_subset: "dboost_star ⊆ Step_class {dboost_step}"
by (auto simp: dboost_star_def)
lemma finite_dboost_star: "finite (dboost_star)"
by (meson dboost_step_finite dboost_star_subset finite_subset)
lemma bigbeta_ge0: "bigbeta ≥ 0"
using μ01 by (simp add: bigbeta_def Let_def beta_ge0 sum_nonneg)
lemma bigbeta_ge_square:
assumes big: "Big_Red_5_3 μ l"
shows "bigbeta ≥ 1 / (real k)^2"
proof -
have k: "1 / (real k)⇧2 ≤ μ"
using big kn0 l_le_k by (auto simp: Big_Red_5_3_def)
have fin: "finite (dboost_star)"
using assms finite_dboost_star by blast
have R53: "∀i ∈ Step_class {dboost_step}. 1 / (real k)^2 ≤ beta i"
using Red_5_3 assms by blast
show "1 / (real k)^2 ≤ bigbeta"
proof (cases "dboost_star = {}")
case True
then show ?thesis
using assms k by (simp add: bigbeta_def)
next
case False
then have card_gt0: "card (dboost_star) > 0"
by (meson card_gt_0_iff dboost_star_subset fin finite_subset)
moreover have *: "∀i ∈ dboost_star. beta i > 0 ∧ (real k)^2 ≥ inverse (beta i)"
using R53 kn0 assms by (simp add: beta_gt0 field_simps dboost_star_def)
ultimately have "(∑i∈dboost_star. inverse (beta i)) ≤ card (dboost_star) * (real k)^2"
by (simp add: sum_bounded_above)
moreover have "(∑i∈dboost_star. inverse (beta i)) ≠ 0"
by (metis * False fin inverse_positive_iff_positive less_irrefl sum_pos)
ultimately show ?thesis
using False card_gt0 k bigbeta_ge0
by (simp add: bigbeta_def Let_def divide_simps split: if_split_asm)
qed
qed
lemma bigbeta_gt0:
assumes big: "Big_Red_5_3 μ l"
shows "bigbeta > 0"
by (smt (verit) kn0 assms bigbeta_ge_square of_nat_zero_less_power_iff zero_less_divide_iff)
lemma bigbeta_less1:
assumes big: "Big_Red_5_3 μ l"
shows "bigbeta < 1"
proof -
have *: "∀i∈Step_class {dboost_step}. 0 < beta i"
using assms beta_gt0 big by blast
have fin: "finite (Step_class {dboost_step})"
using dboost_step_finite assms by blast
show "bigbeta < 1"
proof (cases "dboost_star = {}")
case True
then show ?thesis
using assms μ01 by (simp add: bigbeta_def)
next
case False
then have gt0: "card (dboost_star) > 0"
by (meson card_gt_0_iff dboost_star_subset fin finite_subset)
have "real (card (dboost_star)) = (∑i∈dboost_star. 1)"
by simp
also have "… < (∑i∈dboost_star. 1 / beta i)"
proof (intro sum_strict_mono)
show "finite (dboost_star)"
using card_gt_0_iff gt0 by blast
fix i
assume "i ∈ dboost_star"
with assms μ01 "*" dboost_star_subset beta_le
show "1 < 1 / beta i"
by (force simp: Step_class_insert_NO_MATCH)
qed (use False in auto)
finally show ?thesis
using False by (simp add: bigbeta_def Let_def divide_simps)
qed
qed
lemma bigbeta_le:
assumes big: "Big_Red_5_3 μ l"
shows "bigbeta ≤ μ"
proof -
have "real (card (dboost_star)) = (∑i∈dboost_star. 1)"
by simp
also have "… ≤ (∑i∈dboost_star. μ / beta i)"
proof (intro sum_mono)
fix i
assume i: "i ∈ dboost_star"
with beta_le dboost_star_subset have "beta i ≤ μ"
by (auto simp: Step_class_insert_NO_MATCH)
with beta_gt0 assms show "1 ≤ μ / beta i"
by (smt (verit) dboost_star_subset divide_less_eq_1_pos i subset_iff)
qed
also have "… = μ * (∑i∈dboost_star. 1 / beta i)"
by (simp add: sum_distrib_left)
finally have "real (card (dboost_star)) ≤ μ * (∑i∈dboost_star. 1 / beta i)" .
moreover have "(∑i∈dboost_star. 1 / beta i) ≥ 0"
by (simp add: beta_ge0 sum_nonneg)
ultimately show ?thesis
using μ01 by (simp add: bigbeta_def Let_def divide_simps)
qed
end
subsection ‹Lemma 7.2›
definition "Big_X_7_2 ≡ λμ l. nat ⌈real l powr (3/4)⌉ ≥ 3 ∧ l > 1 / (1-μ)"
text ‹establishing the size requirements for 7.11›
lemma Big_X_7_2:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_2 μ l"
unfolding Big_X_7_2_def eventually_conj_iff all_imp_conj_distrib eps_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_geI1[where L=1] eventually_all_ge_at_top)
apply real_asymp+
by (smt (verit, best) ‹μ1<1› frac_le)
definition "ok_fun_72 ≡ λμ k. (real k / ln 2) * ln (1 - 1 / (k * (1-μ)))"
lemma ok_fun_72:
assumes "μ<1"
shows "ok_fun_72 μ ∈ o(real)"
using assms unfolding ok_fun_72_def by real_asymp
lemma ok_fun_72_uniform:
assumes "0<μ0" "μ1<1"
assumes "e>0"
shows "∀⇧∞k. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ ¦ok_fun_72 μ k¦ / k ≤ e"
proof (intro eventually_all_geI1 [where L = "Suc(nat⌈1/(1-μ1)⌉)"])
show "∀⇧∞k. ¦ok_fun_72 μ1 k¦ / real k ≤ e"
using assms unfolding ok_fun_72_def by real_asymp
next
fix k μ
assume le_e: "¦ok_fun_72 μ1 k¦ / real k ≤ e"
and μ: "μ0 ≤ μ" "μ ≤ μ1"
and k: "Suc(nat⌈1/(1-μ1)⌉) ≤ k"
with assms have "1 > 1 / (real k * (1 - μ1))"
by (smt (verit, best) divide_less_eq divide_less_eq_1 less_eq_Suc_le natceiling_lessD)
then have *: "1 > 1 / (real k * (1 - r))" if "r≤μ1" for r
using that assms k less_le_trans by fastforce
have †: "1 / (k * (1 - μ)) ≤ 1 / (k * (1 - μ1))"
using μ assms by (simp add: divide_simps mult_less_0_iff)
obtain "μ<1" "k>0" using μ k assms by force
then have "¦ok_fun_72 μ k¦ ≤ ¦ok_fun_72 μ1 k¦"
using μ * assms †
by (simp add: ok_fun_72_def abs_mult zero_less_mult_iff abs_of_neg divide_le_cancel)
then show "¦ok_fun_72 μ k¦ / real k ≤ e"
by (smt (verit, best) le_e divide_right_mono of_nat_0_le_iff)
qed
lemma (in Book) X_7_2:
defines "ℛ ≡ Step_class {red_step}"
assumes big: "Big_X_7_2 μ l"
shows "(∏i∈ℛ. card (Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr (ok_fun_72 μ k) * (1-μ) ^ card ℛ"
proof -
define R where "R ≡ RN k (nat ⌈real l powr (3/4)⌉)"
have l34_ge3: "nat ⌈real l powr (3/4)⌉ ≥ 3" and k_gt: "k > 1 / (1-μ)"
using big l_le_k by (auto simp: Big_X_7_2_def)
then obtain "R > k" "k ≥ 2"
using μ01 RN_gt1 R_def l_le_k
by (smt (verit, best) divide_le_eq_1_pos fact_2 nat_le_real_less of_nat_fact)
with k_gt μ01 have bigR: "1-μ > 1/R"
by (smt (verit, best) less_imp_of_nat_less ln_div ln_le_cancel_iff zero_less_divide_iff)
have *: "1-μ - 1/R ≤ card (Xseq (Suc i)) / card (Xseq i)"
if "i ∈ ℛ" for i
proof -
let ?NRX = "λi. Neighbours Red (cvx i) ∩ Xseq i"
have nextX: "Xseq (Suc i) = ?NRX i" and nont: "¬ termination_condition (Xseq i) (Yseq i)"
using that by (auto simp: ℛ_def step_kind_defs next_state_def split: prod.split)
then have cardX: "card (Xseq i) > R"
unfolding R_def by (meson not_less termination_condition_def)
have 1: "card (?NRX i) ≥ (1-μ) * card (Xseq i) - 1"
using that card_cvx_Neighbours μ01 by (simp add: ℛ_def Step_class_def)
have "R ≠ 0"
using ‹k < R› by linarith
with cardX have "(1-μ) - 1 / R ≤ (1-μ) - 1 / card (Xseq i)"
by (simp add: inverse_of_nat_le)
also have "… ≤ card (Xseq (Suc i)) / card (Xseq i)"
using cardX nextX 1 by (simp add: divide_simps)
finally show ?thesis .
qed
have fin_red: "finite ℛ"
using red_step_finite by (auto simp: ℛ_def)
define t where "t ≡ card ℛ"
have "t≥0"
by (auto simp: t_def)
have "(1-μ - 1/R) ^ card Red_steps ≤ (∏i ∈ Red_steps. card (Xseq(Suc i)) / card (Xseq i))"
if "Red_steps ⊆ ℛ" for Red_steps
using finite_subset [OF that fin_red] that
proof induction
case empty
then show ?case
by auto
next
case (insert i Red_steps)
then have i: "i ∈ ℛ"
by auto
have "((1-μ) - 1/R) ^ card (insert i Red_steps) = ((1-μ) - 1/R) * ((1-μ) - 1/R) ^ card (Red_steps)"
by (simp add: insert)
also have "… ≤ (card (Xseq (Suc i)) / card (Xseq i)) * ((1-μ) - 1/R) ^ card (Red_steps)"
using bigR by (intro mult_right_mono * i) auto
also have "… ≤ (card (Xseq (Suc i)) / card (Xseq i)) * (∏i ∈ Red_steps. card (Xseq(Suc i)) / card (Xseq i))"
using insert by (intro mult_left_mono) auto
also have "… = (∏i∈insert i Red_steps. card (Xseq(Suc i)) / card (Xseq i))"
using insert by simp
finally show ?case .
qed
then have *: "(1-μ - 1/R) ^ t ≤ (∏i ∈ ℛ. card (Xseq(Suc i)) / card (Xseq i))"
using t_def by blast
have "1-μ - 1/k ≤ 1-μ - 1/R"
using kn0 ‹k < R› by (simp add: inverse_of_nat_le)
then have ln_le: "ln (1-μ - 1/k) ≤ ln (1-μ - 1/R)"
using μ01 k_gt ‹R>k› by (simp add: bigR divide_simps mult.commute less_le_trans)
have "ok_fun_72 μ k * ln 2 = k * ln (1 - 1 / (k * (1-μ)))"
by (simp add: ok_fun_72_def)
also have "… ≤ t * ln (1 - 1 / (k * (1-μ)))"
proof (intro mult_right_mono_neg)
have red_steps: "card ℛ < k"
using red_step_limit ‹0<μ› by (auto simp: ℛ_def)
show "real t ≤ real k"
using nat_less_le red_steps by (simp add: t_def)
show "ln (1 - 1 / (k * (1-μ))) ≤ 0"
using μ01 divide_less_eq k_gt ln_one_minus_pos_upper_bound by fastforce
qed
also have "… = t * ln ((1-μ - 1/k) / (1-μ))"
using ‹t≥0› μ01 by (simp add: diff_divide_distrib)
also have "… = t * (ln (1-μ - 1/k) - ln (1-μ))"
using ‹t≥0› μ01 k_gt kn0 ln_div by force
also have "… ≤ t * (ln (1-μ - 1/R) - ln (1-μ))"
by (simp add: ln_le mult_left_mono)
finally have "ok_fun_72 μ k * ln 2 + t * ln (1-μ) ≤ t * ln (1-μ - 1/R)"
by (simp add: ring_distribs)
then have "2 powr ok_fun_72 μ k * (1-μ) ^ t ≤ (1-μ - 1/R) ^ t"
using μ01 by (simp add: bigR ln_mult ln_powr ln_realpow flip: ln_le_cancel_iff)
with * show ?thesis
by (simp add: t_def)
qed
subsection ‹Lemma 7.3›
context Book
begin
definition "Bdelta ≡ λ μ i. Bseq (Suc i) ∖ Bseq i"
lemma card_Bdelta: "card (Bdelta μ i) = card (Bseq (Suc i)) - card (Bseq i)"
by (simp add: Bseq_mono Bdelta_def card_Diff_subset finite_Bseq)
lemma card_Bseq_mono: "card (Bseq (Suc i)) ≥ card (Bseq i)"
by (simp add: Bseq_Suc_subset card_mono finite_Bseq)
lemma card_Bseq_sum: "card (Bseq i) = (∑j<i. card (Bdelta μ j))"
proof (induction i)
case 0
then show ?case
by auto
next
case (Suc i)
with card_Bseq_mono show ?case
unfolding card_Bdelta sum.lessThan_Suc
by (smt (verit, del_insts) Nat.add_diff_assoc diff_add_inverse)
qed
definition "get_blue_book ≡ λi. let (X,Y,A,B) = stepper i in choose_blue_book (X,Y,A,B)"
text ‹Tracking changes to X and B. The sets are necessarily finite›
lemma Bdelta_bblue_step:
assumes "i ∈ Step_class {bblue_step}"
shows "∃S ⊆ Xseq i. Bdelta μ i = S
∧ card (Xseq (Suc i)) ≥ (μ ^ card S) * card (Xseq i) / 2"
proof -
obtain X Y A B S T where step: "stepper i = (X,Y,A,B)" and bb: "get_blue_book i = (S,T)"
and valid: "valid_state(X,Y,A,B)"
by (metis surj_pair valid_state_stepper)
moreover have "finite X"
by (metis V_state_stepper finX step)
ultimately have *: "stepper (Suc i) = (T, Y, A, B∪S) ∧ good_blue_book X (S,T)"
and Xeq: "X = Xseq i"
using assms choose_blue_book_works [of X S T Y A B]
by (simp_all add: step_kind_defs next_state_def valid_state_def get_blue_book_def choose_blue_book_works split: if_split_asm)
show ?thesis
proof (intro exI conjI)
have "S ⊆ X"
proof (intro choose_blue_book_subset [THEN conjunct1] ‹finite X›)
show "(S, T) = choose_blue_book (X, Y, A, B)"
using bb step by (simp add: get_blue_book_def Xseq_def)
qed
then show "S ⊆ Xseq i"
using Xeq by force
have "disjnt X B"
using valid by (auto simp: valid_state_def disjoint_state_def)
then show "Bdelta μ i = S"
using * step ‹S ⊆ X› by (auto simp: Bdelta_def Bseq_def disjnt_iff)
show "μ ^ card S * real (card (Xseq i)) / 2 ≤ real (card (Xseq (Suc i)))"
using * by (auto simp: Xseq_def good_blue_book_def step)
qed
qed
lemma Bdelta_dboost_step:
assumes "i ∈ Step_class {dboost_step}"
shows "∃x ∈ Xseq i. Bdelta μ i = {x}"
proof -
obtain X Y A B where step: "stepper i = (X,Y,A,B)" and valid: "valid_state(X,Y,A,B)"
by (metis surj_pair valid_state_stepper)
have cvx: "choose_central_vx (X,Y,A,B) ∈ X"
by (metis Step_class_insert Un_iff cvx_def cvx_in_Xseq assms step stepper_XYseq)
then have "∃X' Y'. stepper (Suc i) = (X', Y', A, insert (choose_central_vx (X,Y,A,B)) B)"
using assms step
by (auto simp: step_kind_defs next_state_def split: if_split_asm)
moreover have "choose_central_vx (X,Y,A,B) ∉ B"
using valid cvx by (force simp: valid_state_def disjoint_state_def disjnt_iff)
ultimately show ?thesis
using step cvx by (auto simp: Bdelta_def Bseq_def disjnt_iff Xseq_def)
qed
lemma card_Bdelta_dboost_step:
assumes "i ∈ Step_class {dboost_step}"
shows "card (Bdelta μ i) = 1"
using Bdelta_dboost_step [OF assms] by force
lemma Bdelta_trivial_step:
assumes i: "i ∈ Step_class {red_step,dreg_step,halted}"
shows "Bdelta μ i = {}"
using assms
by (auto simp: step_kind_defs next_state_def Bdelta_def degree_reg_def split: if_split_asm prod.split)
end
definition "ok_fun_73 ≡ λk. - (real k powr (3/4))"
lemma ok_fun_73: "ok_fun_73 ∈ o(real)"
unfolding ok_fun_73_def by real_asymp
lemma (in Book) X_7_3:
assumes big: "Big_Blue_4_1 μ l"
defines "ℬ ≡ Step_class {bblue_step}"
defines "𝒮 ≡ Step_class {dboost_step}"
shows "(∏i ∈ ℬ. card (Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr (ok_fun_73 k) * μ ^ (l - card 𝒮)"
proof -
have [simp]: "finite ℬ" "finite 𝒮" and cardℬ: "card ℬ ≤ l powr (3/4)"
using assms bblue_step_limit big by (auto simp: ℬ_def 𝒮_def)
define b where "b ≡ λi. card (Bdelta μ i)"
obtain i where "card (Bseq i) = sum b ℬ + card 𝒮"
proof -
define i where "i = Suc (Max (ℬ ∪ 𝒮))"
define TRIV where "TRIV ≡ Step_class {red_step,dreg_step,halted} ∩ {..<i}"
have [simp]: "finite TRIV"
by (auto simp: TRIV_def)
have eq: "ℬ ∪ 𝒮 ∪ TRIV = {..<i}"
proof
show "ℬ ∪ 𝒮 ∪ TRIV ⊆ {..<i}"
by (auto simp: i_def TRIV_def less_Suc_eq_le)
show "{..<i} ⊆ ℬ ∪ 𝒮 ∪ TRIV"
using stepkind.exhaust by (auto simp: ℬ_def 𝒮_def TRIV_def Step_class_def)
qed
have dis: "ℬ ∩ 𝒮 = {}" "(ℬ ∪ 𝒮) ∩ TRIV = {}"
by (auto simp: ℬ_def 𝒮_def TRIV_def Step_class_def)
show thesis
proof
have "card (Bseq i) = (∑j ∈ ℬ ∪ 𝒮 ∪ TRIV. b j)"
using card_Bseq_sum eq unfolding b_def by metis
also have "… = (∑j∈ℬ. b j) + (∑j∈𝒮. b j) + (∑j∈TRIV. b j)"
by (simp add: sum_Un_nat dis)
also have "… = sum b ℬ + card 𝒮"
by (simp add: b_def 𝒮_def card_Bdelta_dboost_step TRIV_def Bdelta_trivial_step)
finally show "card (Bseq i) = sum b ℬ + card 𝒮" .
qed
qed
then have sum_b_ℬ: "sum b ℬ ≤ l - card 𝒮"
by (metis Bseq_less_l less_diff_conv nat_less_le)
have "real (card ℬ) ≤ real k powr (3/4)"
using cardℬ l_le_k
by (smt (verit, best) divide_nonneg_pos of_nat_0_le_iff of_nat_mono powr_mono2)
then have "2 powr (ok_fun_73 k) ≤ (1/2) ^ card ℬ"
by (simp add: ok_fun_73_def powr_minus divide_simps flip: powr_realpow)
then have "2 powr (ok_fun_73 k) * μ ^ (l - card 𝒮) ≤ (1/2) ^ card ℬ * μ ^ (l - card 𝒮)"
by (simp add: μ01)
also have "(1/2) ^ card ℬ * μ ^ (l - card 𝒮) ≤ (1/2) ^ card ℬ * μ ^ (sum b ℬ)"
using μ01 sum_b_ℬ by simp
also have "… = (∏i∈ℬ. μ ^ b i / 2)"
by (simp add: power_sum prod_dividef divide_simps)
also have "… ≤ (∏i∈ℬ. card (Xseq (Suc i)) / card (Xseq i))"
proof (rule prod_mono)
fix i :: nat
assume "i ∈ ℬ"
then have "¬ termination_condition (Xseq i) (Yseq i)"
by (simp add: ℬ_def Step_class_def flip: step_non_terminating_iff)
then have "card (Xseq i) ≠ 0"
using termination_condition_def by force
with ‹i∈ℬ› μ01 show "0 ≤ μ ^ b i / 2 ∧ μ ^ b i / 2 ≤ card (Xseq (Suc i)) / card (Xseq i)"
by (force simp: b_def ℬ_def divide_simps dest!: Bdelta_bblue_step)
qed
finally show ?thesis .
qed
subsection ‹Lemma 7.5›
text ‹Small $o(k)$ bounds on summations for this section›
text ‹This is the explicit upper bound for heights given just below (5) on page 9›
definition "ok_fun_26 ≡ λk. 2 * ln k / eps k"
definition "ok_fun_28 ≡ λk. -2 * real k powr (7/8)"
lemma ok_fun_26: "ok_fun_26 ∈ o(real)" and ok_fun_28: "ok_fun_28 ∈ o(real)"
unfolding ok_fun_26_def ok_fun_28_def eps_def by real_asymp+
definition
"Big_X_7_5 ≡
λμ l. Big_Blue_4_1 μ l ∧ Big_Red_5_3 μ l ∧ Big_Y_6_5_Bblue l
∧ (∀k≥l. Big_height_upper_bound k ∧ k≥16 ∧ (ok_fun_26 k - ok_fun_28 k ≤ k))"
text ‹establishing the size requirements for 7.5›
lemma Big_X_7_5:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_5 μ l"
proof -
have ok: "∀⇧∞l. ok_fun_26 l - ok_fun_28 l ≤ l"
unfolding eps_def ok_fun_26_def ok_fun_28_def by real_asymp
show ?thesis
using assms Big_Y_6_5_Bblue Big_Red_5_3 Big_Blue_4_1
unfolding Big_X_7_5_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_ge_at_top ok Big_height_upper_bound; real_asymp)
done
qed
context Book
begin
lemma X_26_and_28:
assumes big: "Big_X_7_5 μ l"
defines "𝒟 ≡ Step_class {dreg_step}"
defines "ℬ ≡ Step_class {bblue_step}"
defines "ℋ ≡ Step_class {halted}"
defines "h ≡ λi. real (hgt (pseq i))"
obtains "(∑i∈{..<halted_point} ∖ 𝒟. h (Suc i) - h (i-1)) ≤ ok_fun_26 k"
"ok_fun_28 k ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))"
proof -
define 𝒮 where "𝒮 ≡ Step_class {dboost_step}"
have B_limit: "Big_Blue_4_1 μ l" and bigY65B: "Big_Y_6_5_Bblue l"
and hub: "Big_height_upper_bound k"
using big l_le_k by (auto simp: Big_X_7_5_def)
have m_minimal: "i ∉ ℋ ⟷ i < halted_point" for i
unfolding ℋ_def using halted_point_minimal assms by blast
have oddset: "{..<halted_point} ∖ 𝒟 = {i ∈ {..<halted_point}. odd i}"
using m_minimal step_odd step_even not_halted_even_dreg
by (auto simp: 𝒟_def ℋ_def Step_class_insert_NO_MATCH)
have "ok_fun_28 k ≤ -2 * ε powr (-1/2) * card ℬ"
proof -
have "k powr (1/8) * card ℬ ≤ k powr (1/8) * l powr (3/4)"
using B_limit bblue_step_limit by (simp add: ℬ_def mult_left_mono)
also have "… ≤ k powr (1/8) * k powr (3/4)"
by (simp add: l_le_k mult_mono powr_mono2)
also have "… = k powr (7/8)"
by (simp flip: powr_add)
finally show ?thesis
by (simp add: eps_def powr_powr ok_fun_28_def)
qed
also have "… ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))"
proof -
have "(∑i ∈ ℬ. -2 * ε powr (-1/2)) ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))"
proof (rule sum_mono)
fix i :: nat
assume i: "i ∈ ℬ"
show "-2 * ε powr (-1/2) ≤ h(Suc i) - h(i-1)"
using bigY65B kn0 i Y_6_5_Bblue by (fastforce simp: ℬ_def h_def)
qed
then show ?thesis
by (simp add: mult.commute)
qed
finally have 28: "ok_fun_28 k ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))" .
have "(∑i ∈ {..<halted_point} ∖ 𝒟. h(Suc i) - h(i-1)) ≤ h halted_point - h 0"
proof (cases "even halted_point")
case False
have "hgt (pseq (halted_point - Suc 0)) ≤ hgt (pseq halted_point)"
using Y_6_5_DegreeReg [of "halted_point-1"] False m_minimal not_halted_even_dreg odd_pos
by (fastforce simp: ℋ_def)
then have "h(halted_point - Suc 0) ≤ h halted_point"
using h_def of_nat_mono by blast
with False show ?thesis
by (simp add: oddset sum_odds_odd)
qed (simp add: oddset sum_odds_even)
also have "… ≤ ok_fun_26 k"
proof -
have "hgt (pseq i) ≥ 1" for i
by (simp add: Suc_leI hgt_gt0)
moreover have "hgt (pseq halted_point) ≤ ok_fun_26 k"
using hub pee_le1 height_upper_bound unfolding ok_fun_26_def by blast
ultimately show ?thesis
by (simp add: h_def)
qed
finally have 26: "(∑i∈{..<halted_point} ∖ 𝒟. h (Suc i) - h (i-1)) ≤ ok_fun_26 k" .
with 28 show ?thesis
using that by blast
qed
proposition X_7_5:
assumes μ: "0<μ" "μ<1"
defines "𝒮 ≡ Step_class {dboost_step}" and "𝒮𝒮 ≡ dboost_star"
assumes big: "Big_X_7_5 μ l"
shows "card (𝒮∖𝒮𝒮) ≤ 3 * ε powr (1/4) * k"
proof -
define 𝒟 where "𝒟 ≡ Step_class {dreg_step}"
define ℛ where "ℛ ≡ Step_class {red_step}"
define ℬ where "ℬ ≡ Step_class {bblue_step}"
define h where "h ≡ λi. real (hgt (pseq i))"
obtain 26: "(∑i∈{..<halted_point} ∖ 𝒟. h (Suc i) - h (i-1)) ≤ ok_fun_26 k"
and 28: "ok_fun_28 k ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))"
using X_26_and_28 assms(1-3) big
unfolding ℬ_def 𝒟_def h_def Big_X_7_5_def by blast
have 𝒮𝒮: "𝒮𝒮 = {i ∈ 𝒮. h(Suc i) - h i ≤ ε powr (-1/4)}" and "𝒮𝒮 ⊆ 𝒮"
by (auto simp: 𝒮𝒮_def 𝒮_def dboost_star_def h_def)
have in_S: "h(Suc i) - h i > ε powr (-1/4)" if "i ∈ 𝒮∖𝒮𝒮" for i
using that by (fastforce simp: 𝒮𝒮)
have B_limit: "Big_Blue_4_1 μ l"
and bigR53: "Big_Red_5_3 μ l"
and 16: "k≥16"
and ok_fun: "ok_fun_26 k - ok_fun_28 k ≤ k"
using big l_le_k by (auto simp: Big_X_7_5_def)
have [simp]: "finite ℛ" "finite ℬ" "finite 𝒮"
using finite_components by (auto simp: ℛ_def ℬ_def 𝒮_def)
have [simp]: "ℛ ∩ 𝒮 = {}" "ℬ ∩ (ℛ∪𝒮) = {}"
by (auto simp: ℛ_def 𝒮_def ℬ_def Step_class_def)
obtain cardss: "card 𝒮𝒮 ≤ card 𝒮" "card (𝒮∖𝒮𝒮) = card 𝒮 - card 𝒮𝒮"
by (meson ‹𝒮𝒮 ⊆ 𝒮› ‹finite 𝒮› card_Diff_subset card_mono infinite_super)
have "(∑i ∈ 𝒮. h(Suc i) - h(i-1)) ≥ ε powr (-1/4) * card (𝒮∖𝒮𝒮)"
proof -
have "(∑i ∈ 𝒮∖𝒮𝒮. h(Suc i) - h(i-1)) ≥ (∑i ∈ 𝒮∖𝒮𝒮. ε powr (-1/4))"
proof (rule sum_mono)
fix i :: nat
assume i: "i ∈ 𝒮∖𝒮𝒮"
with i obtain "i-1 ∈ 𝒟" "i>0"
using dreg_before_step1 dreg_before_gt0 by (fastforce simp: 𝒮_def 𝒟_def Step_class_insert_NO_MATCH)
with i show "ε powr (-1/4) ≤ h(Suc i) - h(i-1)"
using in_S[of i] Y_6_5_DegreeReg[of "i-1"] by (simp add: 𝒟_def h_def)
qed
moreover
have "(∑i ∈ 𝒮𝒮. h(Suc i) - h(i-1)) ≥ 0"
proof (intro sum_nonneg)
show "⋀i. i ∈ 𝒮𝒮 ⟹ 0 ≤ h (Suc i) - h (i - 1)"
using Y_6_4_dbooSt μ bigR53 by(auto simp: h_def 𝒮𝒮 𝒮_def hgt_mono)
qed
ultimately show ?thesis
by (simp add: mult.commute sum.subset_diff [OF ‹𝒮𝒮 ⊆ 𝒮› ‹finite 𝒮›])
qed
moreover
have "(∑i ∈ ℛ. h(Suc i) - h(i-1)) ≥ (∑i ∈ ℛ. -2)"
proof (rule sum_mono)
fix i :: nat
assume i: "i ∈ ℛ"
with i obtain "i-1 ∈ 𝒟" "i>0"
using dreg_before_step1 dreg_before_gt0
by (fastforce simp: ℛ_def 𝒟_def Step_class_insert_NO_MATCH)
with i have "hgt (pseq (i-1)) - 2 ≤ hgt (pseq (Suc i))"
using Y_6_5_Red[of i] 16 Y_6_5_DegreeReg[of "i-1"]
by (fastforce simp: algebra_simps ℛ_def 𝒟_def)
then show "- 2 ≤ h(Suc i) - h(i-1)"
unfolding h_def by linarith
qed
ultimately have 27: "(∑i ∈ ℛ∪𝒮. h(Suc i) - h(i-1)) ≥ ε powr (-1/4) * card (𝒮∖𝒮𝒮) - 2 * card ℛ"
by (simp add: sum.union_disjoint)
have "ok_fun_28 k + (ε powr (-1/4) * card (𝒮∖𝒮𝒮) - 2 * card ℛ) ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1)) + (∑i ∈ ℛ∪𝒮. h(Suc i) - h(i-1))"
using 27 28 by simp
also have "… = (∑i ∈ ℬ ∪ (ℛ∪𝒮). h(Suc i) - h(i-1))"
by (simp add: sum.union_disjoint)
also have "… = (∑i ∈ {..<halted_point} ∖ 𝒟. h(Suc i) - h(i-1))"
proof -
have "i ∈ ℬ ∪ (ℛ∪𝒮)" if "i < halted_point" "i ∉ 𝒟" for i
using that unfolding 𝒟_def ℬ_def ℛ_def 𝒮_def
using Step_class_cases halted_point_minimal by auto
moreover
have "i ∈ {..<halted_point} ∖ 𝒟" if "i ∈ ℬ ∪ (ℛ∪𝒮)" for i
using halted_point_minimal' that by (force simp: 𝒟_def ℬ_def ℛ_def 𝒮_def Step_class_def)
ultimately have "ℬ ∪ (ℛ∪𝒮) = {..<halted_point} ∖ 𝒟"
by auto
then show ?thesis
by simp
qed
finally have "ok_fun_28 k + (ε powr (-1/4) * card (𝒮∖𝒮𝒮) - real (2 * card ℛ)) ≤ ok_fun_26 k"
using 26 by simp
then have "real (card (𝒮 ∖ 𝒮𝒮)) ≤ (ok_fun_26 k - ok_fun_28 k + 2 * card ℛ) * ε powr (1/4)"
using eps_gt0 by (simp add: powr_minus field_simps del: div_add div_mult_self3)
moreover have "card ℛ < k"
using red_step_limit μ unfolding ℛ_def by blast
ultimately have "card (𝒮∖𝒮𝒮) ≤ (k + 2 * k) * ε powr (1/4)"
by (smt (verit, best) of_nat_add mult_2 mult_right_mono nat_less_real_le ok_fun powr_ge_zero)
then show ?thesis
by (simp add: algebra_simps)
qed
end
subsection ‹Lemma 7.4›
definition
"Big_X_7_4 ≡ λμ l. Big_X_7_5 μ l ∧ Big_Red_5_3 μ l"
text ‹establishing the size requirements for 7.4›
lemma Big_X_7_4:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_4 μ l"
using assms Big_X_7_5 Big_Red_5_3
unfolding Big_X_7_4_def
by (simp add: eventually_conj_iff all_imp_conj_distrib)
definition "ok_fun_74 ≡ λk. -6 * eps k powr (1/4) * k * ln k / ln 2"
lemma ok_fun_74: "ok_fun_74 ∈ o(real)"
unfolding ok_fun_74_def eps_def by real_asymp
context Book
begin
lemma X_7_4:
assumes big: "Big_X_7_4 μ l"
defines "𝒮 ≡ Step_class {dboost_step}"
shows "(∏i∈𝒮. card (Xseq (Suc i)) / card (Xseq i)) ≥ 2 powr ok_fun_74 k * bigbeta ^ card 𝒮"
proof -
define 𝒮𝒮 where "𝒮𝒮 ≡ dboost_star"
then have big53: "Big_Red_5_3 μ l" and X75: "card (𝒮∖𝒮𝒮) ≤ 3 * ε powr (1/4) * k"
using μ01 big by (auto simp: Big_X_7_4_def X_7_5 𝒮_def 𝒮𝒮_def)
then have R53: "pseq (Suc i) ≥ pseq i ∧ beta i ≥ 1 / (real k)⇧2" and beta_gt0: "0 < beta i"
if "i ∈ 𝒮" for i
using that Red_5_3 beta_gt0 by (auto simp: 𝒮_def)
have bigbeta01: "bigbeta ∈ {0<..<1}"
using big53 assms bigbeta_gt0 bigbeta_less1 by force
have "𝒮𝒮 ⊆ 𝒮"
unfolding 𝒮𝒮_def 𝒮_def dboost_star_def by auto
then obtain [simp]: "finite 𝒮" "finite 𝒮𝒮"
by (simp add: 𝒮𝒮_def 𝒮_def finite_dboost_star)
have card_SSS: "card 𝒮𝒮 ≤ card 𝒮"
by (metis 𝒮𝒮_def 𝒮_def ‹finite 𝒮› card_mono dboost_star_subset)
have β: "beta i = card (Xseq (Suc i)) / card (Xseq i)" if "i ∈ 𝒮" for i
proof -
have "Xseq (Suc i) = Neighbours Blue (cvx i) ∩ Xseq i"
using that unfolding 𝒮_def
by (auto simp: step_kind_defs next_state_def split: prod.split)
then show ?thesis
by (force simp: beta_eq)
qed
then have *: "(∏i∈𝒮. card (Xseq (Suc i)) / card (Xseq i)) = (∏i∈𝒮. beta i)"
by force
have prod_beta_gt0: "prod (beta) S' > 0" if "S' ⊆ 𝒮" for S'
using beta_gt0 that
by (force simp: beta_ge0 intro: prod_pos)
have "(∏i∈𝒮∖𝒮𝒮. 1 / beta i) ≤ (∏i∈𝒮∖𝒮𝒮. real k ^ 2)"
proof (rule prod_mono)
fix i
assume i: "i ∈ 𝒮 ∖ 𝒮𝒮"
with R53 kn0 beta_ge0 [of i] show "0 ≤ 1 / beta i ∧ 1 / beta i ≤ (real k)⇧2"
by (force simp: R53 divide_simps mult.commute)
qed
then have "(∏i∈𝒮∖𝒮𝒮. 1 / beta i) ≤ real k ^ (2 * card(𝒮∖𝒮𝒮))"
by (simp add: power_mult)
also have "… = real k powr (2 * card(𝒮∖𝒮𝒮))"
by (metis kn0 of_nat_0_less_iff powr_realpow)
also have "… ≤ k powr (2 * 3 * ε powr (1/4) * k)"
using X75 kn0 by (intro powr_mono; linarith)
also have "… ≤ exp (6 * ε powr (1/4) * k * ln k)"
by (simp add: powr_def)
also have "… = 2 powr -ok_fun_74 k"
by (simp add: ok_fun_74_def powr_def)
finally have "(∏i∈𝒮∖𝒮𝒮. 1 / beta i) ≤ 2 powr -ok_fun_74 k" .
then have A: "(∏i∈𝒮∖𝒮𝒮. beta i) ≥ 2 powr ok_fun_74 k"
using prod_beta_gt0[of "𝒮∖𝒮𝒮"]
by (simp add: powr_minus prod_dividef mult.commute divide_simps)
have "(∏i∈𝒮𝒮. 1 / beta i) ≤ bigbeta powr (- (card 𝒮𝒮))"
proof (cases "𝒮𝒮 = {}")
case True
with bigbeta01 show ?thesis
by fastforce
next
case False
then have "card 𝒮𝒮 > 0"
using ‹finite 𝒮𝒮› card_0_eq by blast
have "(∏i∈𝒮𝒮. 1 / beta i) powr (1 / card 𝒮𝒮) ≤ (∑i∈𝒮𝒮. 1 / beta i / card 𝒮𝒮)"
proof (rule arith_geom_mean [OF ‹finite 𝒮𝒮› ‹𝒮𝒮 ≠ {}›])
show "⋀i. i ∈ 𝒮𝒮 ⟹ 0 ≤ 1 / beta i"
by (simp add: beta_ge0)
qed
then have "((∏i∈𝒮𝒮. 1 / beta i) powr (1 / card 𝒮𝒮)) powr (card 𝒮𝒮)
≤ (∑i∈𝒮𝒮. 1 / beta i / card 𝒮𝒮) powr (card 𝒮𝒮)"
using powr_mono2 by auto
with ‹𝒮𝒮 ≠ {}›
have "(∏i∈𝒮𝒮. 1 / beta i) ≤ (∑i∈𝒮𝒮. 1 / beta i / card 𝒮𝒮) powr (card 𝒮𝒮)"
by (simp add: powr_powr beta_ge0 prod_nonneg)
also have "… ≤ (1 / (card 𝒮𝒮) * (∑i∈𝒮𝒮. 1 / beta i)) powr (card 𝒮𝒮)"
using ‹card 𝒮𝒮 > 0› by (simp add: field_simps sum_divide_distrib)
also have "… ≤ bigbeta powr (- (card 𝒮𝒮))"
using ‹𝒮𝒮 ≠ {}› ‹card 𝒮𝒮 > 0›
by (simp add: bigbeta_def field_simps powr_minus powr_divide beta_ge0 sum_nonneg flip: 𝒮𝒮_def)
finally show ?thesis .
qed
then have B: "(∏i∈𝒮𝒮. beta i) ≥ bigbeta powr (card 𝒮𝒮)"
using ‹𝒮𝒮 ⊆ 𝒮› prod_beta_gt0[of "𝒮𝒮"] bigbeta01
by (simp add: powr_minus prod_dividef mult.commute divide_simps)
have "2 powr ok_fun_74 k * bigbeta powr card 𝒮 ≤ 2 powr ok_fun_74 k * bigbeta powr card 𝒮𝒮"
using bigbeta01 big53 card_SSS by (simp add: powr_mono')
also have "… ≤ (∏i∈𝒮∖𝒮𝒮. beta i) * (∏i∈𝒮𝒮. beta i)"
using beta_ge0 by (intro mult_mono A B) (auto simp: prod_nonneg)
also have "… = (∏i∈𝒮. beta i)"
by (metis ‹𝒮𝒮 ⊆ 𝒮› ‹finite 𝒮› prod.subset_diff)
finally have "2 powr ok_fun_74 k * bigbeta powr real (card 𝒮) ≤ prod (beta) 𝒮" .
with bigbeta01 show ?thesis
by (simp add: "*" powr_realpow)
qed
subsection ‹Observation 7.7›
lemma X_7_7:
assumes i: "i ∈ Step_class {dreg_step}"
defines "q ≡ ε powr (-1/2) * alpha (hgt (pseq i))"
shows "pseq (Suc i) - pseq i ≥ card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) * q ∧ card (Xseq (Suc i)) > 0"
proof -
have finX: "finite (Xseq i)" for i
using finite_Xseq by blast
define Y where "Y ≡ Yseq"
have "Xseq (Suc i) = {x ∈ Xseq i. red_dense (Y i) (red_density (Xseq i) (Y i)) x}"
and Y: "Y (Suc i) = Y i"
using i
by (simp_all add: step_kind_defs next_state_def X_degree_reg_def degree_reg_def
Y_def split: if_split_asm prod.split_asm)
then have Xseq: "Xseq (Suc i) = {x ∈ Xseq i. card (Neighbours Red x ∩ Y i) ≥ (pseq i - q) * card (Y i)}"
by (simp add: red_dense_def q_def pseq_def Y_def)
have Xsub[simp]: "Xseq (Suc i) ⊆ Xseq i"
using Xseq_Suc_subset by blast
then have card_le: "card (Xseq (Suc i)) ≤ card (Xseq i)"
by (simp add: card_mono finX)
have [simp]: "disjnt (Xseq i) (Y i)"
using Xseq_Yseq_disjnt Y_def by blast
have Xnon0: "card (Xseq i) > 0" and Ynon0: "card (Y i) > 0"
using i by (simp_all add: Y_def Xseq_gt0 Yseq_gt0 Step_class_def)
have "alpha (hgt (pseq i)) > 0"
by (simp add: alpha_gt0 kn0 hgt_gt0)
with kn0 have "q > 0"
by (smt (verit) q_def eps_gt0 mult_pos_pos powr_gt_zero)
have Xdif: "Xseq i ∖ Xseq (Suc i) = {x ∈ Xseq i. card (Neighbours Red x ∩ Y i) < (pseq i - q) * card (Y i)}"
using Xseq by force
have disYX: "disjnt (Y i) (Xseq i ∖ Xseq (Suc i))"
by (metis Diff_subset ‹disjnt (Xseq i) (Y i)› disjnt_subset2 disjnt_sym)
have "edge_card Red (Y i) (Xseq i ∖ Xseq (Suc i))
= (∑x ∈ Xseq i ∖ Xseq (Suc i). real (card (Neighbours Red x ∩ Y i)))"
using edge_card_eq_sum_Neighbours [OF _ _ disYX] finX Red_E by simp
also have "… ≤ (∑x ∈ Xseq i ∖ Xseq (Suc i). (pseq i - q) * card (Y i))"
by (smt (verit, del_insts) Xdif mem_Collect_eq sum_mono)
finally have A: "edge_card Red (Xseq i ∖ Xseq (Suc i)) (Y i) ≤ card (Xseq i ∖ Xseq (Suc i)) * (pseq i - q) * card (Y i)"
by (simp add: edge_card_commute)
then have False if "Xseq (Suc i) = {}"
using ‹q>0› Xnon0 Ynon0 that by (simp add: edge_card_eq_pee Y_def mult_le_0_iff)
then have XSnon0: "card (Xseq (Suc i)) > 0"
using card_gt_0_iff finX by blast
have "pseq i * card (Xseq i) * real (card (Y i)) - edge_card Red (Xseq (Suc i)) (Y i)
≤ card (Xseq i ∖ Xseq (Suc i)) * (pseq i - q) * card (Y i)"
by (metis A edge_card_eq_pee edge_card_mono Y_def Xsub ‹disjnt (Xseq i) (Y i)› edge_card_diff finX of_nat_diff)
moreover have "real (card (Xseq (Suc i))) ≤ real (card (Xseq i))"
using Xsub by (simp add: card_le)
ultimately have §: "edge_card Red (Xseq (Suc i)) (Y i) ≥ pseq i * card (Xseq (Suc i)) * card (Y i) + card (Xseq i ∖ Xseq (Suc i)) * q * card (Y i)"
using Xnon0
by (smt (verit, del_insts) Xsub card_Diff_subset card_gt_0_iff card_le left_diff_distrib finite_subset mult_of_nat_commute of_nat_diff)
have "edge_card Red (Xseq (Suc i)) (Y i) / (card (Xseq (Suc i)) * card (Y i)) ≥ pseq i + card (Xseq i ∖ Xseq (Suc i)) * q / card (Xseq (Suc i))"
using divide_right_mono [OF §, of "card (Xseq (Suc i)) * card (Y i)"] XSnon0 Ynon0
by (simp add: add_divide_distrib split: if_split_asm)
moreover have "pseq (Suc i) = real (edge_card Red (Xseq (Suc i)) (Y i)) / (real (card (Y i)) * real (card (Xseq (Suc i))))"
using Y by (simp add: pseq_def gen_density_def Y_def)
ultimately show ?thesis
by (simp add: algebra_simps XSnon0)
qed
end
subsection ‹Lemma 7.8›
definition "Big_X_7_8 ≡ λk. k≥2 ∧ eps k powr (1/2) / k ≥ 2 / k^2"
lemma Big_X_7_8: "∀⇧∞k. Big_X_7_8 k"
unfolding eps_def Big_X_7_8_def eventually_conj_iff eps_def
by (intro conjI; real_asymp)
lemma (in Book) X_7_8:
assumes big: "Big_X_7_8 k"
and i: "i ∈ Step_class {dreg_step}"
shows "card (Xseq (Suc i)) ≥ card (Xseq i) / k^2"
proof -
define q where "q ≡ ε powr (-1/2) * alpha (hgt (pseq i))"
have "k>0" ‹k≥2› using big by (auto simp: Big_X_7_8_def)
have "2 / k^2 ≤ ε powr (1/2) / k"
using big by (auto simp: Big_X_7_8_def)
also have "… ≤ q"
using kn0 eps_gt0 Red_5_7a [of "pseq i"]
by (simp add: q_def powr_minus divide_simps flip: powr_add)
finally have q_ge: "q ≥ 2 / k^2" .
define Y where "Y ≡ Yseq"
have "Xseq (Suc i) = {x ∈ Xseq i. red_dense (Y i) (red_density (Xseq i) (Y i)) x}"
and Y: "Y (Suc i) = Y i"
using i
by (simp_all add: step_kind_defs next_state_def X_degree_reg_def degree_reg_def
Y_def split: if_split_asm prod.split_asm)
have XSnon0: "card (Xseq (Suc i)) > 0"
using X_7_7 kn0 assms by simp
have finX: "finite (Xseq i)" for i
using finite_Xseq by blast
have Xsub[simp]: "Xseq (Suc i) ⊆ Xseq i"
using Xseq_Suc_subset by blast
then have card_le: "card (Xseq (Suc i)) ≤ card (Xseq i)"
by (simp add: card_mono finX)
have "2 ≤ (real k)⇧2"
by (metis of_nat_numeral ‹2 ≤ k› of_nat_power_le_of_nat_cancel_iff self_le_ge2_pow)
then have 2: "2 / (real k ^ 2 + 2) ≥ 1 / k^2"
by (simp add: divide_simps)
have "q * card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) ≤ pseq (Suc i) - pseq i"
using X_7_7 μ01 kn0 assms by (simp add: q_def mult_of_nat_commute)
also have "… ≤ 1"
by (smt (verit) pee_ge0 pee_le1)
finally have "q * card (Xseq i ∖ Xseq (Suc i)) ≤ card (Xseq (Suc i))"
using XSnon0 by auto
with q_ge have "card (Xseq (Suc i)) ≥ (2 / k^2) * card (Xseq i ∖ Xseq (Suc i))"
by (smt (verit, best) mult_right_mono of_nat_0_le_iff)
then have "card (Xseq (Suc i)) * (1 + 2/k^2) ≥ (2/k^2) * card (Xseq i)"
by (simp add: card_Diff_subset finX card_le diff_divide_distrib field_simps)
then have "card (Xseq (Suc i)) ≥ (2/(real k ^ 2 + 2)) * card (Xseq i)"
using kn0 add_nonneg_nonneg[of "real k^2" 2]
by (simp del: add_nonneg_nonneg add: divide_simps split: if_split_asm)
then show ?thesis
using mult_right_mono [OF 2, of "card (Xseq i)"] by simp
qed
subsection ‹Lemma 7.9›
definition "Big_X_7_9 ≡ λk. ((1 + eps k) powr (eps k powr (-1/4) + 1) - 1) / eps k ≤ 2 * eps k powr (-1/4)
∧ k≥2 ∧ eps k powr (1/2) / k ≥ 2 / k^2"
lemma Big_X_7_9: "∀⇧∞k. Big_X_7_9 k"
unfolding eps_def Big_X_7_9_def eventually_conj_iff eps_def
by (intro conjI; real_asymp)
lemma one_plus_powr_le:
fixes p::real
assumes "0≤p" "p≤1" "x≥0"
shows "(1+x) powr p - 1 ≤ x*p"
proof -
define f where "f ≡ λx. x*p - ((1+x) powr p - 1)"
have "0 ≤ f 0"
by (simp add: f_def)
also have "… ≤ f x"
proof (intro DERIV_nonneg_imp_nondecreasing[of concl: f] exI conjI assms)
fix y::real
assume y: "0 ≤ y" "y ≤ x"
show "(f has_real_derivative p - (1+y)powr (p-1) * p) (at y)"
unfolding f_def using assms y by (intro derivative_eq_intros | simp)+
show "p - (1+y)powr (p-1) * p ≥ 0"
using y assms less_eq_real_def powr_less_one by fastforce
qed
finally show ?thesis
by (simp add: f_def)
qed
lemma (in Book) X_7_9:
assumes i: "i ∈ Step_class {dreg_step}" and big: "Big_X_7_9 k"
defines "hp ≡ λi. hgt (pseq i)"
assumes "pseq i ≥ p0" and hgt: "hp (Suc i) ≤ hp i + ε powr (-1/4)"
shows "card (Xseq (Suc i)) ≥ (1 - 2 * ε powr (1/4)) * card (Xseq i)"
proof -
have k: "k≥2" "ε powr (1/2) / k ≥ 2 / k^2"
using big by (auto simp: Big_X_7_9_def)
let ?q = "ε powr (-1/2) * alpha (hp i)"
have "k>0" using k by auto
have Xsub[simp]: "Xseq (Suc i) ⊆ Xseq i"
using Xseq_Suc_subset by blast
have finX: "finite (Xseq i)" for i
using finite_Xseq by blast
then have card_le: "card (Xseq (Suc i)) ≤ card (Xseq i)"
by (simp add: card_mono finX)
have XSnon0: "card (Xseq (Suc i)) > 0"
using X_7_7 ‹0 < k› i by blast
have "card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) * ?q ≤ pseq (Suc i) - pseq i"
using X_7_7 i k hp_def by auto
also have "… ≤ 2 * ε powr (-1/4) * alpha (hp i)"
proof -
have hgt_le: "hp i ≤ hp (Suc i)"
using Y_6_5_DegreeReg ‹0 < k› i hp_def by blast
have A: "pseq (Suc i) ≤ qfun (hp (Suc i))"
by (simp add: ‹0 < k› hp_def hgt_works)
have B: "qfun (hp i - 1) ≤ pseq i"
using hgt_Least [of "hp i - 1" "pseq i"] ‹pseq i ≥ p0› by (force simp: hp_def)
have "pseq (Suc i) - pseq i ≤ qfun (hp (Suc i)) - qfun (hp i - 1)"
using A B by auto
also have "… = ((1 + ε) ^ (Suc (hp i - 1 + hp (Suc i)) - hp i) -
(1 + ε) ^ (hp i - 1)) / k"
using kn0 eps_gt0 hgt_le ‹pseq i ≥ p0› hgt_gt0 [of k]
by (simp add: hp_def qfun_eq Suc_diff_eq_diff_pred hgt_gt0 diff_divide_distrib)
also have "… = alpha (hp i) / ε * ((1 + ε) ^ (1 + hp (Suc i) - hp i) - 1)"
using kn0 hgt_le hgt_gt0
by (simp add: hp_def alpha_eq right_diff_distrib flip: diff_divide_distrib power_add)
also have "… ≤ 2 * ε powr (-1/4) * alpha (hp i)"
proof -
have "((1 + ε) ^ (1 + hp (Suc i) - hp i) - 1) / ε ≤ ((1 + ε) powr (ε powr (-1/4) + 1) - 1) / ε"
using hgt eps_ge0 hgt_le powr_mono_both by (force simp flip: powr_realpow intro: divide_right_mono)
also have "… ≤ 2 * ε powr (-1/4)"
using big by (meson Big_X_7_9_def)
finally have *: "((1 + ε) ^ (1 + hp (Suc i) - hp i) - 1) / ε ≤ 2 * ε powr (-1/4)" .
show ?thesis
using mult_left_mono [OF *, of "alpha (hp i)"]
by (smt (verit) alpha_ge0 mult.commute times_divide_eq_right)
qed
finally show ?thesis .
qed
finally have 29: "card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) * ?q ≤ 2 * ε powr (-1/4) * alpha (hp i)" .
moreover have "alpha (hp i) > 0"
unfolding hp_def
by (smt (verit, ccfv_SIG) eps_gt0 ‹0 < k› alpha_ge divide_le_0_iff hgt_gt0 of_nat_0_less_iff)
ultimately have "card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) * ε powr (-1/2) ≤ 2 * ε powr (-1/4)"
using mult_le_cancel_right by fastforce
then have "card (Xseq i ∖ Xseq (Suc i)) / card (Xseq (Suc i)) ≤ 2 * ε powr (-1/4) * ε powr (1/2)"
using ‹0 < k› eps_gt0
by (force simp: powr_minus divide_simps mult.commute mult_less_0_iff)
then have "card (Xseq i ∖ Xseq (Suc i)) ≤ 2 * ε powr (1/4) * card (Xseq (Suc i))"
using XSnon0 by (simp add: field_simps flip: powr_add)
also have "… ≤ 2 * ε powr (1/4) * card (Xseq i)"
by (simp add: card_le mult_mono')
finally show ?thesis
by (simp add: card_Diff_subset finX card_le algebra_simps)
qed
subsection ‹Lemma 7.10›
definition "Big_X_7_10 ≡ λμ l. Big_X_7_5 μ l ∧ Big_Red_5_3 μ l"
text ‹establishing the size requirements for 7.10›
lemma Big_X_7_10:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_10 μ l"
using Big_X_7_10_def Big_X_7_4 Big_X_7_4_def assms by force
lemma (in Book) X_7_10:
defines "ℛ ≡ Step_class {red_step}"
defines "𝒮 ≡ Step_class {dboost_step}"
defines "h ≡ λi. real (hgt (pseq i))"
defines "C ≡ {i. h i ≥ h (i-1) + ε powr (-1/4)}"
assumes big: "Big_X_7_10 μ l"
shows "card ((ℛ∪𝒮) ∩ C) ≤ 3 * ε powr (1/4) * k"
proof -
define 𝒟 where "𝒟 ≡ Step_class {dreg_step}"
define ℬ where "ℬ ≡ Step_class {bblue_step}"
have hub: "Big_height_upper_bound k"
and 16: "k≥16"
and ok_le_k: "ok_fun_26 k - ok_fun_28 k ≤ k"
and bigR53: "Big_Red_5_3 μ l"
using big l_le_k by (auto simp: Big_X_7_5_def Big_X_7_10_def)
have "ℛ∪𝒮 ⊆ {..<halted_point} ∖ 𝒟 ∖ ℬ" and BmD: "ℬ ⊆ {..<halted_point} ∖ 𝒟"
using halted_point_minimal'
by (fastforce simp: ℛ_def 𝒮_def 𝒟_def ℬ_def Step_class_def)+
then have RS_eq: "ℛ∪𝒮 = {..<halted_point} ∖ 𝒟 - ℬ"
using halted_point_minimal Step_class_cases by (auto simp: ℛ_def 𝒮_def 𝒟_def ℬ_def)
obtain 26: "(∑i∈{..<halted_point} ∖ 𝒟. h (Suc i) - h (i-1)) ≤ ok_fun_26 k"
and 28: "ok_fun_28 k ≤ (∑i ∈ ℬ. h(Suc i) - h(i-1))"
using X_26_and_28 big unfolding ℬ_def 𝒟_def h_def Big_X_7_10_def by blast
have "(∑i∈ℛ∪𝒮. h (Suc i) - h (i-1)) = (∑i∈{..<halted_point} ∖ 𝒟. h (Suc i) - h (i-1)) - (∑i ∈ ℬ. h(Suc i) - h(i-1))"
unfolding RS_eq by (intro sum_diff BmD) auto
also have "… ≤ ok_fun_26 k - ok_fun_28 k"
using 26 28 by linarith
finally have *: "(∑i∈ℛ∪𝒮. h (Suc i) - h (i-1)) ≤ ok_fun_26 k - ok_fun_28 k" .
have [simp]: "finite ℛ" "finite 𝒮"
using finite_components by (auto simp: ℛ_def 𝒮_def)
have h_ge_0_if_S: "h(Suc i) - h(i-1) ≥ 0" if "i ∈ 𝒮" for i
proof -
have *: "hgt (pseq i) ≤ hgt (pseq (Suc i))"
using bigR53 Y_6_5_dbooSt that unfolding 𝒮_def by blast
obtain "i-1 ∈ 𝒟" "i>0"
using that ‹i∈𝒮› dreg_before_step1[of i] dreg_before_gt0[of i]
by (force simp: 𝒮_def 𝒟_def Step_class_insert_NO_MATCH)
then have "hgt (pseq (i-1)) ≤ hgt (pseq i)"
using that kn0 by (metis Suc_diff_1 Y_6_5_DegreeReg 𝒟_def)
with * show "0 ≤ h(Suc i) - h(i-1)"
using kn0 unfolding h_def by linarith
qed
have "card ((ℛ∪𝒮) ∩ C) * ε powr (-1/4) + real (card ℛ) * (-2)
= (∑i ∈ ℛ∪𝒮. if i∈C then ε powr (-1/4) else 0) + (∑i ∈ ℛ∪𝒮. if i∈ℛ then -2 else 0)"
by (simp add: Int_commute Int_left_commute flip: sum.inter_restrict)
also have "… = (∑i ∈ ℛ∪𝒮. (if i∈C then ε powr (-1/4) else 0) + (if i∈ℛ then -2 else 0))"
by (simp add: sum.distrib)
also have "… ≤ (∑i ∈ ℛ∪𝒮. h(Suc i) - h(i-1))"
proof (rule sum_mono)
fix i :: nat
assume i: "i ∈ ℛ∪𝒮"
with i dreg_before_step1 dreg_before_gt0 have D: "i-1 ∈ 𝒟" "i>0"
by (force simp: 𝒮_def ℛ_def 𝒟_def dreg_before_step Step_class_def)+
then have *: "hgt (pseq (i-1)) ≤ hgt (pseq i)"
by (metis Suc_diff_1 Y_6_5_DegreeReg 𝒟_def)
show "(if i∈C then ε powr (-1/4) else 0) + (if i∈ℛ then - 2 else 0) ≤ h (Suc i) - h (i-1)"
proof (cases "i∈ℛ")
case True
then have "h i - 2 ≤ h (Suc i)"
using Y_6_5_Red[of i] 16 by (force simp: algebra_simps ℛ_def h_def)
with * True show ?thesis
by (simp add: h_def C_def)
next
case False
with i have "i∈𝒮" by blast
show ?thesis
proof (cases "i∈C")
case True
then have "h (i - Suc 0) + ε powr (-1/4) ≤ h i"
by (simp add: C_def)
then show ?thesis
using * i ‹i∉ℛ› kn0 bigR53 Y_6_5_dbooSt by (force simp: h_def 𝒮_def)
qed (use ‹i∉ℛ› ‹i∈𝒮› h_ge_0_if_S in auto)
qed
qed
also have "… ≤ k"
using * ok_le_k
by linarith
finally have "card ((ℛ∪𝒮) ∩ C) * ε powr (-1/4) - 2 * card ℛ ≤ k"
by linarith
moreover have "card ℛ ≤ k"
by (metis ℛ_def nless_le red_step_limit)
ultimately have "card ((ℛ∪𝒮) ∩ C) * ε powr (-1/4) ≤ 3 * k"
by linarith
with eps_gt0 show ?thesis
by (simp add: powr_minus divide_simps mult.commute split: if_split_asm)
qed
subsection ‹Lemma 7.11›
definition "Big_X_7_11_inequalities ≡ λk.
eps k * eps k powr (-1/4) ≤ (1 + eps k) ^ (2 * nat ⌊eps k powr (-1/4)⌋) - 1
∧ k ≥ 2 * eps k powr (-1/2) * k powr (3/4)
∧ ((1 + eps k) * (1 + eps k) powr (2 * eps k powr (-1/4))) ≤ 2
∧ (1 + eps k) ^ (nat ⌊2 * eps k powr (-1/4)⌋ + nat ⌊2 * eps k powr (-1/2)⌋ - 1) ≤ 2"
definition "Big_X_7_11 ≡
λμ l. Big_X_7_5 μ l ∧ Big_Red_5_3 μ l ∧ Big_Y_6_5_Bblue l
∧ (∀k. l≤k ⟶ Big_X_7_11_inequalities k)"
text ‹establishing the size requirements for 7.11›
lemma Big_X_7_11:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_11 μ l"
using assms Big_Red_5_3 Big_X_7_5 Big_Y_6_5_Bblue
unfolding Big_X_7_11_def Big_X_7_11_inequalities_def eventually_conj_iff all_imp_conj_distrib eps_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib)
apply (intro conjI strip eventually_all_geI0 eventually_all_ge_at_top; real_asymp)
done
lemma (in Book) X_7_11:
defines "ℛ ≡ Step_class {red_step}"
defines "𝒮 ≡ Step_class {dboost_step}"
defines "C ≡ {i. pseq i ≥ pseq (i-1) + ε powr (-1/4) * alpha 1 ∧ pseq (i-1) ≤ p0}"
assumes big: "Big_X_7_11 μ l"
shows "card ((ℛ∪𝒮) ∩ C) ≤ 4 * ε powr (1/4) * k"
proof -
define qstar where "qstar ≡ p0 + ε powr (-1/4) * alpha 1"
define pstar where "pstar ≡ λi. min (pseq i) qstar"
define 𝒟 where "𝒟 ≡ Step_class {dreg_step}"
define ℬ where "ℬ ≡ Step_class {bblue_step}"
have big_x75: "Big_X_7_5 μ l"
and 711: "ε * ε powr (-1/4) ≤ (1 + ε) ^ (2 * nat ⌊ε powr (-1/4)⌋) - 1"
and big34: "k ≥ 2 * ε powr (-1/2) * k powr (3/4)"
and le2: "((1 + ε) * (1 + ε) powr (2 * ε powr (-1/4))) ≤ 2"
"(1 + ε) ^ (nat ⌊2 * ε powr (-1/4)⌋ + nat ⌊2 * ε powr (-1/2)⌋ - 1) ≤ 2"
and bigY65B: "Big_Y_6_5_Bblue l"
and R53: "⋀i. i ∈ 𝒮 ⟹ pseq (Suc i) ≥ pseq i"
using big l_le_k
by (auto simp: Red_5_3 Big_X_7_11_def Big_X_7_11_inequalities_def 𝒮_def)
then have Y_6_5_B: "⋀i. i ∈ ℬ ⟹ hgt (pseq (Suc i)) ≥ hgt (pseq (i-1)) - 2 * ε powr (-1/2)"
using bigY65B Y_6_5_Bblue unfolding ℬ_def by blast
have big41: "Big_Blue_4_1 μ l"
and hub: "Big_height_upper_bound k"
and 16: "k≥16"
and ok_le_k: "ok_fun_26 k - ok_fun_28 k ≤ k"
using big_x75 l_le_k by (auto simp: Big_X_7_5_def)
have oddset: "{..<halted_point} ∖ 𝒟 = {i ∈ {..<halted_point}. odd i}"
using step_odd step_even not_halted_even_dreg halted_point_minimal by (auto simp: 𝒟_def)
have [simp]: "finite ℛ" "finite ℬ" "finite 𝒮"
using finite_components by (auto simp: ℛ_def ℬ_def 𝒮_def)
have [simp]: "ℛ ∩ 𝒮 = {}" and [simp]: "(ℛ ∪ 𝒮) ∩ ℬ = {}"
by (simp_all add: ℛ_def 𝒮_def ℬ_def Step_class_def disjoint_iff)
have hgt_qstar_le: "hgt qstar ≤ 2 * ε powr (-1/4)"
proof (intro real_hgt_Least)
show "0 < 2 * nat ⌊ε powr (-1/4)⌋"
using kn0 eps_gt0 by (simp add: eps_le1 powr_le1 powr_minus_divide)
show "qstar ≤ qfun (2 * nat ⌊ε powr (-1/4)⌋)"
using kn0 711
by (simp add: qstar_def alpha_def qfun_eq divide_right_mono mult.commute)
qed auto
then have "((1 + ε) * (1 + ε) ^ hgt qstar) ≤ ((1 + ε) * (1 + ε) powr (2 * ε powr (-1/4)))"
by (smt (verit) eps_ge0 mult_left_mono powr_mono powr_realpow)
also have "((1 + ε) * (1 + ε) powr (2 * ε powr (-1/4))) ≤ 2"
using le2 by simp
finally have "(1 + ε) * (1 + ε) ^ hgt qstar ≤ 2" .
moreover have "card ℛ ≤ k"
by (simp add: ℛ_def less_imp_le red_step_limit)
ultimately have §: "((1 + ε) * (1 + ε) ^ hgt qstar) * card ℛ ≤ 2 * real k"
by (intro mult_mono) auto
have "- 2 * alpha 1 * k ≤ - alpha (hgt qstar + 2) * card ℛ"
using mult_right_mono_neg [OF §, of "- ε"] eps_ge0
by (simp add: alpha_eq divide_simps mult_ac)
also have "… ≤ (∑i∈ℛ. pstar (Suc i) - pstar i)"
proof -
{ fix i
assume "i ∈ ℛ"
have "- alpha (hgt qstar + 2) ≤ pstar (Suc i) - pstar i"
proof (cases "hgt (pseq i) > hgt qstar + 2")
case True
then have "hgt (pseq (Suc i)) > hgt qstar"
using Y_6_5_Red 16 ‹i ∈ ℛ› by (force simp: ℛ_def)
then have "pstar (Suc i) = pstar i"
using True hgt_mono' pstar_def by fastforce
then show ?thesis
by (simp add: alpha_ge0)
next
case False
with ‹i ∈ ℛ› show ?thesis
unfolding pstar_def ℛ_def
by (smt (verit, del_insts) Y_6_4_Red alpha_ge0 alpha_mono hgt_gt0 linorder_not_less)
qed
}
then show ?thesis
by (smt (verit, ccfv_SIG) mult_of_nat_commute sum_constant sum_mono)
qed
finally have "- 2 * alpha 1 * k ≤ (∑i∈ℛ. pstar (Suc i) - pstar i)" .
moreover have "0 ≤ (∑i∈𝒮. pstar (Suc i) - pstar i)"
using R53 by (intro sum_nonneg) (force simp: pstar_def)
ultimately have RS_half: "- 2 * alpha 1 * k ≤ (∑i∈ℛ∪𝒮. pstar (Suc i) - pstar i)"
by (simp add: sum.union_disjoint)
let ?e12 = "ε powr (-1/2)"
define h' where "h' ≡ hgt qstar + nat ⌊2 * ?e12⌋"
have "- alpha 1 * k ≤ -2 * ?e12 * alpha 1 * k powr (3/4)"
using mult_right_mono_neg [OF big34, of "- alpha 1"] alpha_ge0 [of 1]
by (simp add: mult_ac)
also have "… ≤ -?e12 * alpha (h') * card ℬ"
proof -
have "card ℬ ≤ l powr (3/4)"
using big41 bblue_step_limit by (simp add: ℬ_def)
also have "… ≤ k powr (3/4)"
by (simp add: powr_mono2 l_le_k)
finally have 1: "card ℬ ≤ k powr (3/4)" .
have "alpha (h') ≤ alpha (nat ⌊2 * ε powr (-1/4)⌋ + nat ⌊2 * ?e12⌋)"
proof (rule alpha_mono)
show "h' ≤ nat ⌊2 * ε powr (-1/4)⌋ + nat ⌊2 * ?e12⌋"
using h'_def hgt_qstar_le le_nat_floor by auto
qed (simp add: hgt_gt0 h'_def)
also have "… ≤ 2 * alpha 1"
proof -
have *: "(1 + ε) ^ (nat ⌊2 * ε powr (-1/4)⌋ + nat ⌊2 * ?e12⌋ - 1) ≤ 2"
using le2 by simp
have "1 ≤ 2 * ε powr (-1/4)"
by (smt (verit) hgt_qstar_le Suc_leI divide_minus_left hgt_gt0 numeral_nat(7) real_of_nat_ge_one_iff)
then show ?thesis
using mult_right_mono [OF *, of "ε"] eps_ge0
by (simp add: alpha_eq hgt_gt0 divide_right_mono mult.commute)
qed
finally have 2: "2 * alpha 1 ≥ alpha (h')" .
show ?thesis
using mult_right_mono_neg [OF mult_mono [OF 1 2], of "-?e12"] alpha_ge0 by (simp add: mult_ac)
qed
also have "… ≤ (∑i∈ℬ. pstar (Suc i) - pstar (i-1))"
proof -
{ fix i
assume "i ∈ ℬ"
have "-?e12 * alpha (h') ≤ pstar (Suc i) - pstar (i-1)"
proof (cases "hgt (pseq (i-1)) > hgt qstar + 2 * ?e12")
case True
then have "hgt (pseq (Suc i)) > hgt qstar"
using Y_6_5_B ‹i ∈ ℬ› by (force simp: ℛ_def)
then have "pstar (i-1) = pstar(Suc i)"
unfolding pstar_def
by (smt (verit) True hgt_mono' of_nat_less_iff powr_non_neg)
then show ?thesis
by (simp add: alpha_ge0)
next
case False
then have "hgt (pseq (i-1)) ≤ h'"
by (simp add: h'_def) linarith
then have †: "alpha (hgt (pseq (i-1))) ≤ alpha h'"
by (intro alpha_mono hgt_gt0)
have "pseq (Suc i) ≥ pseq (i-1) - ?e12 * alpha (hgt (pseq (i-1)))"
using Y_6_4_Bblue ‹i ∈ ℬ› unfolding ℬ_def by blast
with mult_left_mono [OF †, of ?e12] show ?thesis
unfolding pstar_def
by (smt (verit) alpha_ge0 mult_minus_left powr_non_neg mult_le_0_iff)
qed
}
then show ?thesis
by (smt (verit, ccfv_SIG) mult_of_nat_commute sum_constant sum_mono)
qed
finally have B: "- alpha 1 * k ≤ (∑i∈ℬ. pstar (Suc i) - pstar (i-1))" .
have "ε powr (-1/4) * alpha 1 * card ((ℛ∪𝒮) ∩ C) ≤ (∑i∈ℛ∪𝒮. if i ∈ C then ε powr (-1/4) * alpha 1 else 0)"
by (simp add: flip: sum.inter_restrict)
also have "(∑i∈ℛ∪𝒮. if i ∈ C then ε powr (-1/4) * alpha 1 else 0) ≤ (∑i∈ℛ∪𝒮. pstar i - pstar (i-1))"
proof (intro sum_mono)
fix i
assume i: "i ∈ ℛ ∪ 𝒮"
then obtain "i-1 ∈ 𝒟" "i>0"
unfolding ℛ_def 𝒮_def 𝒟_def by (metis dreg_before_step1 dreg_before_gt0 Step_class_insert Un_iff)
then have "pseq (i-1) ≤ pseq i"
by (metis Suc_pred' Y_6_4_DegreeReg 𝒟_def)
then have "pstar (i-1) ≤ pstar i"
by (fastforce simp: pstar_def)
then show "(if i ∈ C then ε powr (-1/4) * alpha 1 else 0) ≤ pstar i - pstar (i-1)"
using C_def pstar_def qstar_def by auto
qed
finally have §: "ε powr (-1/4) * alpha 1 * card ((ℛ∪𝒮) ∩ C) ≤ (∑i∈ℛ∪𝒮. pstar i - pstar (i-1))" .
have psplit: "pstar (Suc i) - pstar (i-1) = (pstar (Suc i) - pstar i) + (pstar i - pstar (i-1))" for i
by simp
have RS: "ε powr (-1/4) * alpha 1 * card ((ℛ∪𝒮) ∩ C) + (- 2 * alpha 1 * k) ≤ (∑i∈ℛ∪𝒮. pstar (Suc i) - pstar (i-1))"
unfolding psplit sum.distrib using RS_half § by linarith
have k16: "k powr (1/16) ≤ k powr 1"
using kn0 by (intro powr_mono) auto
have meq: "{..<halted_point} ∖ 𝒟 = (ℛ∪𝒮) ∪ ℬ"
using Step_class_cases halted_point_minimal' by(fastforce simp: ℛ_def 𝒮_def 𝒟_def ℬ_def Step_class_def)
have "(ε powr (-1/4) * alpha 1 * card ((ℛ∪𝒮) ∩ C) + (- 2 * alpha 1 * k))
+ (- alpha 1 * k)
≤ (∑i ∈ ℛ∪𝒮. pstar(Suc i) - pstar(i-1)) + (∑i∈ℬ. pstar(Suc i) - pstar(i-1))"
using RS B by linarith
also have "… = (∑i ∈ {..<halted_point} ∖ 𝒟. pstar(Suc i) - pstar(i-1))"
by (simp add: meq sum.union_disjoint)
also have "… ≤ pstar halted_point - pstar 0"
proof (cases "even halted_point")
case False
have "pseq (halted_point - Suc 0) ≤ pseq halted_point"
using Y_6_4_DegreeReg [of "halted_point-1"] False not_halted_even_dreg odd_pos
by (auto simp: halted_point_minimal)
then have "pstar(halted_point - Suc 0) ≤ pstar halted_point"
by (simp add: pstar_def)
with False show ?thesis
by (simp add: oddset sum_odds_odd)
qed (simp add: oddset sum_odds_even)
also have "… = (∑i < halted_point. pstar(Suc i) - pstar i)"
by (simp add: sum_lessThan_telescope)
also have "… = pstar halted_point - pstar 0"
by (simp add: sum_lessThan_telescope)
also have "… ≤ alpha 1 * ε powr (-1/4)"
using alpha_ge0 by (simp add: mult.commute pee_eq_p0 pstar_def qstar_def)
also have "… ≤ alpha 1 * k"
using alpha_ge0 k16 by (intro powr_mono mult_left_mono) (auto simp: eps_def powr_powr)
finally have "ε powr (-1/4) * card ((ℛ ∪ 𝒮) ∩ C) * alpha 1 ≤ 4 * k * alpha 1"
by (simp add: mult_ac)
then have "ε powr (-1/4) * real (card ((ℛ ∪ 𝒮) ∩ C)) ≤ 4 * k"
using kn0 by (simp add: divide_simps alpha_eq eps_gt0)
then show ?thesis
using alpha_ge0[of 1] kn0 eps_gt0 by (simp add: powr_minus divide_simps mult_ac split: if_split_asm)
qed
subsection ‹Lemma 7.12›
definition "Big_X_7_12 ≡
λμ l. Big_X_7_11 μ l ∧ Big_X_7_10 μ l ∧ (∀k. l≤k ⟶ Big_X_7_9 k)"
text ‹establishing the size requirements for 7.12›
lemma Big_X_7_12:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_12 μ l"
using assms Big_X_7_11 Big_X_7_10 Big_X_7_9
unfolding Big_X_7_12_def eventually_conj_iff
apply (simp add: eventually_conj_iff all_imp_conj_distrib eventually_frequently_const_simps)
using eventually_all_ge_at_top by blast
lemma (in Book) X_7_12:
defines "ℛ ≡ Step_class {red_step}"
defines "𝒮 ≡ Step_class {dboost_step}"
defines "C ≡ {i. card (Xseq i) < (1 - 2 * ε powr (1/4)) * card (Xseq (i-1))}"
assumes big: "Big_X_7_12 μ l"
shows "card ((ℛ∪𝒮) ∩ C) ≤ 7 * ε powr (1/4) * k"
proof -
define 𝒟 where "𝒟 ≡ Step_class {dreg_step}"
have big_711: "Big_X_7_11 μ l" and big_710: "Big_X_7_10 μ l"
using big by (auto simp: Big_X_7_12_def)
have [simp]: "finite ℛ" "finite 𝒮"
using finite_components by (auto simp: ℛ_def 𝒮_def)
define C10 where "C10 ≡ {i. hgt (pseq i) ≥ hgt (pseq (i-1)) + ε powr (-1/4)}"
define C11 where "C11 ≡ {i. pseq i ≥ pseq (i-1) + ε powr (-1/4) * alpha 1 ∧ pseq (i-1) ≤ p0}"
have "(ℛ∪𝒮) ∩ C ∩ {i. pseq (i-1) ≤ p0} ⊆ (ℛ∪𝒮) ∩ C11"
proof
fix i
assume i: "i ∈ (ℛ∪𝒮) ∩ C ∩ {i. pseq (i-1) ≤ p0}"
then have iRS: "i ∈ ℛ ∪ 𝒮" and iC: "i ∈ C"
by auto
then obtain i1: "i-1 ∈ 𝒟" "i>0"
unfolding ℛ_def 𝒮_def 𝒟_def by (metis Step_class_insert Un_iff dreg_before_step1 dreg_before_gt0)
then have 77: "card (Xseq (i-1) ∖ Xseq i) / card (Xseq i) * (ε powr (-1/2) * alpha (hgt (pseq (i-1))))
≤ pseq i - pseq (i-1)"
by (metis Suc_diff_1 X_7_7 𝒟_def)
have card_Xm1: "card (Xseq (i-1)) = card (Xseq i) + card (Xseq (i-1) ∖ Xseq i)"
by (metis Xseq_antimono add_diff_inverse_nat card_Diff_subset card_mono diff_le_self
finite_Xseq linorder_not_less)
have "card (Xseq i) > 0"
by (metis Step_class_insert card_Xseq_pos ℛ_def 𝒮_def iRS)
have "card (Xseq (i-1)) > 0"
using C_def iC less_irrefl by fastforce
moreover have "2 * (card (Xseq (i-1)) * ε powr (1/4)) < card (Xseq (i-1) ∖ Xseq i)"
using iC card_Xm1 by (simp add: algebra_simps C_def)
moreover have "card (Xseq i) ≤ 2 * card (Xseq (i-1))"
using card_Xm1 by linarith
ultimately have "ε powr (1/4) ≤ card (Xseq (i-1) ∖ Xseq i) / card (Xseq (i-1))"
by (simp add: divide_simps mult.commute)
moreover have "real (card (Xseq i)) ≤ card (Xseq (i-1))"
using card_Xm1 by linarith
ultimately have 1: "ε powr (1/4) ≤ card (Xseq (i-1) ∖ Xseq i) / card (Xseq i)"
by (smt (verit) ‹0 < card (Xseq i)› frac_le of_nat_0_le_iff of_nat_0_less_iff)
have "ε powr (-1/4) * alpha 1
≤ card (Xseq (i-1) ∖ Xseq i) / card (Xseq i) * (ε powr (-1/2) * alpha 1)"
using alpha_ge0 mult_right_mono [OF 1, of "ε powr (-1/2) * alpha 1"]
by (simp add: mult_ac flip: powr_add)
also have "… ≤ card (Xseq (i-1) ∖ Xseq i) / card (Xseq i) * (ε powr (-1/2) * alpha (hgt (pseq (i-1))))"
by (intro mult_left_mono alpha_mono) (auto simp: Suc_leI hgt_gt0)
also have "… ≤ pseq i - pseq (i-1)"
using 77 by simp
finally have "ε powr (-1/4) * alpha 1 ≤ pseq i - pseq (i-1)" .
with i show "i ∈ (ℛ ∪ 𝒮) ∩ C11"
by (simp add: C11_def)
qed
then have "real (card ((ℛ∪𝒮) ∩ C ∩ {i. pseq (i-1) ≤ p0})) ≤ real (card ((ℛ∪𝒮) ∩ C11))"
by (simp add: card_mono)
also have "… ≤ 4 * ε powr (1/4) * k"
using X_7_11 big_711 by (simp add: ℛ_def 𝒮_def C11_def Step_class_insert_NO_MATCH)
finally have "card ((ℛ∪𝒮) ∩ C ∩ {i. pseq (i-1) ≤ p0}) ≤ 4 * ε powr (1/4) * k" .
moreover
have "card ((ℛ∪𝒮) ∩ C ∖ {i. pseq (i-1) ≤ p0}) ≤ 3 * ε powr (1/4) * k"
proof -
have "Big_X_7_9 k"
using Big_X_7_12_def big l_le_k by presburger
then have X79: "card (Xseq (Suc i)) ≥ (1 - 2 * ε powr (1/4)) * card (Xseq i)"
if "i ∈ Step_class {dreg_step}" and "pseq i ≥ p0"
and "hgt (pseq (Suc i)) ≤ hgt (pseq i) + ε powr (-1/4)" for i
using X_7_9 that by blast
have "(ℛ∪𝒮) ∩ C ∖ {i. pseq (i-1) ≤ p0} ⊆ (ℛ∪𝒮) ∩ C10"
unfolding C10_def C_def
proof clarify
fix i
assume "i ∈ ℛ ∪ 𝒮"
and §: "card (Xseq i) < (1 - 2 * ε powr (1/4)) * card (Xseq (i-1))" "¬ pseq (i-1) ≤ p0"
then obtain "i-1 ∈ 𝒟" "i>0"
unfolding 𝒟_def ℛ_def 𝒮_def
by (metis dreg_before_step1 dreg_before_gt0 Step_class_Un Un_iff insert_is_Un)
with X79 § show "hgt (pseq (i - 1)) + ε powr (-1/4) ≤ hgt (pseq i)"
by (force simp: 𝒟_def)
qed
then have "card ((ℛ∪𝒮) ∩ C ∖ {i. pseq (i-1) ≤ p0}) ≤ real (card ((ℛ∪𝒮) ∩ C10))"
by (simp add: card_mono)
also have "card ((ℛ∪𝒮) ∩ C10) ≤ 3 * ε powr (1/4) * k"
unfolding ℛ_def 𝒮_def C10_def by (intro X_7_10 assms big_710)
finally show ?thesis .
qed
moreover
have "card ((ℛ∪𝒮) ∩ C)
= real (card ((ℛ∪𝒮) ∩ C ∩ {i. pseq (i-1) ≤ p0})) + real (card ((ℛ∪𝒮) ∩ C ∖ {i. pseq (i-1) ≤ p0}))"
by (metis card_Int_Diff of_nat_add ‹finite ℛ› ‹finite 𝒮› finite_Int infinite_Un)
ultimately show ?thesis
by linarith
qed
subsection ‹Lemma 7.6›
definition "Big_X_7_6 ≡
λμ l. Big_Blue_4_1 μ l ∧ Big_X_7_12 μ l ∧ (∀k. k≥l ⟶ Big_X_7_8 k ∧ 1 - 2 * eps k powr (1/4) > 0)"
lemma Big_X_7_6:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_6 μ l"
using assms Big_Blue_4_1 Big_X_7_8 Big_X_7_12
unfolding Big_X_7_6_def eps_def
apply (simp add: eventually_conj_iff all_imp_conj_distrib eventually_all_ge_at_top)
apply (intro conjI strip eventually_all_geI0 eventually_all_ge_at_top; real_asymp)
done
definition "ok_fun_76 ≡
λk. ((1 + 2 * real k) * ln (1 - 2 * eps k powr (1/4))
- (k powr (3/4) + 7 * eps k powr (1/4) * k + 1) * (2 * ln k)) / ln 2"
lemma ok_fun_76: "ok_fun_76 ∈ o(real)"
unfolding eps_def ok_fun_76_def by real_asymp
lemma (in Book) X_7_6:
assumes big: "Big_X_7_6 μ l"
defines "𝒟 ≡ Step_class {dreg_step}"
shows "(∏i∈𝒟. card(Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr ok_fun_76 k"
proof -
define ℛ where "ℛ ≡ Step_class {red_step}"
define ℬ where "ℬ ≡ Step_class {bblue_step}"
define 𝒮 where "𝒮 ≡ Step_class {dboost_step}"
define C where "C ≡ {i. card (Xseq i) < (1 - 2 * ε powr (1/4)) * card (Xseq (i-1))}"
define C' where "C' ≡ Suc -` C"
have big41: "Big_Blue_4_1 μ l"
and 712: "card ((ℛ∪𝒮) ∩ C) ≤ 7 * ε powr (1/4) * k"
using big X_7_12 l_le_k by (auto simp: Big_X_7_6_def ℛ_def 𝒮_def C_def)
have [simp]: "finite 𝒟" "finite ℛ" "finite ℬ" "finite 𝒮"
using finite_components by (auto simp: 𝒟_def ℛ_def ℬ_def 𝒮_def)
have "card ℛ < k"
using ℛ_def assms red_step_limit by blast+
have "card ℬ ≤ l powr (3/4)"
using big41 bblue_step_limit by (auto simp: ℬ_def)
then have "card (ℬ ∩ C) ≤ l powr (3/4)"
using card_mono [OF _ Int_lower1] by (smt (verit) ‹finite ℬ› of_nat_mono)
also have "… ≤ k powr (3/4)"
by (simp add: l_le_k powr_mono2)
finally have Bk_34: "card (ℬ ∩ C) ≤ k powr (3/4)" .
have less_l: "card ℬ + card 𝒮 < l"
using bblue_dboost_step_limit big41 by (auto simp: ℬ_def 𝒮_def)
have [simp]: "(ℬ ∪ (ℛ ∪ 𝒮)) ∩ {halted_point} = {}" "ℛ ∩ 𝒮 = {}" "ℬ ∩ (ℛ ∪ 𝒮) = {}"
"halted_point ∉ ℬ" "halted_point ∉ ℛ" "halted_point ∉ 𝒮"
"ℬ ∩ C ∩ (ℛ ∩ C ∪ 𝒮 ∩ C) = {}" for C
using halted_point_minimal' by (force simp: ℬ_def ℛ_def 𝒮_def Step_class_def)+
have "Big_X_7_8 k" and one_minus_gt0: "1 - 2 * ε powr (1/4) > 0"
using big l_le_k by (auto simp: Big_X_7_6_def)
then have X78: "card (Xseq (Suc i)) ≥ card (Xseq i) / k^2" if "i ∈ 𝒟" for i
using X_7_8 that by (force simp: 𝒟_def)
let ?DC = "λk. k powr (3/4) + 7 * eps k powr (1/4) * k + 1"
have dc_pos: "?DC k > 0" for k
by (smt (verit) of_nat_less_0_iff powr_ge_zero zero_le_mult_iff)
have X_pos: "card (Xseq i) > 0" if "i ∈ 𝒟" for i
proof -
have "card (Xseq (Suc i)) > 0"
using that X_7_7 kn0 unfolding 𝒟_def by blast
then show ?thesis
by (metis Xseq_Suc_subset card_mono finite_Xseq gr0I leD)
qed
have "ok_fun_76 k ≤ log 2 ((1 / (real k)⇧2) powr ?DC k * (1 - 2 * ε powr (1/4)) ^ (k + l + 1))"
unfolding ok_fun_76_def log_def
using kn0 l_le_k one_minus_gt0
by (simp add: ln_mult ln_div ln_realpow divide_right_mono mult_le_cancel_right flip: power_Suc mult.assoc)
then have "2 powr ok_fun_76 k ≤ (1 / (real k)⇧2) powr ?DC k * (1 - 2 * ε powr (1/4)) ^ (k + l + 1)"
using powr_eq_iff kn0 one_minus_gt0 by (simp add: le_log_iff)
also have "… ≤ (1 / (real k)⇧2) powr card (𝒟 ∩ C') * (1 - 2 * ε powr (1/4)) ^ card (𝒟∖C')"
proof (intro mult_mono powr_mono')
have "Suc i ∈ ℛ" if "i ∈ 𝒟" "Suc i ≠ halted_point" "Suc i ∉ ℬ" "Suc i ∉ 𝒮" for i
proof -
have "Suc i ∉ 𝒟"
by (metis 𝒟_def ‹i ∈ 𝒟› even_Suc step_even)
moreover
have "stepper_kind i ≠ halted"
using 𝒟_def ‹i ∈ 𝒟› Step_class_def by force
ultimately show "Suc i ∈ ℛ"
using that halted_point_minimal' halted_point_minimal Step_class_cases Suc_lessI
ℬ_def 𝒟_def ℛ_def 𝒮_def by blast
qed
then have "Suc ` 𝒟 ⊆ ℬ ∪ (ℛ ∪ 𝒮) ∪ {halted_point}"
by auto
then have ifD: "Suc i ∈ ℬ ∨ Suc i ∈ ℛ ∨ Suc i ∈ 𝒮 ∨ Suc i = halted_point" if "i ∈ 𝒟" for i
using that by force
then have "card 𝒟 ≤ card (ℬ ∪ (ℛ∪𝒮) ∪ {halted_point})"
by (intro card_inj_on_le [of Suc]) auto
also have "… = card ℬ + card ℛ + card 𝒮 + 1"
by (simp add: card_Un_disjoint card_insert_if)
also have "… ≤ k + l + 1"
using ‹card ℛ < k› less_l by linarith
finally have card_D: "card 𝒟 ≤ k + l + 1" .
have "(1 - 2 * ε powr (1/4)) * card (Xseq 0) ≤ 1 * real (card (Xseq 0))"
by (intro mult_right_mono; force)
then have "0 ∉ C"
by (force simp: C_def)
then have C_eq_C': "C = Suc ` C'"
using nat.exhaust by (auto simp: C'_def set_eq_iff image_iff)
have "card (𝒟 ∩ C') ≤ real (card ((ℬ ∪ (ℛ∪𝒮) ∪ {halted_point}) ∩ C))"
using ifD
by (intro of_nat_mono card_inj_on_le [of Suc]) (force simp: Int_insert_left C_eq_C')+
also have "… ≤ card (ℬ ∩ C) + real (card ((ℛ∪𝒮) ∩ C)) + 1"
by (simp add: Int_insert_left Int_Un_distrib2 card_Un_disjoint card_insert_if)
also have "… ≤ ?DC k"
using Bk_34 712 by force
finally show "card (𝒟 ∩ C') ≤ ?DC k" .
have "card (𝒟∖C') ≤ card 𝒟"
using ‹finite 𝒟› by (simp add: card_mono)
then show "(1 - 2 * ε powr (1/4)) ^ (k+l+1) ≤ (1 - 2 * ε powr (1/4)) ^ card (𝒟∖C')"
by (smt (verit) card_D add_leD2 one_minus_gt0 power_decreasing powr_ge_zero)
qed (use one_minus_gt0 kn0 in auto)
also have "… = (∏i∈𝒟. if i ∈ C' then 1 / real k ^ 2 else 1 - 2 * ε powr (1/4))"
by (simp add: kn0 powr_realpow prod.If_cases Diff_eq)
also have "… ≤ (∏i ∈ 𝒟. card (Xseq (Suc i)) / card (Xseq i))"
using X_pos X78 one_minus_gt0 kn0 by (simp add: divide_simps C'_def C_def prod_mono)
finally show ?thesis .
qed
subsection ‹Lemma 7.1›
definition "Big_X_7_1 ≡
λμ l. Big_Blue_4_1 μ l ∧ Big_X_7_2 μ l ∧ Big_X_7_4 μ l ∧ Big_X_7_6 μ l"
text ‹establishing the size requirements for 7.11›
lemma Big_X_7_1:
assumes "0<μ0" "μ1<1"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_X_7_1 μ l"
unfolding Big_X_7_1_def
using assms Big_Blue_4_1 Big_X_7_2 Big_X_7_4 Big_X_7_6
by (simp add: eventually_conj_iff all_imp_conj_distrib)
definition "ok_fun_71 ≡ λμ k. ok_fun_72 μ k + ok_fun_73 k + ok_fun_74 k + ok_fun_76 k"
lemma ok_fun_71:
assumes "0<μ" "μ<1"
shows "ok_fun_71 μ ∈ o(real)"
using ok_fun_72 ok_fun_73 ok_fun_74 ok_fun_76
by (simp add: assms ok_fun_71_def sum_in_smallo)
lemma (in Book) X_7_1:
assumes big: "Big_X_7_1 μ l"
defines "𝒟 ≡ Step_class {dreg_step}"
defines "ℛ ≡ Step_class {red_step}" and "𝒮 ≡ Step_class {dboost_step}"
shows "card (Xseq halted_point) ≥
2 powr ok_fun_71 μ k * μ^l * (1-μ) ^ card ℛ * (bigbeta / μ) ^ card 𝒮 * card X0"
proof -
define ℬ where "ℬ ≡ Step_class {bblue_step}"
have 72: "Big_X_7_2 μ l" and 74: "Big_X_7_4 μ l"
and 76: "Big_X_7_6 μ l"
and big41: "Big_Blue_4_1 μ l"
using big by (auto simp: Big_X_7_1_def)
then have [simp]: "finite ℛ" "finite ℬ" "finite 𝒮" "finite 𝒟"
"ℛ∩ℬ = {}" "𝒮∩𝒟 = {}" "(ℛ∪ℬ)∩(𝒮∪𝒟) = {}"
using finite_components by (auto simp: ℛ_def ℬ_def 𝒮_def 𝒟_def Step_class_def)
have BS_le_l: "card ℬ + card 𝒮 < l"
using big41 bblue_dboost_step_limit by (auto simp: 𝒮_def ℬ_def)
have R: "(∏i∈ℛ. card (Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr (ok_fun_72 μ k) * (1-μ) ^ card ℛ"
unfolding ℛ_def using 72 X_7_2 by meson
have B: "(∏i∈ℬ. card (Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr (ok_fun_73 k) * μ ^ (l - card 𝒮)"
unfolding ℬ_def 𝒮_def using big41 X_7_3 by meson
have S: "(∏i∈𝒮. card (Xseq (Suc i)) / card (Xseq i)) ≥ 2 powr ok_fun_74 k * bigbeta ^ card 𝒮"
unfolding 𝒮_def using 74 X_7_4 by meson
have D: "(∏i∈𝒟. card(Xseq(Suc i)) / card (Xseq i)) ≥ 2 powr ok_fun_76 k"
unfolding 𝒟_def using 76 X_7_6 by meson
have below_m: "ℛ∪ℬ∪𝒮∪𝒟 = {..<halted_point}"
using assms by (auto simp: ℛ_def ℬ_def 𝒮_def 𝒟_def before_halted_eq Step_class_insert_NO_MATCH)
have X_nz: "⋀i. i < halted_point ⟹ card (Xseq i) ≠ 0"
using assms below_halted_point_cardX by blast
have tele: "card (Xseq halted_point) = (∏i < halted_point. card (Xseq(Suc i)) / card (Xseq i)) * card (Xseq 0)"
proof (cases "halted_point=0")
case False
with X_nz prod_lessThan_telescope_mult [where f = "λi. real (card (Xseq i))"]
show ?thesis by simp
qed auto
have X0_nz: "card (Xseq 0) > 0"
by (simp add: card_XY0)
have "2 powr ok_fun_71 μ k * μ^l * (1-μ) ^ card ℛ * (bigbeta / μ) ^ card 𝒮
≤ 2 powr ok_fun_71 μ k * μ ^ (l - card 𝒮) * (1-μ) ^ card ℛ * (bigbeta ^ card 𝒮)"
using μ01 BS_le_l by (simp add: power_diff power_divide)
also have "… ≤ (∏i∈ℛ∪ℬ∪𝒮∪𝒟. card (Xseq(Suc i)) / card (Xseq i))"
proof -
have "(∏i∈(ℛ∪ℬ)∪(𝒮∪𝒟). card (Xseq(Suc i)) / card (Xseq i))
≥ ((2 powr (ok_fun_72 μ k) * (1-μ) ^ card ℛ) * (2 powr (ok_fun_73 k) * μ ^ (l - card 𝒮)))
* ((2 powr ok_fun_74 k * bigbeta ^ card 𝒮) * (2 powr ok_fun_76 k))"
using μ01 by (auto simp: R B S D prod.union_disjoint prod_nonneg bigbeta_ge0 intro!: mult_mono)
then show ?thesis
by (simp add: Un_assoc mult_ac powr_add ok_fun_71_def)
qed
also have "… ≤ (∏i < halted_point. card (Xseq(Suc i)) / card (Xseq i))"
using below_m by auto
finally show ?thesis
using X0_nz μ01 unfolding tele by (simp add: divide_simps)
qed
end