Theory Zeta_Zerofree
theory Zeta_Zerofree
imports
"PNT_Complex_Analysis_Lemmas"
begin
unbundle pnt_syntax
section ‹Zero-free region of zeta function›
lemma cos_inequality_1:
fixes x :: real
shows "3 + 4 * cos x + cos (2 * x) ≥ 0"
proof -
have "cos (2 * x) = (cos x)⇧2 - (sin x)⇧2"
by (rule cos_double)
also have "… = (cos x)⇧2 - (1 - (cos x)⇧2)"
unfolding sin_squared_eq ..
also have "… = 2 * (cos x)⇧2 - 1" by auto
finally have 1: "cos (2 * x) = 2 * (cos x)⇧2 - 1" .
have "0 ≤ 2 * (1 + cos x)⇧2" by auto
also have "… = 3 + 4 * cos x + (2 * (cos x)⇧2 - 1)"
by (simp add: field_simps power2_eq_square)
finally show ?thesis unfolding 1.
qed
lemma multiplicative_fds_zeta:
"completely_multiplicative_function (fds_nth fds_zeta_complex)"
by standard auto
lemma fds_mangoldt_eq:
"fds mangoldt_complex = -(fds_deriv fds_zeta / fds_zeta)"
proof -
have "fds_nth fds_zeta_complex 1 ≠ 0" by auto
hence "fds_nth (fds_deriv fds_zeta_complex / fds_zeta) n = -fds_nth fds_zeta n * mangoldt n" for n
using multiplicative_fds_zeta
by (intro fds_nth_logderiv_completely_multiplicative)
thus ?thesis by (intro fds_eqI, auto)
qed
lemma abs_conv_abscissa_log_deriv:
"abs_conv_abscissa (fds_deriv fds_zeta_complex / fds_zeta) ≤ 1"
by (rule abs_conv_abscissa_completely_multiplicative_log_deriv
[OF multiplicative_fds_zeta, unfolded abs_conv_abscissa_zeta], auto)
lemma abs_conv_abscissa_mangoldt:
"abs_conv_abscissa (fds mangoldt_complex) ≤ 1"
using abs_conv_abscissa_log_deriv
by (subst fds_mangoldt_eq, subst abs_conv_abscissa_minus)
lemma
assumes s: "Re s > 1"
shows eval_fds_mangoldt: "eval_fds (fds mangoldt) s = - deriv zeta s / zeta s"
and abs_conv_mangoldt: "fds_abs_converges (fds mangoldt) s"
proof -
from abs_conv_abscissa_log_deriv
have 1: "abs_conv_abscissa (fds_deriv fds_zeta_complex / fds_zeta) < ereal (s ∙ 1)"
using s by (intro le_ereal_less, auto simp: one_ereal_def)
have 2: "abs_conv_abscissa fds_zeta_complex < ereal (s ∙ 1)"
using s by (subst abs_conv_abscissa_zeta, auto)
hence 3: "fds_abs_converges (fds_deriv fds_zeta_complex / fds_zeta) s"
by (intro fds_abs_converges) (rule 1)
have "eval_fds (fds mangoldt) s = eval_fds (-(fds_deriv fds_zeta_complex / fds_zeta)) s"
using fds_mangoldt_eq by auto
also have "… = -eval_fds (fds_deriv fds_zeta_complex / fds_zeta) s"
by (intro eval_fds_uminus fds_abs_converges_imp_converges 3)
also have "… = -(eval_fds (fds_deriv fds_zeta_complex) s / eval_fds fds_zeta s)"
using s by (subst eval_fds_log_deriv; ((intro 1 2)?, (auto intro!: eval_fds_zeta_nonzero)?))
also have "… = - deriv zeta s / zeta s"
using s by (subst eval_fds_zeta, blast, subst eval_fds_deriv_zeta, auto)
finally show "eval_fds (fds mangoldt) s = - deriv zeta s / zeta s" .
show "fds_abs_converges (fds mangoldt) s"
by (subst fds_mangoldt_eq) (intro fds_abs_converges_uminus 3)
qed
lemma sums_mangoldt:
fixes s :: complex
assumes s: "Re s > 1"
shows "((λn. mangoldt n / n nat_powr s) has_sum - deriv zeta s / zeta s) {1..}"
proof -
let ?f = "(λn. mangoldt n / n nat_powr s)"
have 1: "fds_abs_converges (fds mangoldt) s"
by (intro abs_conv_mangoldt s)
hence 2: "fds_converges (fds mangoldt) s"
by (rule fds_abs_converges_imp_converges)
hence "summable (λn. ∥fds_nth (fds mangoldt) n / nat_power n s∥)"
by (fold fds_abs_converges_def, intro 1)
moreover have "(λn. fds_nth (fds mangoldt) n / nat_power n s) sums (- deriv zeta s / zeta s)"
by (subst eval_fds_mangoldt(1) [symmetric], intro s, fold fds_converges_iff, intro 2)
ultimately have "((λn. fds_nth (fds mangoldt) n / n nat_powr s) has_sum - deriv zeta s / zeta s) UNIV"
by (fold nat_power_complex_def, rule norm_summable_imp_has_sum)
moreover have [simp]: "(if n = 0 then 0 else mangoldt n) = mangoldt n" for n by auto
ultimately have "(?f has_sum - deriv zeta s / zeta s) UNIV" by (auto simp add: fds_nth_fds)
hence 3: "(?f has_sum - deriv zeta s / zeta s) UNIV" by auto
have "sum ?f {0} = 0" by auto
moreover have "(?f has_sum sum ?f {0}) {0}"
by (rule has_sum_finite, auto)
ultimately have "(?f has_sum 0) {0}" by auto
hence "(?f has_sum - deriv zeta s / zeta s - 0) (UNIV - {0})"
by (intro has_sum_Diff 3, auto)
moreover have "UNIV - {0 :: nat} = {1..}" by auto
ultimately show "(?f has_sum - deriv zeta s / zeta s) {1..}" by auto
qed
lemma sums_Re_logderiv_zeta:
fixes σ t :: real
assumes s: "σ > 1"
shows "((λn. mangoldt_real n * n nat_powr (-σ) * cos (t * ln n))
has_sum Re (- deriv zeta (Complex σ t) / zeta (Complex σ t))) {1..}"
proof -
have "((λx. Re (mangoldt_complex x / x nat_powr Complex σ t))
has_sum Re (- deriv zeta (Complex σ t) / zeta (Complex σ t))) {1..}"
using s by (intro has_sum_Re sums_mangoldt) auto
moreover have "Re (mangoldt n / n nat_powr (Complex σ t))
= mangoldt_real n * n nat_powr (-σ) * cos (t * ln n)" if *: "1 ≤ n" for n
proof -
let ?n = "n :: complex"
have "1 / n nat_powr (Complex σ t) = n nat_powr (Complex (-σ) (-t))"
by (fold powr_minus_divide, auto simp add: legacy_Complex_simps)
also have "… = exp (Complex (-σ * ln n) (-t * ln n))"
unfolding powr_def by (auto simp add: field_simps legacy_Complex_simps, use * in linarith)
finally have "Re (1 / n nat_powr (Complex σ t)) = Re …" by auto
also have "… = n nat_powr (-σ) * cos (t * ln n)"
by (unfold powr_def, subst Re_exp, use * in auto)
finally have 1: "mangoldt_real n * Re (1 / n nat_powr (Complex σ t))
= mangoldt_real n * n nat_powr (-σ) * cos (t * ln n)" by auto
have rule_1: "Re (w * z) = Re w * Re z" if *: "Im w = 0" for z w :: complex using * by auto
have "Re (mangoldt n * (1 / n nat_powr (Complex σ t)))
= mangoldt_real n * Re (1 / n nat_powr (Complex σ t))"
by (subst rule_1, auto)
with 1 show ?thesis by auto
qed
ultimately show "((λn. mangoldt_real n * n nat_powr (- σ) * cos (t * ln (real n)))
has_sum Re (- deriv zeta (Complex σ t) / zeta (Complex σ t))) {1..}"
by (subst has_sum_cong) auto
qed
lemma logderiv_zeta_ineq:
fixes σ t :: real
assumes s: "σ > 1"
shows "3 * Re (logderiv zeta (Complex σ 0)) + 4 * Re (logderiv zeta (Complex σ t))
+ Re (logderiv zeta (Complex σ (2*t))) ≤ 0" (is "?x ≤ 0")
proof -
have [simp]: "Re (-z) = - Re z" for z by auto
have "((λn.
3 * (mangoldt_real n * n nat_powr (-σ) * cos (0 * ln n))
+ 4 * (mangoldt_real n * n nat_powr (-σ) * cos (t * ln n))
+ 1 * (mangoldt_real n * n nat_powr (-σ) * cos (2*t * ln n))
) has_sum
3 * Re (- deriv zeta (Complex σ 0) / zeta (Complex σ 0))
+ 4 * Re (- deriv zeta (Complex σ t) / zeta (Complex σ t))
+ 1 * Re (- deriv zeta (Complex σ (2*t)) / zeta (Complex σ (2*t)))
) {1..}"
by (intro has_sum_add has_sum_cmult_right sums_Re_logderiv_zeta s)
hence *: "((λn. mangoldt_real n * n nat_powr (-σ)
* (3 + 4 * cos (t * ln n) + cos (2 * (t * ln n)))
) has_sum -?x) {1..}"
unfolding logderiv_def by (auto simp add: field_simps)
have "-?x ≥ 0"
by (rule has_sum_nonneg, rule *,
intro mult_nonneg_nonneg,
auto intro: mangoldt_nonneg cos_inequality_1)
thus "?x ≤ 0" by linarith
qed
lemma sums_zeta_real:
fixes r :: real
assumes "1 < r"
shows "(∑n. (n⇩+) powr -r) = Re (zeta r)"
proof -
have "(∑n. (n⇩+) powr -r) = (∑n. Re (n⇩+ powr (-r :: complex)))"
by (subst of_real_nat_power) auto
also have "… = (∑n. Re (n⇩+ powr - (r :: complex)))" by auto
also have "… = Re (∑n. n⇩+ powr - (r :: complex))"
by (intro Re_suminf [symmetric] summable_zeta)
(use assms in auto)
also have "… = Re (zeta r)"
using Re_complex_of_real zeta_conv_suminf assms by presburger
finally show ?thesis .
qed
lemma inverse_zeta_bound':
assumes "1 < Re s"
shows "∥inverse (zeta s)∥ ≤ Re (zeta (Re s))"
proof -
write moebius_mu (‹μ›)
let ?f = "λn :: nat. μ (n⇩+) / (n⇩+) powr s"
let ?g = "λn :: nat. (n⇩+) powr - Re s"
have "∥μ n :: complex∥ ≤ 1" for n by (auto simp add: power_neg_one_If moebius_mu_def)
hence 1: "∥?f n∥ ≤ ?g n" for n
by (auto simp add: powr_minus norm_divide norm_powr_real_powr field_simps)
have "inverse (zeta s) = (∑n. ?f n)"
by (intro sums_unique inverse_zeta_sums assms)
hence "∥inverse (zeta s)∥ = ∥∑n. ?f n∥" by auto
also have "… ≤ (∑n. ?g n)" by (intro suminf_norm_bound summable_zeta_real assms 1)
finally show ?thesis using sums_zeta_real assms by auto
qed
lemma zeta_bound':
assumes "1 < Re s"
shows "∥zeta s∥ ≤ Re (zeta (Re s))"
proof -
let ?f = "λn :: nat. (n⇩+) powr - s"
let ?g = "λn :: nat. (n⇩+) powr - Re s"
have "zeta s = (∑n. ?f n)" by (intro sums_unique sums_zeta assms)
hence "∥zeta s∥ = ∥∑n. ?f n∥" by auto
also have "… ≤ (∑n. ?g n)"
by (intro suminf_norm_bound summable_zeta_real assms)
(subst norm_nat_power, auto)
also have "… = Re (zeta (Re s))" by (subst sums_zeta_real) (use assms in auto)
finally show ?thesis .
qed
lemma zeta_bound_trivial':
assumes "1 / 2 ≤ Re s ∧ Re s ≤ 2"
and "¦Im s¦ ≥ 1 / 11"
shows "∥zeta s∥ ≤ 12 + 2 * ¦Im s¦"
proof -
have "∥pre_zeta 1 s∥ ≤ ∥s∥ / Re s"
by (rule pre_zeta_1_bound) (use assms in auto)
also have "… ≤ (¦Re s¦ + ¦Im s¦) / Re s"
proof -
have "∥s∥ ≤ ¦Re s¦ + ¦Im s¦" using cmod_le by auto
thus ?thesis using assms by (auto intro: divide_right_mono)
qed
also have "… = 1 + ¦Im s¦ / Re s"
using assms by (simp add: field_simps)
also have "… ≤ 1 + ¦Im s¦ / (1 / 2)"
using assms by (intro add_left_mono divide_left_mono) auto
finally have 1: "∥pre_zeta 1 s∥ ≤ 1 + 2 * ¦Im s¦" by auto
have "∥1 / (s - 1)∥ = 1 / ∥s - 1∥" by (subst norm_divide) auto
also have "… ≤ 11" proof -
have "1 / 11 ≤ ¦Im s¦" by (rule assms(2))
also have "… = ¦Im (s - 1)¦" by auto
also have "… ≤ ∥s - 1∥" by (rule abs_Im_le_cmod)
finally show ?thesis by (intro mult_imp_div_pos_le) auto
qed
finally have 2: "∥1 / (s - 1)∥ ≤ 11" by auto
have "zeta s = pre_zeta 1 s + 1 / (s - 1)" by (intro zeta_pole_eq) (use assms in auto)
moreover have "∥…∥ ≤ ∥pre_zeta 1 s∥ + ∥1 / (s - 1)∥" by (rule norm_triangle_ineq)
ultimately have "∥zeta s∥ ≤ …" by auto
also have "… ≤ 12 + 2 * ¦Im s¦" using 1 2 by auto
finally show ?thesis .
qed
lemma zeta_bound_gt_1:
assumes "1 < Re s"
shows "∥zeta s∥ ≤ Re s / (Re s - 1)"
proof -
have "∥zeta s∥ ≤ Re (zeta (Re s))" by (intro zeta_bound' assms)
also have "… ≤ ∥zeta (Re s)∥" by (rule complex_Re_le_cmod)
also have "… = ∥pre_zeta 1 (Re s) + 1 / (Re s - 1)∥"
by (subst zeta_pole_eq) (use assms in auto)
also have "… ≤ ∥pre_zeta 1 (Re s)∥ + ∥1 / (Re s - 1) :: complex∥"
by (rule norm_triangle_ineq)
also have "… ≤ 1 + 1 / (Re s - 1)"
proof -
have "∥pre_zeta 1 (Re s)∥ ≤ ∥Re s :: complex∥ / Re (Re s)"
by (rule pre_zeta_1_bound) (use assms in auto)
also have "… = 1" using assms by auto
moreover have "∥1 / (Re s - 1) :: complex∥ = 1 / (Re s - 1)"
by (subst norm_of_real) (use assms in auto)
ultimately show ?thesis by auto
qed
also have "… = Re s / (Re s - 1)"
using assms by (auto simp add: field_simps)
finally show ?thesis .
qed
lemma zeta_bound_trivial:
assumes "1 / 2 ≤ Re s" and "¦Im s¦ ≥ 1 / 11"
shows "∥zeta s∥ ≤ 12 + 2 * ¦Im s¦"
proof (cases "Re s ≤ 2")
assume "Re s ≤ 2"
thus ?thesis by (intro zeta_bound_trivial') (use assms in auto)
next
assume "¬ Re s ≤ 2"
hence *: "Re s > 1" "Re s > 2" by auto
hence "∥zeta s∥ ≤ Re s / (Re s - 1)" by (intro zeta_bound_gt_1)
also have "… ≤ 2" using * by (auto simp add: field_simps)
also have "… ≤ 12 + 2 * ¦Im s¦" by auto
finally show ?thesis .
qed
lemma zeta_nonzero_small_imag':
assumes "¦Im s¦ ≤ 13 / 22" and "Re s ≥ 1 / 2" and "Re s < 1"
shows "zeta s ≠ 0"
proof -
have "∥pre_zeta 1 s∥ ≤ (1 + ∥s∥ / Re s) / 2 * 1 powr - Re s"
by (rule pre_zeta_bound) (use assms(2) in auto)
also have "… ≤ 129 / 100" proof -
have "∥s∥ / Re s ≤ 79 / 50"
proof (rule ccontr)
assume "¬ ∥s∥ / Re s ≤ 79 / 50"
hence "sqrt (6241 / 2500) < ∥s∥ / Re s" by (simp add: real_sqrt_divide)
also have "… = ∥s∥ / sqrt ((Re s)⇧2)" using assms(2) by simp
also have "… = sqrt (1 + (Im s / Re s)⇧2)"
unfolding cmod_def using assms(2)
by (auto simp add: real_sqrt_divide [symmetric] field_simps
simp del: real_sqrt_abs)
finally have 1: "6241 / 2500 < 1 + (Im s / Re s)⇧2" by auto
have "¦Im s / Re s¦ ≤ ¦6 / 5¦" using assms by (auto simp add: field_simps abs_le_square_iff)
hence "(Im s / Re s)⇧2 ≤ (6 / 5)⇧2" by (subst (asm) abs_le_square_iff)
hence 2: "1 + (Im s / Re s)⇧2 ≤ 61 / 25" unfolding power2_eq_square by auto
from 1 2 show False by auto
qed
hence "(1 + ∥s∥ / Re s) / 2 ≤ (129 / 50) / 2" by (subst divide_right_mono) auto
also have "… = 129 / 100" by auto
finally show ?thesis by auto
qed
finally have 1: "∥pre_zeta 1 s∥ ≤ 129 / 100" .
have "∥s - 1∥ < 100 / 129" proof -
from assms have "(Re (s - 1))⇧2 ≤ (1 / 2)⇧2" by (simp add: abs_le_square_iff [symmetric])
moreover have "(Im (s - 1))⇧2 ≤ (13 / 22)⇧2" using assms(1) by (simp add: abs_le_square_iff [symmetric])
ultimately have "(Re (s - 1))⇧2 + (Im (s - 1))⇧2 ≤ 145 / 242" by (auto simp add: power2_eq_square)
hence "sqrt ((Re (s - 1))⇧2 + (Im (s - 1))⇧2) ≤ sqrt (145 / 242)" by (rule real_sqrt_le_mono)
also have "… < sqrt ((100 / 129)⇧2)" by (subst real_sqrt_less_iff) (simp add: power2_eq_square)
finally show ?thesis unfolding cmod_def by auto
qed
moreover have "∥s - 1∥ ≠ 0" using assms(3) by auto
ultimately have 2: "∥1 / (s - 1)∥ > 129 / 100" by (auto simp add: field_simps norm_divide)
from 1 2 have "0 < ∥1 / (s - 1)∥ - ∥pre_zeta 1 s∥" by auto
also have "… ≤ ∥pre_zeta 1 s + 1 / (s - 1)∥" by (subst add.commute) (rule norm_diff_ineq)
also from assms(3) have "s ≠ 1" by auto
hence "∥pre_zeta 1 s + 1 / (s - 1)∥ = ∥zeta s∥" using zeta_pole_eq by auto
finally show ?thesis by auto
qed
lemma zeta_nonzero_small_imag:
assumes "¦Im s¦ ≤ 13 / 22" and "Re s > 0" and "s ≠ 1"
shows "zeta s ≠ 0"
proof -
consider "Re s ≤ 1 / 2" | "1 / 2 ≤ Re s ∧ Re s < 1" | "Re s ≥ 1" by fastforce
thus ?thesis proof cases
case 1 hence "zeta (1 - s) ≠ 0" using assms by (intro zeta_nonzero_small_imag') auto
moreover case 1
ultimately show ?thesis using assms(2) zeta_zero_reflect_iff by auto
next
case 2 thus ?thesis using assms(1) by (intro zeta_nonzero_small_imag') auto
next
case 3 thus ?thesis using zeta_Re_ge_1_nonzero assms(3) by auto
qed
qed
lemma inverse_zeta_bound:
assumes "1 < Re s"
shows "∥inverse (zeta s)∥ ≤ Re s / (Re s - 1)"
proof -
have "∥inverse (zeta s)∥ ≤ Re (zeta (Re s))" by (intro inverse_zeta_bound' assms)
also have "… ≤ ∥zeta (Re s)∥" by (rule complex_Re_le_cmod)
also have "… ≤ Re (Re s) / (Re (Re s) - 1)"
by (intro zeta_bound_gt_1) (use assms in auto)
also have "… = Re s / (Re s - 1)" by auto
finally show ?thesis .
qed
lemma deriv_zeta_bound:
fixes s :: complex
assumes Hr: "0 < r" and Hs: "s ≠ 1"
and hB: "⋀w. ∥s - w∥ = r ⟹ ∥pre_zeta 1 w∥ ≤ B"
shows "∥deriv zeta s∥ ≤ B / r + 1 / ∥s - 1∥⇧2"
proof -
have "∥deriv zeta s∥ = ∥deriv (pre_zeta 1) s - 1 / (s - 1)⇧2∥"
proof -
let ?A = "UNIV - {1 :: complex}"
let ?f = "λs. pre_zeta 1 s + 1 / (s - 1)"
let ?v = "deriv (pre_zeta 1) s + (0 * (s - 1) - 1 * (1 - 0)) / (s - 1)⇧2"
let ?v' = "deriv (pre_zeta 1) s - 1 / (s - 1 :: complex)⇧2"
have "∀z∈?A. zeta z = pre_zeta 1 z + 1 / (z - 1)"
by (auto intro: zeta_pole_eq)
hence "∀⇩F z in nhds s. zeta z = pre_zeta 1 z + 1 / (z - 1)"
using Hs by (subst eventually_nhds, intro exI [where x = ?A]) auto
hence "DERIV zeta s :> ?v' = DERIV ?f s :> ?v'"
by (intro DERIV_cong_ev) auto
moreover have "DERIV ?f s :> ?v"
unfolding power2_eq_square
by (intro derivative_intros field_differentiable_derivI holomorphic_pre_zeta
holomorphic_on_imp_differentiable_at [where s = ?A])
(use Hs in auto)
moreover have "?v = ?v'" by (auto simp add: field_simps)
ultimately have "DERIV zeta s :> ?v'" by auto
moreover have "DERIV zeta s :> deriv zeta s"
by (intro field_differentiable_derivI field_differentiable_at_zeta)
(use Hs in auto)
ultimately have "?v' = deriv zeta s" by (rule DERIV_unique)
thus ?thesis by auto
qed
also have "… ≤ ∥deriv (pre_zeta 1) s∥ + ∥1 / (s - 1)⇧2∥" by (rule norm_triangle_ineq4)
also have "… ≤ B / r + 1 / ∥s - 1∥⇧2"
proof -
have "∥(deriv ^^ 1) (pre_zeta 1) s∥ ≤ fact 1 * B / r ^ 1"
by (intro Cauchy_inequality holomorphic_pre_zeta continuous_on_pre_zeta assms) auto
thus ?thesis by (auto simp add: norm_divide norm_power)
qed
finally show ?thesis .
qed
lemma zeta_lower_bound:
assumes "0 < Re s" "s ≠ 1"
shows "1 / ∥s - 1∥ - ∥s∥ / Re s ≤ ∥zeta s∥"
proof -
have "∥pre_zeta 1 s∥ ≤ ∥s∥ / Re s" by (intro pre_zeta_1_bound assms)
hence "1 / ∥s - 1∥ - ∥s∥ / Re s ≤ ∥1 / (s - 1)∥ - ∥pre_zeta 1 s∥"
using assms by (auto simp add: norm_divide)
also have "… ≤ ∥pre_zeta 1 s + 1 / (s - 1)∥"
by (subst add.commute) (rule norm_diff_ineq)
also have "… = ∥zeta s∥" using assms by (subst zeta_pole_eq) auto
finally show ?thesis .
qed
lemma logderiv_zeta_bound:
fixes σ :: real
assumes "1 < σ" "σ ≤ 23 / 20"
shows "∥logderiv zeta σ∥ ≤ 5 / 4 * (1 / (σ - 1))"
proof -
have "∥pre_zeta 1 s∥ ≤ sqrt 2" if *: "∥σ - s∥ = 1 / sqrt 2" for s :: complex
proof -
have 1: "0 < Re s" proof -
have "1 - Re s ≤ Re (σ - s)" using assms(1) by auto
also have "Re (σ - s) ≤ ∥σ - s∥" by (rule complex_Re_le_cmod)
also have "… = 1 / sqrt 2" by (rule *)
finally have "1 - 1 / sqrt 2 ≤ Re s" by auto
moreover have "0 < 1 - 1 / sqrt 2" by auto
ultimately show ?thesis by linarith
qed
hence "∥pre_zeta 1 s∥ ≤ ∥s∥ / Re s" by (rule pre_zeta_1_bound)
also have "… ≤ sqrt 2" proof -
define x y where "x ≡ Re s" and "y ≡ Im s"
have "sqrt ((σ - x)⇧2 + y⇧2) = 1 / sqrt 2"
using * unfolding cmod_def x_def y_def by auto
also have "… = sqrt (1 / 2)" by (auto simp add: field_simps real_sqrt_mult [symmetric])
finally have 2: "x⇧2 + y⇧2 - 2*σ*x + σ⇧2 = 1 / 2" by (auto simp add: field_simps power2_eq_square)
have "y⇧2 ≤ x⇧2" proof (rule ccontr)
assume "¬ y⇧2 ≤ x⇧2"
hence "x⇧2 < y⇧2" by auto
with 2 have "2*x⇧2 - 2*σ*x + σ⇧2 < 1 / 2" by auto
hence "2 * (x - σ / 2)⇧2 < (1 - σ⇧2) / 2" by (auto simp add: field_simps power2_eq_square)
also have "… < 0" using ‹1 < σ› by auto
finally show False by auto
qed
moreover have "x ≠ 0" unfolding x_def using 1 by auto
ultimately have "sqrt ((x⇧2 + y⇧2) / x⇧2) ≤ sqrt 2" by (auto simp add: field_simps)
with 1 show ?thesis unfolding cmod_def x_def y_def by (auto simp add: real_sqrt_divide)
qed
finally show ?thesis .
qed
hence "∥deriv zeta σ∥ ≤ sqrt 2 / (1 / sqrt 2) + 1 / ∥(σ :: complex) - 1∥⇧2"
by (intro deriv_zeta_bound) (use assms(1) in auto)
also have "… ≤ 2 + 1 / (σ - 1)⇧2"
by (subst in_Reals_norm) (use assms(1) in auto)
also have "… = (2 * σ⇧2 - 4 * σ + 3) / (σ - 1)⇧2"
proof -
have "σ * σ - 2 * σ + 1 = (σ - 1) * (σ - 1)" by (auto simp add: field_simps)
also have "… ≠ 0" using assms(1) by auto
finally show ?thesis by (auto simp add: power2_eq_square field_simps)
qed
finally have 1: "∥deriv zeta σ∥ ≤ (2 * σ⇧2 - 4 * σ + 3) / (σ - 1)⇧2" .
have "(2 - σ) / (σ - 1) = 1 / ∥(σ :: complex) - 1∥ - ∥σ :: complex∥ / Re σ"
using assms(1) by (auto simp add: field_simps in_Reals_norm)
also have "… ≤ ∥zeta σ∥" by (rule zeta_lower_bound) (use assms(1) in auto)
finally have 2: "(2 - σ) / (σ - 1) ≤ ∥zeta σ∥" .
have "4 * (2 * σ⇧2 - 4 * σ + 3) - 5 * (2 - σ) = 8 * (σ - 11 / 16)⇧2 - 57 / 32"
by (auto simp add: field_simps power2_eq_square)
also have "… ≤ 0" proof -
have "0 ≤ σ - 11 / 16" using assms(1) by auto
moreover have "σ - 11 / 16 ≤ 37 / 80" using assms(2) by auto
ultimately have "(σ - 11 / 16)⇧2 ≤ (37 / 80)⇧2" by auto
thus ?thesis by (auto simp add: power2_eq_square)
qed
finally have "4 * (2 * σ⇧2 - 4 * σ + 3) - 5 * (2 - σ) ≤ 0" .
moreover have "0 < 2 - σ" using assms(2) by auto
ultimately have 3: "(2 * σ⇧2 - 4 * σ + 3) / (2 - σ) ≤ 5 / 4" by (subst pos_divide_le_eq) auto
moreover have "0 ≤ 2 * σ⇧2 - 4 * σ + 3" proof -
have "0 ≤ 2 * (σ - 1)⇧2 + 1" by auto
also have "… = 2 * σ⇧2 - 4 * σ + 3" by (auto simp add: field_simps power2_eq_square)
finally show ?thesis .
qed
moreover have "0 < (2 - σ) / (σ - 1)" using assms by auto
ultimately have "∥logderiv zeta σ∥ ≤ ((2 * σ⇧2 - 4 * σ + 3) / (σ - 1)⇧2) / ((2 - σ) / (σ - 1))"
unfolding logderiv_def using 1 2 by (subst norm_divide) (rule frac_le, auto)
also have "… = (2 * σ⇧2 - 4 * σ + 3) / (2 - σ) * (1 / (σ - 1))"
by (simp add: power2_eq_square)
also have "… ≤ 5 / 4 * (1 / (σ - 1))"
using 3 by (rule mult_right_mono) (use assms(1) in auto)
finally show ?thesis .
qed
lemma Re_logderiv_zeta_bound:
fixes σ :: real
assumes "1 < σ" "σ ≤ 23 / 20"
shows "Re (logderiv zeta σ) ≥ - 5 / 4 * (1 / (σ - 1))"
proof -
have "- Re (logderiv zeta σ) = Re (- logderiv zeta σ)" by auto
also have "Re (- logderiv zeta σ) ≤ ∥- logderiv zeta σ∥" by (rule complex_Re_le_cmod)
also have "… = ∥logderiv zeta σ∥" by auto
also have "… ≤ 5 / 4 * (1 / (σ - 1))" by (intro logderiv_zeta_bound assms)
finally show ?thesis by auto
qed
locale zeta_bound_param =
fixes θ φ :: "real ⇒ real"
assumes zeta_bn': "⋀z. 1 - θ (Im z) ≤ Re z ⟹ Im z ≥ 1 / 11 ⟹ ∥zeta z∥ ≤ exp (φ (Im z))"
and θ_pos: "⋀t. 0 < θ t ∧ θ t ≤ 1 / 2"
and φ_pos: "⋀t. 1 ≤ φ t"
and inv_θ: "⋀t. φ t / θ t ≤ 1 / 960 * exp (φ t)"
and moθ: "antimono θ" and moφ: "mono φ"
begin
definition "region ≡ {z. 1 - θ (Im z) ≤ Re z ∧ Im z ≥ 1 / 11}"
lemma zeta_bn: "⋀z. z ∈ region ⟹ ∥zeta z∥ ≤ exp (φ (Im z))"
using zeta_bn' unfolding region_def by auto
lemma θ_pos': "⋀t. 0 < θ t ∧ θ t ≤ 1"
using θ_pos by (smt (verit) exp_ge_add_one_self exp_half_le2)
lemma φ_pos': "⋀t. 0 < φ t" using φ_pos by (smt (verit, ccfv_SIG))
end
locale zeta_bound_param_1 = zeta_bound_param +
fixes γ :: real
assumes γ_cnd: "γ ≥ 13 / 22"
begin
definition r where "r ≡ θ (2 * γ + 1)"
end
locale zeta_bound_param_2 = zeta_bound_param_1 +
fixes σ δ :: real
assumes σ_cnd: "σ ≥ 1 + exp (- φ(2 * γ + 1))"
and δ_cnd: "δ = γ ∨ δ = 2 * γ"
begin
definition s where "s ≡ Complex σ δ"
end
context zeta_bound_param_2 begin
declare dist_complex_def [simp] norm_minus_commute [simp]
declare legacy_Complex_simps [simp]
lemma cball_lm:
assumes "z ∈ cball s r"
shows "r ≤ 1" "¦Re z - σ¦ ≤ r" "¦Im z - δ¦ ≤ r"
"1 / 11 ≤ Im z" "Im z ≤ 2 * γ + r"
proof -
have "¦Re (z - s)¦ ≤ ∥z - s∥" "¦Im (z - s)¦ ≤ ∥z - s∥"
by (rule abs_Re_le_cmod) (rule abs_Im_le_cmod)
moreover have "∥z - s∥ ≤ r" using assms by auto
ultimately show 1: "¦Re z - σ¦ ≤ r" "¦Im z - δ¦ ≤ r" unfolding s_def by auto
moreover have 3: "r ≤ 1 / 2" unfolding r_def using θ_pos by auto
ultimately have 2: "¦Re z - σ¦ ≤ 1 / 2" "¦Im z - δ¦ ≤ 1 / 2" by auto
moreover have "δ ≤ 2 * γ" using δ_cnd γ_cnd by auto
ultimately show "Im z ≤ 2 * γ + r" using 1 by auto
have "1 / 11 ≤ δ - 1 / 2" using δ_cnd γ_cnd by auto
also have "… ≤ Im z" using 2 by (auto simp del: Num.le_divide_eq_numeral1)
finally show "1 / 11 ≤ Im z" .
from 3 show "r ≤ 1" by auto
qed
lemma cball_in_region:
shows "cball s r ⊆ region"
proof
fix z :: complex
assume hz: "z ∈ cball s r"
note lm = cball_lm [OF hz]
hence "1 - θ (Im z) ≤ 1 - θ (2 * γ + θ (2 * γ + 1))"
unfolding r_def using moθ lm by (auto intro: antimonoD)
also have "… ≤ 1 + exp (-φ (2 * γ + 1)) - θ (2 * γ + 1)"
proof -
have "2 * γ + θ (2 * γ + 1) ≤ 2 * γ + 1"
unfolding r_def using θ_pos' by auto
hence "θ (2 * γ + 1) - θ (2 * γ + θ (2 * γ + 1)) ≤ 0"
using moθ by (auto intro: antimonoD)
also have "0 ≤ exp (-φ (2 * γ + 1))" by auto
finally show ?thesis by auto
qed
also have "… ≤ σ - r" using σ_cnd unfolding r_def s_def by auto
also have "… ≤ Re z" using lm by auto
finally have "1 - θ (Im z) ≤ Re z" .
thus "z ∈ region" unfolding region_def using lm by auto
qed
lemma Re_s_gt_1:
shows "1 < Re s"
proof -
have *: "exp (- φ (2 * γ + 1)) > 0" by auto
show ?thesis using σ_cnd s_def by auto (use * in linarith)
qed
lemma zeta_analytic_on_region:
shows "zeta analytic_on region"
by (rule analytic_zeta) (unfold region_def, auto)
lemma zeta_div_bound:
assumes "z ∈ cball s r"
shows "∥zeta z / zeta s∥ ≤ exp (3 * φ (2 * γ + 1))"
proof -
let ?φ = "φ (2 * γ + 1)"
have "∥zeta z∥ ≤ exp (φ (Im z))" using cball_in_region zeta_bn assms by auto
also have "… ≤ exp (?φ)"
proof -
have "Im z ≤ 2 * γ + 1" using cball_lm [OF assms] by auto
thus ?thesis by auto (rule monoD [OF moφ])
qed
also have "∥inverse (zeta s)∥ ≤ exp (2 * ?φ)"
proof -
have "∥inverse (zeta s)∥ ≤ Re s / (Re s - 1)"
by (intro inverse_zeta_bound Re_s_gt_1)
also have "… = 1 + 1 / (Re s - 1)"
using Re_s_gt_1 by (auto simp add: field_simps)
also have "… ≤ 1 + exp (?φ)"
proof -
have "Re s - 1 ≥ exp (-?φ)" using s_def σ_cnd by auto
hence "1 / (Re s - 1) ≤ 1 / exp (-?φ)"
using Re_s_gt_1 by (auto intro: divide_left_mono)
thus ?thesis by (auto simp add: exp_minus field_simps)
qed
also have "… ≤ exp (2 * ?φ)" by (intro exp_lemma_1 less_imp_le φ_pos)
finally show ?thesis .
qed
ultimately have "∥zeta z * inverse (zeta s)∥ ≤ exp (?φ) * exp (2 * ?φ)"
by (subst norm_mult, intro mult_mono') auto
also have "… = exp (3 * ?φ)" by (subst exp_add [symmetric]) auto
finally show ?thesis by (auto simp add: divide_inverse)
qed
lemma logderiv_zeta_bound:
shows "Re (logderiv zeta s) ≥ - 24 * φ (2 * γ + 1) / r"
and "⋀β. σ - r / 2 ≤ β ⟹ zeta (Complex β δ) = 0 ⟹
Re (logderiv zeta s) ≥ - 24 * φ (2 * γ + 1) / r + 1 / (σ - β)"
proof -
have 1: "0 < r" unfolding r_def using θ_pos' by auto
have 2: "0 ≤ 3 * φ (2 * γ + 1)" using φ_pos' by (auto simp add: less_imp_le)
have 3: "zeta s ≠ 0" "⋀z. Re s < Re z ⟹ zeta z ≠ 0"
using Re_s_gt_1 by (auto intro!: zeta_Re_gt_1_nonzero)
have 4: "zeta analytic_on cball s r"
by (rule analytic_on_subset;
rule cball_in_region zeta_analytic_on_region)
have 5: "z ∈ cball s r ⟹ ∥zeta z / zeta s∥ ≤ exp (3 * φ (2 * γ + 1))"
for z by (rule zeta_div_bound)
have 6: "{} ⊆ {z ∈ cball s (r / 2). zeta z = 0}" by auto
have 7: "{Complex β δ} ⊆ {z ∈ cball s (r / 2). zeta z = 0}"
if "σ - r / 2 ≤ β" "zeta (Complex β δ) = 0" for β
proof -
have "β ≤ σ"
using zeta_Re_gt_1_nonzero [of "Complex β δ"] Re_s_gt_1 that(2)
unfolding s_def by fastforce
thus ?thesis using that unfolding s_def by auto
qed
have "- Re (logderiv zeta s) ≤ 8 * (3 * φ (2 * γ + 1)) / r + Re (∑z∈{}. 1 / (z - s))"
by (intro lemma_3_9_beta3 1 2 3 4 5 6)
thus "Re (logderiv zeta s) ≥ - 24 * φ (2 * γ + 1) / r" by auto
show "Re (logderiv zeta s) ≥ - 24 * φ (2 * γ + 1) / r + 1 / (σ - β)"
if *: "σ - r / 2 ≤ β" "zeta (Complex β δ) = 0" for β
proof -
have bs: "β ≠ σ" using *(2) 3(1) unfolding s_def by auto
hence bs': "1 / (β - σ) = - 1 / (σ - β)" by (auto simp add: field_simps)
have inv_r: "1 / (Complex r 0) = Complex (1 / r) 0" if "r ≠ 0" for r
using that by (auto simp add: field_simps)
have "- Re (logderiv zeta s) ≤ 8 * (3 * φ (2 * γ + 1)) / r + Re (∑z∈{Complex β δ}. 1 / (z - s))"
by (intro lemma_3_9_beta3 1 2 3 4 5 7 *)
thus ?thesis unfolding s_def
by (auto simp add: field_simps)
(subst (asm) inv_r, use bs bs' in auto)
qed
qed
end
context zeta_bound_param_1 begin
lemma zeta_nonzero_region':
assumes "1 + 1 / 960 * (r / φ (2 * γ + 1)) - r / 2 ≤ β"
and "zeta (Complex β γ) = 0"
shows "1 - β ≥ 1 / 29760 * (r / φ (2 * γ + 1))"
proof -
let ?φ = "φ (2 * γ + 1)" and ?θ = "θ (2 * γ + 1)"
define σ where "σ ≡ 1 + 1 / 960 * (r / φ (2 * γ + 1))"
define a where "a ≡ - 5 / 4 * (1 / (σ - 1))"
define b where "b ≡ - 24 * φ (2 * γ + 1) / r + 1 / (σ - β)"
define c where "c ≡ - 24 * φ (2 * γ + 1) / r"
have "1 + exp (- ?φ) ≤ σ"
proof -
have "960 * exp (- ?φ) = 1 / (1 / 960 * exp ?φ)"
by (auto simp add: exp_add [symmetric] field_simps)
also have "… ≤ 1 / (?φ / ?θ)" proof -
have "?φ / ?θ ≤ 1 / 960 * exp ?φ" by (rule inv_θ)
thus ?thesis by (intro divide_left_mono) (use θ_pos φ_pos' in auto)
qed
also have "… = r / ?φ" unfolding r_def by auto
finally show ?thesis unfolding σ_def by auto
qed
note * = this γ_cnd
interpret z: zeta_bound_param_2 θ φ γ σ γ by (standard, use * in auto)
interpret z': zeta_bound_param_2 θ φ γ σ "2 * γ" by (standard, use * in auto)
have "r ≤ 1" unfolding r_def using θ_pos' [of "2 * γ + 1"] by auto
moreover have "1 ≤ φ (2 * γ + 1)" using φ_pos by auto
ultimately have "r / φ (2 * γ + 1) ≤ 1" by auto
moreover have "0 < r" "0 < φ (2 * γ + 1)" unfolding r_def using θ_pos' φ_pos' by auto
hence "0 < r / φ (2 * γ + 1)" by auto
ultimately have 1: "1 < σ" "σ ≤ 23 / 20" unfolding σ_def by auto
hence "Re (logderiv zeta σ) ≥ a" unfolding a_def by (intro Re_logderiv_zeta_bound)
hence "Re (logderiv zeta (Complex σ 0)) ≥ a" by auto
moreover have "Re (logderiv zeta z.s) ≥ b" unfolding b_def
by (rule z.logderiv_zeta_bound) (use assms r_def σ_def in auto)
hence "Re (logderiv zeta (Complex σ γ)) ≥ b" unfolding z.s_def by auto
moreover have "Re (logderiv zeta z'.s) ≥ c" unfolding c_def by (rule z'.logderiv_zeta_bound)
hence "Re (logderiv zeta (Complex σ (2 * γ))) ≥ c" unfolding z'.s_def by auto
ultimately have "3 * a + 4 * b + c
≤ 3 * Re (logderiv zeta (Complex σ 0)) + 4 * Re (logderiv zeta (Complex σ γ))
+ Re (logderiv zeta (Complex σ (2 * γ)))" by auto
also have "… ≤ 0" by (rule logderiv_zeta_ineq, rule 1)
finally have "3 * a + 4 * b + c ≤ 0" .
hence "4 / (σ - β) ≤ 15 / 4 * (1 / (σ - 1)) + 120 * φ (2 * γ + 1) / r"
unfolding a_def b_def c_def by auto
also have "… = 3720 * φ (2 * γ + 1) / r" unfolding σ_def by auto
finally have 2: "inverse (σ - β) ≤ 930 * φ (2 * γ + 1) / r" by (auto simp add: inverse_eq_divide)
have 3: "σ - β ≥ 1 / 930 * (r / φ (2 * γ + 1))"
proof -
have "1 / 930 * (r / φ (2 * γ + 1)) = 1 / (930 * (φ (2 * γ + 1) / r))"
by (auto simp add: field_simps)
also have "… ≤ σ - β" proof -
have "β ≤ 1" using assms(2) zeta_Re_gt_1_nonzero [of "Complex β γ"] by fastforce
also have "1 < σ" by (rule 1)
finally have "β < σ" .
thus ?thesis using 2 by (auto intro: inverse_le_imp_le)
qed
finally show ?thesis .
qed
show ?thesis proof -
let ?x = "r / φ (2 * γ + 1)"
have "1 / 29760 * ?x = 1 / 930 * ?x - 1 / 960 * ?x" by auto
also have "… ≤ (σ - β) - (σ - 1)" using 3 by (subst (2) σ_def) auto
also have "… = 1 - β" by auto
finally show ?thesis .
qed
qed
lemma zeta_nonzero_region:
assumes "zeta (Complex β γ) = 0"
shows "1 - β ≥ 1 / 29760 * (r / φ (2 * γ + 1))"
proof (cases "1 + 1 / 960 * (r / φ (2 * γ + 1)) - r / 2 ≤ β")
case True
thus ?thesis using assms by (rule zeta_nonzero_region')
next
case False
let ?x = "r / φ (2 * γ + 1)"
assume 1: "¬ 1 + 1 / 960 * ?x - r / 2 ≤ β"
have "0 < r" using θ_pos' unfolding r_def by auto
hence "1 / 930 * ?x ≤ r / 2"
using φ_pos [of "2 * γ + 1"] by (auto intro!: mult_imp_div_pos_le)
hence "1 / 29760 * ?x ≤ r / 2 - 1 / 960 * ?x" by auto
also have "… ≤ 1 - β" using 1 by auto
finally show ?thesis .
qed
end
context zeta_bound_param begin
theorem zeta_nonzero_region:
assumes "zeta (Complex β γ) = 0" and "Complex β γ ≠ 1"
shows "1 - β ≥ 1 / 29760 * (θ (2 * ¦γ¦ + 1) / φ (2 * ¦γ¦ + 1))"
proof (cases "¦γ¦ ≥ 13 / 22")
case True
assume 1: "13 / 22 ≤ ¦γ¦"
have 2: "zeta (Complex β ¦γ¦) = 0"
proof (cases "γ ≥ 0")
case True thus ?thesis using assms by auto
next
case False thus ?thesis by (auto simp add: complex_cnj [symmetric] intro: assms)
qed
interpret z: zeta_bound_param_1 θ φ ‹¦γ¦› by standard (use 1 in auto)
show ?thesis by (intro z.zeta_nonzero_region [unfolded z.r_def] 2)
next
case False
hence 1: "¦γ¦ ≤ 13 / 22" by auto
show ?thesis
proof (cases "0 < β", rule ccontr)
case True thus False using zeta_nonzero_small_imag [of "Complex β γ"] assms 1 by auto
next
have "0 < θ (2 * ¦γ¦ + 1)" "θ (2 * ¦γ¦ + 1) ≤ 1" "1 ≤ φ (2 * ¦γ¦ + 1)"
using θ_pos' φ_pos by auto
hence "1 / 29760 * (θ (2 * ¦γ¦ + 1) / φ (2 * ¦γ¦ + 1)) ≤ 1" by auto
also case False hence "1 ≤ 1 - β" by auto
finally show ?thesis .
qed
qed
end
lemma zeta_bound_param_nonneg:
fixes θ φ :: "real ⇒ real"
assumes zeta_bn': "⋀z. 1 - θ (Im z) ≤ Re z ⟹ Im z ≥ 1 / 11 ⟹ ∥zeta z∥ ≤ exp (φ (Im z))"
and θ_pos: "⋀t. 0 ≤ t ⟹ 0 < θ t ∧ θ t ≤ 1 / 2"
and φ_pos: "⋀t. 0 ≤ t ⟹ 1 ≤ φ t"
and inv_θ: "⋀t. 0 ≤ t ⟹ φ t / θ t ≤ 1 / 960 * exp (φ t)"
and moθ: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ θ y ≤ θ x"
and moφ: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ φ x ≤ φ y"
shows "zeta_bound_param (λt. θ (max 0 t)) (λt. φ (max 0 t))"
by standard (insert assms, auto simp add: antimono_def mono_def)
interpretation classical_zeta_bound:
zeta_bound_param "λt. 1 / 2" "λt. 4 * ln (12 + 2 * max 0 t)"
proof -
define θ :: "real ⇒ real" where "θ ≡ λt. 1 / 2"
define φ :: "real ⇒ real" where "φ ≡ λt. 4 * ln (12 + 2 * t)"
have "zeta_bound_param (λt. θ (max 0 t)) (λt. φ (max 0 t))"
proof (rule zeta_bound_param_nonneg)
fix z assume *: "1 - θ (Im z) ≤ Re z" "Im z ≥ 1 / 11"
have "∥zeta z∥ ≤ 12 + 2 * ¦Im z¦"
using * unfolding θ_def by (intro zeta_bound_trivial) auto
also have "… = exp (ln (12 + 2 * Im z))" using *(2) by auto
also have "… ≤ exp (φ (Im z))" proof -
have "0 ≤ ln (12 + 2 * Im z)" using *(2) by auto
thus ?thesis unfolding φ_def by auto
qed
finally show "∥zeta z∥ ≤ exp (φ (Im z))" .
next
fix t :: real assume *: "0 ≤ t"
have "φ t / θ t = 8 * ln (12 + 2 * t)" unfolding φ_def θ_def by auto
also have "… ≤ 8 * (5 / 2 + t)"
proof -
have "ln (12 + 2 * t) = ln (12 * (1 + t / 6))" by auto
also have "… = ln 12 + ln (1 + t / 6)"
unfolding ln_mult using * by simp
also have "… ≤ 5 / 2 + t / 6"
proof (rule add_mono)
have "(144 :: real) < (271 / 100) ^ 5"
by (simp add: power_numeral_reduce)
also have "271 / 100 < exp (1 :: real)"
using e_approx_32 by (simp add: abs_if split: if_split_asm)
hence "(271 / 100) ^ 5 < exp (1 :: real) ^ 5"
by (rule power_strict_mono) auto
also have "… = exp ((5 :: nat) * (1 :: real))"
by (rule exp_of_nat_mult [symmetric])
also have "… = exp (5 :: real)"
by auto
finally have "exp (ln (12 :: real) * (2 :: nat)) ≤ exp 5"
by (subst exp_of_nat2_mult) auto
thus "ln (12 :: real) ≤ 5 / 2"
by auto
show "ln (1 + t / 6) ≤ t / 6"
by (intro ln_add_one_self_le_self) (use * in auto)
qed
finally show ?thesis using * by auto
qed
also have "… ≤ 1 / 960 * exp (φ t)"
proof -
have "8 * (5 / 2 + t) - 1 / 960 * (12 + 2 * t) ^ 4
= -(1 / 60 * t ^ 4 + 2 / 5 * t ^ 3 + 18 / 5 * t ^ 2 + 32 / 5 * t + 8 / 5)"
by (simp add: power_numeral_reduce field_simps)
also have "… ≤ 0" using *
by (subst neg_le_0_iff_le) (auto intro: add_nonneg_nonneg)
moreover have "exp (φ t) = (12 + 2 * t) ^ 4"
proof -
have "exp (φ t) = (12 + 2 * t) powr (real 4)" unfolding φ_def powr_def using * by auto
also have "… = (12 + 2 * t) ^ 4" by (rule powr_realpow) (use * in auto)
finally show ?thesis .
qed
ultimately show ?thesis by auto
qed
finally show "φ t / θ t ≤ 1 / 960 * exp (φ t)" .
next
fix t :: real assume *: "0 ≤ t"
have "(1 :: real) ≤ 4 * 1" by auto
also have "… ≤ 4 * ln 12"
proof -
have "exp (1 :: real) ≤ 3" by (rule exp_le)
also have "… ≤ exp (ln 12)" by auto
finally have "(1 :: real) ≤ ln 12" using exp_le_cancel_iff by blast
thus ?thesis by auto
qed
also have "… ≤ 4 * ln (12 + 2 * t)" using * by auto
finally show "1 ≤ φ t" unfolding φ_def .
next
show "⋀t. 0 < θ t ∧ θ t ≤ 1 / 2"
"⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ θ y ≤ θ x"
"⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ φ x ≤ φ y"
unfolding θ_def φ_def by auto
qed
thus "zeta_bound_param (λt. 1 / 2) (λt. 4 * ln (12 + 2 * max 0 t))"
unfolding θ_def φ_def by auto
qed
theorem zeta_nonzero_region:
assumes "zeta (Complex β γ) = 0" and "Complex β γ ≠ 1"
shows "1 - β ≥ C⇩1 / ln (¦γ¦ + 2)"
proof -
have "1 / 952320 * (1 / ln (¦γ¦ + 2))
≤ 1 / 29760 * (1 / 2 / (4 * ln (12 + 2 * max 0 (2 * ¦γ¦ + 1))))" (is "?x ≤ ?y")
proof -
have "ln (14 + 4 * ¦γ¦) ≤ 4 * ln (¦γ¦ + 2)" by (rule ln_bound_1) auto
hence "1 / 238080 / (4 * ln (¦γ¦ + 2)) ≤ 1 / 238080 / (ln (14 + 4 * ¦γ¦))"
by (intro divide_left_mono) auto
also have "… = ?y" by auto
finally show ?thesis by auto
qed
also have "… ≤ 1 - β" by (intro classical_zeta_bound.zeta_nonzero_region assms)
finally show ?thesis unfolding PNT_const_C⇩1_def by auto
qed
unbundle no pnt_syntax
end