Theory From_Diagonal
section ‹From diagonal to off-diagonal›
theory From_Diagonal
imports Closer_To_Diagonal
begin
subsection ‹Lemma 11.2›
definition "ok_fun_11_2a ≡ λk. ⌈real k powr (3/4)⌉ * log 2 k"
definition "ok_fun_11_2b ≡ λμ k. k powr (39/40) * (log 2 μ + 3 * log 2 k)"
definition "ok_fun_11_2c ≡ λμ k. - k * log 2 (1 - (2 / (1-μ)) * k powr (-1/40))"
definition "ok_fun_11_2 ≡ λμ k. 2 - ok_fun_71 μ k + ok_fun_11_2a k
+ max (ok_fun_11_2b μ k) (ok_fun_11_2c μ k)"
lemma ok_fun_11_2a: "ok_fun_11_2a ∈ o(real)"
unfolding ok_fun_11_2a_def
by real_asymp
text ‹possibly, the functions that depend upon @{term μ} need a more refined analysis to cover
a closed interval of possible values. But possibly not, as the text implies @{term "μ=2/5"}.›
lemma ok_fun_11_2b: "ok_fun_11_2b μ ∈ o(real)"
unfolding ok_fun_11_2b_def by real_asymp
lemma ok_fun_11_2c: "ok_fun_11_2c μ ∈ o(real)"
unfolding ok_fun_11_2c_def
by real_asymp
lemma ok_fun_11_2:
assumes "0<μ" "μ<1"
shows "ok_fun_11_2 μ ∈ o(real)"
unfolding ok_fun_11_2_def
by (simp add: assms const_smallo_real maxmin_in_smallo ok_fun_11_2a ok_fun_11_2b ok_fun_11_2c ok_fun_71 sum_in_smallo)
definition "Big_From_11_2 ≡
λμ k. Big_ZZ_8_6 μ k ∧ Big_X_7_1 μ k ∧ Big_Y_6_2 μ k ∧ Big_Red_5_3 μ k ∧ Big_Blue_4_1 μ k
∧ 1 ≤ μ^2 * real k ∧ 2 / (1-μ) * real k powr (-1/40) < 1 ∧ 1/k < 1/2 - 3 * eps k"
lemma Big_From_11_2:
assumes "0<μ0" "μ0 ≤ μ1" "μ1<1"
shows "∀⇧∞k. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_From_11_2 μ k"
proof -
have A: "∀⇧∞k. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 1 ≤ μ⇧2 * k"
proof (intro eventually_all_geI0)
show *: "∀⇧∞x. 1 ≤ μ0⇧2 * real x"
using ‹0<μ0› by real_asymp
next
fix k μ
assume "1 ≤ μ0⇧2 * real k" and "μ0 ≤ μ" "μ ≤ μ1"
with ‹0<μ0› show "1 ≤ μ⇧2 * k"
by (smt (verit, ccfv_SIG) mult_le_cancel_right of_nat_less_0_iff power_mono)
qed
have B: "∀⇧∞k. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 2 / (1-μ) * k powr (-1/40) < 1"
proof (intro eventually_all_geI1)
show "∀⇧∞k. 2 / (1-μ1) * k powr (-1/40) < 1"
by real_asymp
qed (use assms in auto)
have C: "∀⇧∞k. 1/k < 1/2 - 3 * eps k"
unfolding eps_def by real_asymp
show ?thesis
unfolding Big_From_11_2_def
using assms Big_ZZ_8_6 Big_X_7_1 Big_Y_6_2 Big_Red_5_3 Big_Blue_4_1 A B C
by (simp add: eventually_conj_iff all_imp_conj_distrib)
qed
text ‹Simply to prevent issues about the positioning of the function @{term real}›
abbreviation "ratio ≡ λμ s t. μ * (real s + real t) / real s"
text ‹the text refers to the actual Ramsey number but I don't see how that could work.
Theorem 11.1 will define @{term n} to be one less than the Ramsey number, hence we add that one back here.›
lemma (in Book) From_11_2:
assumes "l=k"
assumes big: "Big_From_11_2 μ k"
defines "ℛ ≡ Step_class {red_step}" and "𝒮 ≡ Step_class {dboost_step}"
defines "t ≡ card ℛ" and "s ≡ card 𝒮"
defines "nV' ≡ Suc nV"
assumes 0: "card X0 ≥ nV div 2" and "p0 ≥ 1/2"
shows "log 2 nV' ≤ k * log 2 (1/μ) + t * log 2 (1 / (1-μ)) + s * log 2 (ratio μ s t) + ok_fun_11_2 μ k"
proof -
have big71: "Big_X_7_1 μ k" and big62: "Big_Y_6_2 μ k" and big86: "Big_ZZ_8_6 μ k" and big53: "Big_Red_5_3 μ k"
and big41: "Big_Blue_4_1 μ k" and bigμ: "1 ≤ μ^2 * real k"
and big_le1: "2 / (1-μ) * real k powr (-1/40) < 1"
using big by (auto simp: Big_From_11_2_def)
have bigμ1: "1 ≤ μ * real k"
using bigμ μ01
by (smt (verit, best) mult_less_cancel_right2 mult_right_mono of_nat_less_0_iff power2_eq_square)
then have log2μk: "log 2 μ + log 2 k ≥ 0"
using kn0 μ01 add_log_eq_powr by auto
have bigμ2: "1 ≤ μ * (real k)⇧2"
unfolding power2_eq_square by (smt (verit, ccfv_SIG) bigμ1 μ01 mult_less_cancel_left1 mult_mono')
define g where "g ≡ λk. ⌈real k powr (3/4)⌉ * log 2 k"
have g: "g ∈ o(real)"
unfolding g_def by real_asymp
have bb_gt0: "bigbeta > 0"
using big53 bigbeta_gt0 ‹l=k› by blast
have "t < k"
by (simp add: ℛ_def t_def red_step_limit)
have "s < k"
unfolding 𝒮_def s_def
using bblue_dboost_step_limit big41 ‹l=k› by fastforce
have k34: "k powr (3/4) ≤ k powr 1"
using kn0 by (intro powr_mono) auto
define g712 where "g712 ≡ λk. 2 - ok_fun_71 μ k + g k"
have "nV' ≥ 2"
using gorder_ge2 nV'_def by linarith
have "nV' ≤ 4 * card X0"
using 0 card_XY0 by (auto simp: nV'_def odd_iff_mod_2_eq_one)
with μ01 have "2 powr (ok_fun_71 μ k - 2) * μ^k * (1-μ) ^ t * (bigbeta / μ) ^ s * nV'
≤ 2 powr ok_fun_71 μ k * μ^k * (1-μ) ^ t * (bigbeta / μ) ^ s * card X0"
using μ01 by (simp add: powr_diff mult.assoc bigbeta_ge0 mult_left_mono)
also have "… ≤ card (Xseq halted_point)"
using X_7_1 assms big71 by blast
also have "… ≤ 2 powr (g k)"
proof -
have "1/k < p0 - 3 * eps k"
using big ‹p0 ≥ 1/2› by (auto simp: Big_From_11_2_def)
also have "… ≤ pee halted_point"
using Y_6_2_halted big62 assms by blast
finally have "pee halted_point > 1/k" .
moreover have "termination_condition (Xseq halted_point) (Yseq halted_point)"
using halted_point_halted step_terminating_iff by blast
ultimately have "card (Xseq halted_point) ≤ RN k (nat ⌈real k powr (3/4)⌉)"
using ‹l=k› pee_def termination_condition_def by auto
then show ?thesis
unfolding g_def by (smt (verit) RN34_le_2powr_ok kn0 of_nat_le_iff)
qed
finally have 58: "2 powr (g k) ≥ 2 powr (ok_fun_71 μ k - 2) * μ^k * (1-μ) ^ t * (bigbeta / μ) ^ s * nV'" .
then have 59: "nV' ≤ 2 powr (g712 k) * (1/μ) ^ k * (1 / (1-μ)) ^ t * (μ / bigbeta) ^ s"
using μ01 bb_gt0 by (simp add: g712_def powr_diff powr_add mult.commute divide_simps) argo
define a where "a ≡ 2 / (1-μ)"
have ok_less1: "a * real k powr (-1/40) < 1"
unfolding a_def using big_le1 by blast
consider "s < k powr (39/40)" | "s ≥ k powr (39/40)" "bigbeta ≥ (1 - a * k powr (-1/40)) * (s / (s + t))"
using ZZ_8_6 big86 a_def ‹l=k› by (force simp: s_def t_def 𝒮_def ℛ_def)
then show ?thesis
proof cases
case 1
define h where "h ≡ λc k. real k powr (39/40) * (log 2 μ + real c * log 2 (real k))"
have h: "h c ∈ o(real)" for c
unfolding h_def by real_asymp
have le_h: "¦s * log 2 (ratio μ s t)¦ ≤ h 1 k"
proof (cases "s>0")
case True
with ‹s>0› have μeq: "ratio μ s t = μ * (1 + t/s)"
by (auto simp: distrib_left add_divide_distrib)
show ?thesis
proof (cases "log 2 (ratio μ s t) ≤ 0")
case True
have "s * (- log 2 (μ * (1 + t/s))) ≤ real k powr (39/40) * (log 2 μ + log 2 (real k))"
proof (intro mult_mono)
show "s ≤ k powr (39 / 40)"
using "1" by linarith
next
have "inverse (μ * (1 + t/s)) ≤ inverse μ"
using μ01 inverse_le_1_iff by fastforce
also have "… ≤ μ * k"
using bigμ μ01 by (metis neq_iff mult.assoc mult_le_cancel_left_pos power2_eq_square right_inverse)
finally have "inverse (μ * (1 + t/s)) ≤ μ * k" .
moreover have "0 < μ * (1 + real t / real s)"
using μ01 ‹0 < s› by (simp add: zero_less_mult_iff add_num_frac)
ultimately show "- log 2 (μ * (1 + real t / real s)) ≤ log 2 μ + log 2 (real k)"
using μ01 kn0 by (simp add: zero_less_mult_iff flip: log_inverse log_mult)
qed (use True μeq in auto)
with ‹s>0› bigμ1 True show ?thesis
by (simp add: μeq h_def mult_le_0_iff)
next
case False
have lek: "1 + t/s ≤ k"
proof -
have "real t ≤ real t * real s"
using True mult_le_cancel_left1 by fastforce
then have "1 + t/s ≤ 1 + t"
by (simp add: True pos_divide_le_eq)
also have "… ≤ k"
using ‹t < k› by linarith
finally show ?thesis .
qed
have "¦s * log 2 (ratio μ s t)¦ ≤ k powr (39/40) * log 2 (ratio μ s t)"
using False "1" by auto
also have "… = k powr (39/40) * (log 2 (μ * (1 + t/s)))"
by (simp add: μeq)
also have "… = k powr (39/40) * (log 2 μ + log 2 (1 + t/s))"
using μ01 by (smt (verit, best) divide_nonneg_nonneg log_mult of_nat_0_le_iff)
also have "… ≤ k powr (39/40) * (log 2 μ + log 2 k)"
by (smt (verit, best) "1" Transcendental.log_mono divide_nonneg_nonneg lek
mult_le_cancel_left_pos of_nat_0_le_iff)
also have "… ≤ h 1 k"
unfolding h_def using kn0 by force
finally show ?thesis .
qed
qed (use log2μk h_def in auto)
have β: "bigbeta ≥ 1 / (real k)⇧2"
using big53 bigbeta_ge_square ‹l=k› by blast
then have "(μ / bigbeta) ^ s ≤ (μ * (real k)⇧2) ^ s"
using bb_gt0 kn0 μ01 by (intro power_mono) (auto simp: divide_simps mult.commute)
also have "… ≤ (μ * (real k)⇧2) powr (k powr (39/40))"
using μ01 bigμ2 1 by (smt (verit) powr_less_mono powr_one_eq_one powr_realpow)
also have "… = 2 powr (log 2 ((μ * (real k)⇧2) powr (k powr (39/40))))"
by (smt (verit, best) bigμ2 powr_gt_zero powr_log_cancel)
also have "… = 2 powr h 2 k"
using μ01 bigμ2 kn0 by (simp add: log_powr log_nat_power log_mult h_def)
finally have †: "(μ / bigbeta) ^ s ≤ 2 powr h 2 k" .
have ‡: "nV' ≤ 2 powr (g712 k) * (1/μ) ^ k * (1 / (1-μ)) ^ t * 2 powr h 2 k"
using 59 mult_left_mono [OF †, of "2 powr (g712 k) * (1/μ) ^ k * (1 / (1-μ)) ^ t"]
by (smt (verit) μ01 pos_prod_le powr_nonneg_iff zero_less_divide_iff zero_less_power)
have *: "log 2 nV' ≤ k * log 2 (1/μ) + t * log 2 (1 / (1-μ)) + (g712 k + h 2 k)"
using μ01 ‹nV' ≥ 2› by (simp add: log_mult log_nat_power order.trans [OF Transcendental.log_mono [OF _ _ ‡]])
show ?thesis
proof -
have le_ok_fun: "g712 k + h 3 k ≤ ok_fun_11_2 μ k"
by (simp add: g712_def h_def ok_fun_11_2_def g_def ok_fun_11_2a_def ok_fun_11_2b_def)
have h3: "h 3 k = h 1 k + h 2 k - real k powr (39/40) * log 2 μ"
by (simp add: h_def algebra_simps)
have "0 ≤ h 1 k + s * log 2 ((μ * real s + μ * real t) / s)"
by (smt (verit, del_insts) of_nat_add distrib_left le_h)
moreover have "log 2 μ < 0"
using μ01 by simp
ultimately have "g712 k + h 2 k ≤ s * log 2 (ratio μ s t) + ok_fun_11_2 μ k"
by (smt (verit, best) kn0 distrib_left h3 le_ok_fun nat_neq_iff of_nat_eq_0_iff pos_prod_lt powr_gt_zero)
then show "log 2 nV' ≤ k * log 2 (1/μ) + t * log 2 (1 / (1-μ)) + s * log 2 (ratio μ s t) + ok_fun_11_2 μ k"
using "*" by linarith
qed
next
case 2
then have "s > 0"
using kn0 powr_gt_zero by fastforce
define h where "h ≡ λk. real k * log 2 (1 - a * k powr (-1/40))"
have "s * log 2 (μ / bigbeta) = s * log 2 μ - s * log 2 (bigbeta)"
using μ01 bb_gt0 2 by (simp add: log_divide algebra_simps)
also have "… ≤ s * log 2 μ - s * log 2 ((1 - a * k powr (-1/40)) * (s / (s + t)))"
using 2 ‹s>0› ok_less1 by (intro diff_mono order_refl mult_left_mono Transcendental.log_mono) auto
also have "… = s * log 2 μ - s * (log 2 (1 - a * k powr (-1/40)) + log 2 (s / (s + t)))"
using ‹0 < s› a_def add_log_eq_powr big_le1 by auto
also have "… = s * log 2 (ratio μ s t) - s * log 2 (1 - a * k powr (-1/40))"
using ‹0 < μ› ‹0 < s› minus_log_eq_powr by (auto simp flip: right_diff_distrib')
also have "… < s * log 2 (ratio μ s t) - h k"
proof -
have "log 2 (1 - a * real k powr (-1/40)) < 0"
using μ01 kn0 a_def ok_less1 by auto
with ‹s<k› show ?thesis
by (simp add: h_def)
qed
finally have †: "s * log 2 (μ / bigbeta) < s * log 2 (ratio μ s t) - h k" .
show ?thesis
proof -
have le_ok_fun: "g712 k - h k ≤ ok_fun_11_2 μ k"
by (simp add: g712_def h_def ok_fun_11_2_def g_def ok_fun_11_2a_def a_def ok_fun_11_2c_def)
have "log 2 nV' ≤ s * log 2 (μ / bigbeta) + k * log 2 (1/μ) + t * log 2 (1 / (1-μ)) + (g712 k)"
using μ01 ‹nV' ≥ 2›
by (simp add: bb_gt0 log_mult log_nat_power order.trans [OF Transcendental.log_mono [OF _ _ 59]])
with † le_ok_fun show "log 2 nV' ≤ k * log 2 (1/μ) + t * log 2 (1 / (1-μ)) + s * log 2 (ratio μ s t) + ok_fun_11_2 μ k"
by simp
qed
qed
qed
subsection ‹Lemma 11.3›
text ‹same remark as in Lemma 11.2 about the use of the Ramsey number in the conclusion›
lemma (in Book) From_11_3:
assumes "l=k"
assumes big: "Big_Y_6_1 μ k"
defines "ℛ ≡ Step_class {red_step}" and "𝒮 ≡ Step_class {dboost_step}"
defines "t ≡ card ℛ" and "s ≡ card 𝒮"
defines "nV' ≡ Suc nV"
assumes 0: "card Y0 ≥ nV div 2" and "p0 ≥ 1/2"
shows "log 2 nV' ≤ log 2 (RN k (k-t)) + s + t + 2 - ok_fun_61 k"
proof -
define RS where "RS ≡ Step_class {red_step,dboost_step}"
have "RS = ℛ ∪ 𝒮"
using Step_class_insert ℛ_def 𝒮_def RS_def by blast
moreover obtain "finite ℛ" "finite 𝒮"
by (simp add: ℛ_def 𝒮_def)
moreover have "disjnt ℛ 𝒮"
using ℛ_def 𝒮_def disjnt_Step_class by auto
ultimately have card_RS: "card RS = t+s"
by (simp add: t_def s_def card_Un_disjnt)
have 4: "nV'/4 ≤ card Y0"
using 0 card_XY0 by (auto simp: nV'_def odd_iff_mod_2_eq_one)
have ge0: "0 ≤ 2 powr ok_fun_61 k * p0 ^ card RS"
using p0_01 by fastforce
have "nV' ≥ 2"
using gorder_ge2 nV'_def by linarith
have "2 powr (- real s - real t + ok_fun_61 k - 2) * nV' = 2 powr (ok_fun_61 k - 2) * (1/2) ^ card RS * nV'"
by (simp add: powr_add powr_diff powr_minus power_add powr_realpow divide_simps card_RS)
also have "… ≤ 2 powr (ok_fun_61 k - 2) * p0 ^ card RS * nV'"
using power_mono [OF ‹p0 ≥ 1/2›] ‹nV' ≥ 2› by auto
also have "… ≤ 2 powr (ok_fun_61 k) * p0 ^ card RS * (nV'/4)"
by (simp add: divide_simps powr_diff split: if_split_asm)
also have "… ≤ 2 powr (ok_fun_61 k) * p0 ^ card RS * card Y0"
using mult_left_mono [OF 4 ge0 ] by simp
also have "… ≤ card (Yseq halted_point)"
using Y_6_1 big ‹l=k› by (auto simp: RS_def divide_simps split: if_split_asm)
finally have "2 powr (- real s - real t + ok_fun_61 k - 2) * nV' ≤ card (Yseq halted_point)" .
moreover
{ assume "card (Yseq halted_point) ≥ RN k (k-t)"
then obtain K where K: "K ⊆ Yseq halted_point" and "size_clique (k-t) K Red ∨ size_clique k K Blue"
by (metis RN_commute Red_Blue_RN Yseq_subset_V)
then have KRed: "size_clique (k-t) K Red"
using ‹l=k› no_Blue_clique by blast
have "card (K ∪ Aseq halted_point) = k"
proof (subst card_Un_disjnt)
show "finite K" "finite (Aseq halted_point)"
using K finite_Aseq finite_Yseq infinite_super by blast+
show "disjnt K (Aseq halted_point)"
using valid_state_seq[of halted_point] K disjnt_subset1
by (auto simp: valid_state_def disjoint_state_def)
have "card (Aseq halted_point) = t"
using red_step_eq_Aseq ℛ_def t_def by presburger
then show "card K + card (Aseq halted_point) = k"
using Aseq_less_k[OF] nat_less_le KRed size_clique_def by force
qed
moreover have "clique (K ∪ Aseq halted_point) Red"
proof -
obtain "K ⊆ V" "Aseq halted_point ⊆ V"
by (meson Aseq_subset_V KRed size_clique_def)
moreover have "clique K Red"
using KRed size_clique_def by blast
moreover have "clique (Aseq halted_point) Red"
by (meson A_Red_clique valid_state_seq)
moreover have "all_edges_betw_un (Aseq halted_point) (Yseq halted_point) ⊆ Red"
using valid_state_seq[of halted_point] K
by (auto simp: valid_state_def RB_state_def all_edges_betw_un_Un2)
then have "all_edges_betw_un K (Aseq halted_point) ⊆ Red"
using K all_edges_betw_un_mono2 all_edges_betw_un_commute by blast
ultimately show ?thesis
by (simp add: local.clique_Un)
qed
ultimately have "size_clique k (K ∪ Aseq halted_point) Red"
using KRed Aseq_subset_V by (auto simp: size_clique_def)
then have False
using no_Red_clique by blast
}
ultimately have *: "2 powr (- real s - real t + ok_fun_61 k - 2) * nV' < RN k (k-t)"
by fastforce
have "- real s - real t + ok_fun_61 k - 2 + log 2 nV' = log 2 (2 powr (- real s - real t + ok_fun_61 k - 2) * nV')"
using add_log_eq_powr ‹nV' ≥ 2› by auto
also have "… ≤ log 2 (RN k (k-t))"
using "*" Transcendental.log_mono ‹nV' ≥ 2› less_eq_real_def by auto
finally show "log 2 nV' ≤ log 2 (RN k (k - t)) + real s + real t + 2 - ok_fun_61 k"
by linarith
qed
subsection ‹Theorem 11.1›
definition FF :: "nat ⇒ real ⇒ real ⇒ real" where
"FF ≡ λk x y. log 2 (RN k (nat⌊real k - x * real k⌋)) / real k + x + y"
definition GG :: "real ⇒ real ⇒ real ⇒ real" where
"GG ≡ λμ x y. log 2 (1/μ) + x * log 2 (1/(1-μ)) + y * log 2 (μ * (x+y) / y)"
definition FF_bound :: "nat ⇒ real ⇒ real" where
"FF_bound ≡ λk u. FF k 0 u + 1"
lemma log2_RN_ge0: "0 ≤ log 2 (RN k k) / k"
proof (cases "k=0")
case False
then have "RN k k ≥ 1"
by (simp add: RN_eq_0_iff leI)
then show ?thesis
by simp
qed auto
lemma le_FF_bound:
assumes x: "x ∈ {0..1}" and "y ∈ {0..u}"
shows "FF k x y ≤ FF_bound k u"
proof (cases "⌊k - x*k⌋ = 0")
case True
with assms log2_RN_ge0[of k] show ?thesis
by (simp add: True FF_def FF_bound_def)
next
case False
with gr0I have "k>0" by fastforce
with False assms have *: "0 < ⌊k - x*k⌋"
using linorder_neqE_linordered_idom by fastforce
have le_k: "k - x*k ≤ k"
using x by auto
then have le_k: "nat ⌊k - x*k⌋ ≤ k"
by linarith
have "log 2 (RN k (nat ⌊k - x*k⌋)) / k ≤ log 2 (RN k k) / k"
proof (intro divide_right_mono Transcendental.log_mono)
show "0 < real (RN k (nat ⌊k - x*k⌋))"
by (metis RN_eq_0_iff ‹k>0› gr_zeroI * of_nat_0_less_iff zero_less_nat_eq)
qed (auto simp: RN_mono le_k)
then show ?thesis
using assms False le_SucE by (fastforce simp: FF_def FF_bound_def)
qed
lemma FF2: "y' ≤ y ⟹ FF k x y' ≤ FF k x y"
by (simp add: FF_def)
lemma FF_GG_bound:
assumes μ: "0 < μ" "μ < 1" and x: "x ∈ {0..1}" and y: "y ∈ {0..μ * x / (1-μ) + η}"
shows "min (FF k x y) (GG μ x y) + η ≤ FF_bound k (μ / (1-μ) + η) + η"
proof -
have FF_ub: "FF k x y ≤ FF_bound k (μ / (1-μ) + η)"
proof (rule order.trans)
show "FF k x y ≤ FF_bound k y"
using x y by (simp add: le_FF_bound)
next
have "y ≤ μ / (1-μ) + η"
using x y μ by simp (smt (verit, best) frac_le mult_left_le)
then show "FF_bound k y ≤ FF_bound k (μ / (1-μ) + η)"
by (simp add: FF_bound_def FF_def)
qed
show ?thesis
using FF_ub by auto
qed
context P0_min
begin
definition "ok_fun_11_1 ≡ λμ k. max (ok_fun_11_2 μ k) (2 - ok_fun_61 k)"
lemma ok_fun_11_1:
assumes "0<μ" "μ<1"
shows "ok_fun_11_1 μ ∈ o(real)"
unfolding ok_fun_11_1_def
by (simp add: assms const_smallo_real maxmin_in_smallo ok_fun_11_2 ok_fun_61 sum_in_smallo)
lemma eventually_ok111_le_η:
assumes "η > 0" and μ: "0<μ" "μ<1"
shows "∀⇧∞k. ok_fun_11_1 μ k / k ≤ η"
proof -
have "(λk. ok_fun_11_1 μ k / k) ∈ o(λk. 1)"
using eventually_mono ok_fun_11_1 [OF μ] by (fastforce simp: smallo_def divide_simps)
with assms have "∀⇧∞k. ¦ok_fun_11_1 μ k¦ / k ≤ η"
by (auto simp: smallo_def)
then show ?thesis
by (metis (mono_tags, lifting) eventually_mono abs_divide abs_le_D1 abs_of_nat)
qed
lemma eventually_powr_le_η:
assumes "η > 0"
shows "∀⇧∞k. (2 / (1-μ)) * k powr (-1/20) ≤ η"
using assms by real_asymp
definition "Big_From_11_1 ≡
λη μ k. Big_From_11_2 μ k ∧ Big_ZZ_8_5 μ k ∧ Big_Y_6_1 μ k ∧ ok_fun_11_1 μ k / k ≤ η/2
∧ (2 / (1-μ)) * k powr (-1/20) ≤ η/2
∧ Big_Closer_10_1 (1/101) (nat⌈k/100⌉) ∧ 3 / (k * ln 2) ≤ η/2 ∧ k≥3"
text ‹In sections 9 and 10 (and by implication all proceeding sections), we needed to consider
a closed interval of possible values of @{term μ}. Let's hope, maybe not here.
The fact below can only be proved with the strict inequality @{term "η > 0"},
which is why it is also strict in the theorems depending on this property.›
lemma Big_From_11_1:
assumes "η > 0" "0<μ" "μ<1"
shows "∀⇧∞k. Big_From_11_1 η μ k"
proof -
have "∀⇧∞l. Big_Closer_10_1 (1/101) l"
by (rule Big_Closer_10_1) auto
then have a: "∀⇧∞k. Big_Closer_10_1 (1/101) (nat⌈k/100⌉)"
unfolding eventually_sequentially
by (meson le_divide_eq_numeral1(1) le_natceiling_iff nat_ceiling_le_eq)
have b: "∀⇧∞k. 3 / (k * ln 2) ≤ η/2"
using ‹η>0› by real_asymp
show ?thesis
unfolding Big_From_11_1_def
using assms a b Big_From_11_2[of μ μ] Big_ZZ_8_5[of μ μ] Big_Y_6_1[of μ μ]
using eventually_ok111_le_η[of "η/2"] eventually_powr_le_η [of "η/2"]
by (auto simp: eventually_conj_iff all_imp_conj_distrib eventually_sequentially)
qed
text ‹The actual proof of theorem 11.1 is now combined with the development of section 12,
since the concepts seem to be inescapably mixed up.›
end
end