Theory Assumptions_and_Approximations
section ‹Simplied Version of Gordeev's Proof for Monotone Circuits›
subsection ‹Setup of Global Assumptions and Proofs of Approximations›
theory Assumptions_and_Approximations
imports
"HOL-Real_Asymp.Real_Asymp"
Stirling_Formula.Stirling_Formula
Preliminaries
begin
locale first_assumptions =
fixes l p k :: nat
assumes l2: "l > 2"
and pl: "p > l"
and kp: "k > p"
begin
lemma k2: "k > 2" using pl l2 kp by auto
lemma p: "p > 2" using pl l2 kp by auto
lemma k: "k > l" using pl l2 kp by auto
definition "m = k^4"
lemma km: "k < m"
using power_strict_increasing_iff[of k 1 4] k2 unfolding m_def by auto
lemma lm: "l + 1 < m" using km k by simp
lemma m2: "m > 2" using k2 km by auto
lemma mp: "m > p" using km k kp by simp
definition "L = fact l * (p - 1) ^ l"
lemma kml: "k ≤ m - l"
proof -
have "k ≤ k * k - k" using k2 by (cases k, auto)
also have "… ≤ (k * k) * 1 - l" using k by simp
also have "… ≤ (k * k) * (k * k) - l"
by (intro diff_le_mono mult_left_mono, insert k2, auto)
also have "(k * k) * (k * k) = m" unfolding m_def by algebra
finally show ?thesis .
qed
end
locale second_assumptions = first_assumptions +
assumes kl2: "k = l^2"
and l8: "l ≥ 8"
begin
lemma Lm: "L ≥ m"
proof -
have "m ≤ l ^ l"
unfolding L_def m_def
unfolding kl2 power_mult[symmetric]
by (intro power_increasing, insert l8, auto)
also have "… ≤ (p - 1) ^ l"
by (rule power_mono, insert pl, auto)
also have "… ≤ fact l * (p - 1) ^ l" by simp
also have "… ≤ L" unfolding L_def by simp
finally show ?thesis .
qed
lemma Lp: "L > p" using Lm mp by auto
lemma L3: "L > 3" using p Lp by auto
end
definition "eps = 1/(1000 :: real)"
lemma eps: "eps > 0" unfolding eps_def by simp
definition L0 :: nat where
"L0 = (SOME l0. ∀l≥l0. 1 / 3 < (1 + - 1 / real l) ^ l)"
definition M0 :: nat where
"M0 = (SOME y. ∀ x. x ≥ y ⟶ (root 8 (real x) * log 2 (real x) + 1) / real x powr (1 / 8 + eps) ≤ 1)"
definition L0' :: nat where
"L0' = (SOME l0. ∀ n ≥ l0. 6 * (real n)^16 * fact n < real (n⇧2 ^ 4) powr (1 / 8 * real (n⇧2 ^ 4) powr (1 / 8)))"
definition L0'' :: nat where "L0'' = (SOME l0. ∀ l ≥ l0. real l * log 2 (real (l⇧2 ^ 4)) + 1 < real (l⇧2))"
lemma L0'': assumes "l ≥ L0''" shows "real l * log 2 (real (l⇧2 ^ 4)) + 1 < real (l⇧2)"
proof -
have "(λ l :: nat. (real l * log 2 (real (l⇧2 ^ 4)) + 1) / real (l⇧2)) ⇢ 0" by real_asymp
from LIMSEQ_D[OF this, of 1] obtain l0
where "∀l≥l0. ¦1 + real l * log 2 (real l ^ 8)¦ / (real l)⇧2 < 1" by (auto simp: field_simps)
hence "∀ l ≥ max 1 l0. real l * log 2 (real (l⇧2 ^ 4)) + 1 < real (l⇧2)"
by (auto simp: field_simps)
hence "∃ l0. ∀ l ≥ l0. real l * log 2 (real (l⇧2 ^ 4)) + 1 < real (l⇧2)" by blast
from someI_ex[OF this, folded L0''_def, rule_format, OF assms]
show ?thesis .
qed
definition M0' :: nat where
"M0' = (SOME x0. ∀ x ≥ x0. real x powr (2 / 3) ≤ x powr (3 / 4) - 1)"
locale third_assumptions = second_assumptions +
assumes pllog: "l * log 2 m ≤ p" "real p ≤ l * log 2 m + 1"
and L0: "l ≥ L0"
and L0': "l ≥ L0'"
and M0': "m ≥ M0'"
and M0: "m ≥ M0"
begin
lemma approximation1:
"(real (k - 1)) ^ (m - l) * prod (λ i. real (k - 1 - i)) {0..<l}
> (real (k - 1)) ^ m / 3"
proof -
have "real (k - 1) ^ (m - l) * (∏i = 0..<l. real (k - 1 - i)) =
real (k - 1) ^ m *
(inverse (real (k - 1)) ^ l * (∏i = 0..<l. real (k - 1 - i)))"
by (subst power_diff_conv_inverse, insert k2 lm, auto)
also have "… > (real (k - 1)) ^ m * (1/3)"
proof (rule mult_strict_left_mono)
define f where "f l = (1 + (-1) / real l) ^ l" for l
define e1 :: real where "e1 = exp (- 1)"
define lim :: real where "lim = 1 / 3"
from tendsto_exp_limit_sequentially[of "-1", folded f_def]
have f: "f ⇢ e1" by (simp add: e1_def)
have "lim < (1 - 1 / real 6) ^ 6" unfolding lim_def by code_simp
also have " … ≤ exp (- 1)"
by (rule exp_ge_one_minus_x_over_n_power_n, auto)
finally have "lim < e1" unfolding e1_def by auto
with f have "∃ l0. ∀ l. l ≥ l0 ⟶ f l > lim"
by (metis eventually_sequentially order_tendstoD(1))
from someI_ex[OF this[unfolded f_def lim_def], folded L0_def] L0
have fl: "f l > 1/3" unfolding f_def by auto
define start where "start = inverse (real (k - 1)) ^ l * (∏i = 0..<l. real (k - 1 - i))"
have "uminus start
= uminus (prod (λ _. inverse (real (k - 1))) {0..<l} * prod (λ i. real (k - 1 - i)) {0 ..< l})"
by (simp add: start_def)
also have "… = uminus (prod (λ i. inverse (real (k - 1)) * real (k - 1 - i)) {0..<l})"
by (subst prod.distrib, simp)
also have "… ≤ uminus (prod (λ i. inverse (real (k - 1)) * real (k - 1 - (l - 1))) {0..<l})"
unfolding neg_le_iff_le
by (intro prod_mono conjI mult_left_mono, insert k2 l2, auto intro!: diff_le_mono2)
also have "… = uminus ((inverse (real (k - 1)) * real (k - l)) ^ l)" by simp
also have "inverse (real (k - 1)) * real (k - l) = inverse (real (k - 1)) * ((real (k - 1)) - (real l - 1))"
using l2 k2 k by simp
also have "… = 1 - (real l - 1) / (real (k - 1))" using l2 k2 k
by (simp add: field_simps)
also have "real (k - 1) = real k - 1" using k2 by simp
also have "… = (real l - 1) * (real l + 1)" unfolding kl2 of_nat_power
by (simp add: field_simps power2_eq_square)
also have "(real l - 1) / … = inverse (real l + 1)"
using l2 by (smt (verit, best) divide_divide_eq_left' divide_inverse nat_1_add_1 nat_less_real_le nonzero_mult_div_cancel_left of_nat_1 of_nat_add)
also have "- ((1 - inverse (real l + 1)) ^ l) ≤ - ((1 - inverse (real l)) ^ l)"
unfolding neg_le_iff_le
by (intro power_mono, insert l2, auto simp: field_simps)
also have "… < - (1/3)" using fl unfolding f_def by (auto simp: field_simps)
finally have start: "start > 1 / 3" by simp
thus "inverse (real (k - 1)) ^ l * (∏i = 0..<l. real (k - 1 - i)) > 1/3"
unfolding start_def by simp
qed (insert k2, auto)
finally show ?thesis by simp
qed
lemma approximation2: fixes s :: nat
assumes "m choose k ≤ s * L⇧2 * (m - l - 1 choose (k - l - 1))"
shows "((m - l) / k)^l / (6 * L^2) < s"
proof -
let ?r = real
define q where "q = (?r (L⇧2) * ?r (m - l - 1 choose (k - l - 1)))"
have q: "q > 0" unfolding q_def
by (insert L3 km, auto)
have "?r (m choose k) ≤ ?r (s * L⇧2 * (m - l - 1 choose (k - l - 1)))"
unfolding of_nat_le_iff using assms by simp
hence "m choose k ≤ s * q" unfolding q_def by simp
hence *: "s ≥ (m choose k) / q" using q by (metis mult_imp_div_pos_le)
have "(((m - l) / k)^l / (L^2)) / 6 < ((m - l) / k)^l / (L^2) / 1"
by (rule divide_strict_left_mono, insert m2 L3 lm k, auto intro!: mult_pos_pos divide_pos_pos zero_less_power)
also have "… = ((m - l) / k)^l / (L^2)" by simp
also have "… ≤ ((m choose k) / (m - l - 1 choose (k - l - 1))) / (L^2)"
proof (rule divide_right_mono)
define b where "b = ?r (m - l - 1 choose (k - l - 1))"
define c where "c = (?r k)^l"
have b0: "b > 0" unfolding b_def using km l2 by simp
have c0: "c > 0" unfolding c_def using k by auto
define aim where "aim = (((m - l) / k)^l ≤ (m choose k) / (m - l - 1 choose (k - l - 1)))"
have "aim ⟷ ((m - l) / k)^l ≤ (m choose k) / b" unfolding b_def aim_def by simp
also have "… ⟷ b * ((m - l) / k)^l ≤ (m choose k)" using b0
by (simp add: mult.commute pos_le_divide_eq)
also have "… ⟷ b * (m - l)^l / c ≤ (m choose k)"
by (simp add: power_divide c_def)
also have "… ⟷ b * (m - l)^l ≤ (m choose k) * c" using c0 b0
by (auto simp add: mult.commute pos_divide_le_eq)
also have "(m choose k) = fact m / (fact k * fact (m - k))"
by (rule binomial_fact, insert km, auto)
also have "b = fact (m - l - 1) / (fact (k - l - 1) * fact (m - l - 1 - (k - l - 1)))" unfolding b_def
by (rule binomial_fact, insert k km, auto)
finally have "aim ⟷
fact (m - l - 1) / fact (k - l - 1) * (m - l) ^ l / fact (m - l - 1 - (k - l - 1))
≤ (fact m / fact k) * (?r k)^l / fact (m - k)" unfolding c_def by simp
also have "m - l - 1 - (k - l - 1) = m - k" using l2 k km by simp
finally have "aim ⟷
fact (m - l - 1) / fact (k - l - 1) * ?r (m - l) ^ l
≤ fact m / fact k * ?r k ^ l" unfolding divide_le_cancel using km by simp
also have "… ⟷ (fact (m - (l + 1)) * ?r (m - l) ^ l) * fact k
≤ (fact m / k) * (fact (k - (l + 1)) * (?r k * ?r k ^ l))"
using k2
by (simp add: field_simps)
also have "…"
proof (intro mult_mono)
have "fact k ≤ fact (k - (l + 1)) * (?r k ^ (l + 1))"
by (rule fact_approx_minus, insert k, auto)
also have "… = (fact (k - (l + 1)) * ?r k ^ l) * ?r k" by simp
finally show "fact k ≤ fact (k - (l + 1)) * (?r k * ?r k ^ l)" by (simp add: field_simps)
have "fact (m - (l + 1)) * real (m - l) ^ l ≤ fact m / k ⟷
(fact (m - (l + 1)) * ?r k) * real (m - l) ^ l ≤ fact m" using k2 by (simp add: field_simps)
also have "…"
proof -
have "(fact (m - (l + 1)) * ?r k) * ?r (m - l) ^ l ≤
(fact (m - (l + 1)) * ?r (m - l)) * ?r (m - l) ^ l"
by (intro mult_mono, insert kml, auto)
also have "((fact (m - (l + 1)) * ?r (m - l)) * ?r (m - l) ^ l) =
(fact (m - (l + 1)) * ?r (m - l) ^ (l + 1))" by simp
also have "… ≤ fact m"
by (rule fact_approx_upper_minus, insert km k, auto)
finally show "fact (m - (l + 1)) * real k * real (m - l) ^ l ≤ fact m" .
qed
finally show "fact (m - (l + 1)) * real (m - l) ^ l ≤ fact m / k" .
qed auto
finally show "((m - l) / k)^l ≤ (m choose k) / (m - l - 1 choose (k - l - 1))"
unfolding aim_def .
qed simp
also have "… = (m choose k) / q"
unfolding q_def by simp
also have "… ≤ s" using q * by metis
finally show "((m - l) / k)^l / (6 * L^2) < s" by simp
qed
lemma approximation3: fixes s :: nat
assumes "(k - 1)^m / 3 < (s * (L⇧2 * (k - 1) ^ m)) / 2 ^ (p - 1)"
shows "((m - l) / k)^l / (6 * L^2) < s"
proof -
define A where "A = real (L⇧2 * (k - 1) ^ m)"
have A0: "A > 0" unfolding A_def using L3 k2 m2 by simp
from mult_strict_left_mono[OF assms, of "2 ^ (p - 1)"]
have "2^(p - 1) * (k - 1)^m / 3 < s * A"
by (simp add: A_def)
from divide_strict_right_mono[OF this, of A] A0
have "2^(p - 1) * (k - 1)^m / 3 / A < s"
by simp
also have "2^(p - 1) * (k - 1)^m / 3 / A = 2^(p - 1) / (3 * L^2)"
unfolding A_def using k2 by simp
also have "… = 2^p / (6 * L^2)" using p by (cases p, auto)
also have "2^p = 2 powr p"
by (simp add: powr_realpow)
finally have *: "2 powr p / (6 * L⇧2) < s" .
have "m ^ l = m powr l" using m2 l2 powr_realpow by auto
also have "… = 2 powr (log 2 m * l)"
unfolding powr_powr[symmetric]
by (subst powr_log_cancel, insert m2, auto)
also have "… = 2 powr (l * log 2 m)" by (simp add: ac_simps)
also have "… ≤ 2 powr p"
by (rule powr_mono, insert pllog, auto)
finally have "m ^ l ≤ 2 powr p" .
from divide_right_mono[OF this, of "6 * L⇧2"] *
have "m ^ l / (6 * L⇧2) < s" by simp
moreover have "((m - l) / k)^l / (6 * L^2) ≤ m^l / (6 * L^2)"
proof (rule divide_right_mono, unfold of_nat_power, rule power_mono)
have "real (m - l) / real k ≤ real (m - l) / 1"
using k2 lm by (intro divide_left_mono, auto)
also have "… ≤ m" by simp
finally show "(m - l) / k ≤ m" by simp
qed auto
ultimately show ?thesis by simp
qed
lemma identities: "k = root 4 m" "l = root 8 m"
proof -
let ?r = real
have "?r k ^ 4 = ?r m" unfolding m_def by simp
from arg_cong[OF this, of "root 4"]
show km_id: "k = root 4 m" by (simp add: real_root_pos2)
have "?r l ^ 8 = ?r m" unfolding m_def using kl2 by simp
from arg_cong[OF this, of "root 8"]
show lm_id: "l = root 8 m" by (simp add: real_root_pos2)
qed
lemma identities2: "root 4 m = m powr (1/4)" "root 8 m = m powr (1/8)"
by (subst root_powr_inverse, insert m2, auto)+
lemma appendix_A_1: assumes "x ≥ M0'" shows "x powr (2/3) ≤ x powr (3/4) - 1"
proof -
have "(λ x. x powr (2/3) / (x powr (3/4) - 1)) ⇢ 0"
by real_asymp
from LIMSEQ_D[OF this, of 1, simplified] obtain x0 :: nat where
sub: "x ≥ x0 ⟹ x powr (2 / 3) / ¦x powr (3/4) - 1¦ < 1" for x
by (auto simp: field_simps)
have "(λ x :: real. 2 / (x powr (3/4))) ⇢ 0"
by real_asymp
from LIMSEQ_D[OF this, of 1, simplified] obtain x1 :: nat where
sub2: "x ≥ x1 ⟹ 2 / x powr (3 / 4) < 1" for x by auto
{
fix x
assume x: "x ≥ x0" "x ≥ x1" "x ≥ 1"
define a where "a = x powr (3/4) - 1"
from sub[OF x(1)] have small: "x powr (2 / 3) / ¦a¦ ≤ 1"
by (simp add: a_def)
have 2: "2 ≤ x powr (3/4)" using sub2[OF x(2)] x(3) by simp
hence a: "a > 0" by (simp add: a_def)
from mult_left_mono[OF small, of a] a
have "x powr (2 / 3) ≤ a"
by (simp add: field_simps)
hence "x powr (2 / 3) ≤ x powr (3 / 4) - 1" unfolding a_def by simp
}
hence "∃ x0 :: nat. ∀ x ≥ x0. x powr (2 / 3) ≤ x powr (3 / 4) - 1"
by (intro exI[of _ "max x0 (max x1 1)"], auto)
from someI_ex[OF this, folded M0'_def, rule_format, OF assms]
show ?thesis .
qed
lemma appendix_A_2: "(p - 1)^l < m powr ((1 / 8 + eps) * l)"
proof -
define f where "f (x :: nat) = (root 8 x * log 2 x + 1) / (x powr (1/8 + eps))" for x
have "f ⇢ 0" using eps unfolding f_def by real_asymp
from LIMSEQ_D[OF this, of 1]
have ex: "∃ x. ∀ y. y ≥ x ⟶ f y ≤ 1" by fastforce
have lim: "root 8 m * log 2 m + 1 ≤ m powr (1 / 8 + eps)"
using someI_ex[OF ex[unfolded f_def], folded M0_def, rule_format, OF M0] m2
by (simp add: field_simps)
define start where "start = real (p - 1)^l"
have "(p - 1)^l < p ^ l"
by (rule power_strict_mono, insert p l2, auto)
hence "start < real (p ^ l)"
using start_def of_nat_less_of_nat_power_cancel_iff by blast
also have "… = p powr l"
by (subst powr_realpow, insert p, auto)
also have "… ≤ (l * log 2 m + 1) powr l"
by (rule powr_mono2, insert pllog, auto)
also have "l = root 8 m" unfolding identities by simp
finally have "start < (root 8 m * log 2 m + 1) powr root 8 m"
by (simp add: identities2)
also have "… ≤ (m powr (1 / 8 + eps)) powr root 8 m"
by (rule powr_mono2[OF _ _ lim], insert m2, auto)
also have "… = m powr ((1 / 8 + eps) * l)" unfolding powr_powr identities ..
finally show ?thesis unfolding start_def by simp
qed
lemma appendix_A_3: "6 * real l^16 * fact l < m powr (1 / 8 * l)"
proof -
define f where "f = (λn. 6 * (real n)^16 * (sqrt (2 * pi * real n) * (real n / exp 1) ^ n))"
define g where "g = (λ n. 6 * (real n)^16 * (sqrt (2 * 4 * real n) * (real n / 2) ^ n))"
define h where "h = (λ n. ((real (n⇧2 ^ 4) powr (1 / 8 * (real (n⇧2 ^ 4)) powr (1/8)))))"
have e: "2 ≤ (exp 1 :: real)" using exp_ge_add_one_self[of 1] by simp
from fact_asymp_equiv
have 1: "(λ n. 6 * (real n)^16 * fact n / h n) ∼[sequentially] (λ n. f n / h n)" unfolding f_def
by (intro asymp_equiv_intros)
have 2: "f n ≤ g n" for n unfolding f_def g_def
by (intro mult_mono power_mono divide_left_mono real_sqrt_le_mono, insert pi_less_4 e, auto)
have 2: "abs (f n / h n) ≤ abs (g n / h n)" for n
unfolding abs_le_square_iff power2_eq_square
by (intro mult_mono divide_right_mono 2, auto simp: h_def f_def g_def)
have 2: "abs (g n / h n) < e ⟹ abs (f n / h n) < e" for n e using 2[of n] by simp
have "(λn. g n / h n) ⇢ 0"
unfolding g_def h_def by real_asymp
from LIMSEQ_D[OF this] 2
have "(λn. f n / h n) ⇢ 0"
by (intro LIMSEQ_I, fastforce)
with 1 have "(λn. 6 * (real n)^16 * fact n / h n) ⇢ 0"
using tendsto_asymp_equiv_cong by blast
from LIMSEQ_D[OF this, of 1] obtain n0 where 3: "n ≥ n0 ⟹ norm (6 * (real n)^16 * fact n / h n) < 1" for n by auto
{
fix n
assume n: "n ≥ max 1 n0"
hence hn: "h n > 0" unfolding h_def by auto
from n have "n ≥ n0" by simp
from 3[OF this] have "6 * n ^ 16 * fact n / abs (h n) < 1" by auto
with hn have "6 * (real n) ^ 16 * fact n < h n" by simp
}
hence "∃ n0. ∀ n. n ≥ n0 ⟶ 6 * n ^ 16 * fact n < h n" by blast
from someI_ex[OF this[unfolded h_def], folded L0'_def, rule_format, OF L0']
have "6 * real l^16 * fact l < real (l⇧2 ^ 4) powr (1 / 8 * real (l⇧2 ^ 4) powr (1 / 8))" by simp
also have "… = m powr (1 / 8 * l)" using identities identities2 kl2
by (metis m_def)
finally show ?thesis .
qed
lemma appendix_A_4: "12 * L^2 ≤ m powr (m powr (1 / 8) * 0.51)"
proof -
let ?r = real
define Lappr where "Lappr = m * m * fact l * p ^ l / 2"
have "L = (fact l * (p - 1) ^ l)" unfolding L_def by simp
hence "?r L ≤ (fact l * (p - 1) ^ l)" by linarith
also have "… = (1 * ?r (fact l)) * (?r (p - 1) ^ l)" by simp
also have "… ≤ ((m * m / 2) * ?r (fact l)) * (?r (p - 1) ^ l)"
by (intro mult_right_mono, insert m2, cases m; cases "m - 1", auto)
also have "… = (6 * real (m * m) * fact l) * (?r (p - 1) ^ l) / 12" by simp
also have "real (m * m) = real l^16" unfolding m_def unfolding kl2 by simp
also have "(6 * real l^16 * fact l) * (?r (p - 1) ^ l) / 12
≤ (m powr (1 / 8 * l) * (m powr ((1 / 8 + eps) * l))) / 12"
by (intro divide_right_mono mult_mono, insert appendix_A_2 appendix_A_3, auto)
also have "… = (m powr (1 / 8 * l + (1 / 8 + eps) * l)) / 12"
by (simp add: powr_add)
also have "1 / 8 * l + (1 / 8 + eps) * l = l * (1/4 + eps)" by (simp add: field_simps)
also have "l = m powr (1/8)" unfolding identities identities2 ..
finally have LL: "?r L ≤ m powr (m powr (1 / 8) * (1 / 4 + eps)) / 12" .
from power_mono[OF this, of 2]
have "L^2 ≤ (m powr (m powr (1 / 8) * (1 / 4 + eps)) / 12)^2"
by simp
also have "… = (m powr (m powr (1 / 8) * (1 / 4 + eps)))^2 / 144"
by (simp add: power2_eq_square)
also have "… = (m powr (m powr (1 / 8) * (1 / 4 + eps) * 2)) / 144"
by (subst powr_realpow[symmetric], (use m2 in force), unfold powr_powr, simp)
also have "… = (m powr (m powr (1 / 8) * (1 / 2 + 2 * eps))) / 144"
by (simp add: algebra_simps)
also have "… ≤ (m powr (m powr (1 / 8) * 0.51)) / 144"
by (intro divide_right_mono powr_mono mult_left_mono, insert m2, auto simp: eps_def)
finally have "L^2 ≤ m powr (m powr (1 / 8) * 0.51) / 144" by simp
from mult_left_mono[OF this, of 12]
have "12 * L^2 ≤ 12 * m powr (m powr (1 / 8) * 0.51) / 144" by simp
also have "… = m powr (m powr (1 / 8) * 0.51) / 12" by simp
also have "… ≤ m powr (m powr (1 / 8) * 0.51) / 1"
by (rule divide_left_mono, auto)
finally show ?thesis by simp
qed
lemma approximation4: fixes s :: nat
assumes "s > ((m - l) / k)^l / (6 * L^2)"
shows "s > 2 * k powr (4 / 7 * sqrt k)"
proof -
let ?r = real
have diff: "?r (m - l) = ?r m - ?r l" using lm by simp
have "m powr (2/3) ≤ m powr (3/4) - 1" using appendix_A_1[OF M0'] by auto
also have "… ≤ (m - m powr (1/8)) / m powr (1/4)"
unfolding diff_divide_distrib
by (rule diff_mono, insert m2, auto simp: divide_powr_uminus powr_mult_base powr_add[symmetric],
auto simp: powr_minus_divide intro!: ge_one_powr_ge_zero)
also have "… = (m - root 8 m) / root 4 m" using m2
by (simp add: root_powr_inverse)
also have "… = (m - l) / k" unfolding identities diff by simp
finally have "m powr (2/3) ≤ (m - l) / k" by simp
from power_mono[OF this, of l]
have ineq1: "(m powr (2 / 3)) ^ l ≤ ((m - l) / k) ^ l" using m2 by auto
have "(m powr (l / 7)) ≤ (m powr (2 / 3 * l - l * 0.51))"
by (intro powr_mono, insert m2, auto)
also have "… = (m powr (2 / 3)) powr l / (m powr (m powr (1 / 8) * 0.51))"
unfolding powr_diff powr_powr identities identities2 by simp
also have "… = (m powr (2 / 3)) ^ l / (m powr (m powr (1 / 8) * 0.51))"
by (subst powr_realpow, insert m2, auto)
also have "… ≤ (m powr (2 / 3)) ^ l / (12 * L⇧2)"
by (rule divide_left_mono[OF appendix_A_4], insert L3 m2, auto intro!: mult_pos_pos)
also have "… = (m powr (2 / 3)) ^ l / (?r 12 * L⇧2)" by simp
also have "… ≤ ((m - l) / k) ^ l / (?r 12 * L⇧2)"
by (rule divide_right_mono[OF ineq1], insert L3, auto)
also have "… < s / 2" using assms by simp
finally have "2 * m powr (real l / 7) < s" by simp
also have "m powr (real l / 7) = m powr (root 8 m / 7)"
unfolding identities by simp
finally have "s > 2 * m powr (root 8 m / 7)" by simp
also have "root 8 m = root 2 k" using m2
by (metis identities(2) kl2 of_nat_0_le_iff of_nat_power pos2 real_root_power_cancel)
also have "?r m = k powr 4" unfolding m_def by simp
also have "(k powr 4) powr ((root 2 k) / 7)
= k powr (4 * (root 2 k) / 7)" unfolding powr_powr by simp
also have "… = k powr (4 / 7 * sqrt k)" unfolding sqrt_def by simp
finally show "s > 2 * k powr (4 / 7 * sqrt k)" .
qed
end
end