def zeroZ : Set ℂ

Equations

• zeroZ = {s : ℂ | riemannZeta s = 0}

def ZetaZerosNearPoint (t : ℝ) : Set ℂ

Equations

• ZetaZerosNearPoint t = {ρ : ℂ | ρ ∈ zeroZ ∧ ‖ρ - (3 / 2 + ↑t * Complex.I)‖ ≤ 5 / 6}

theorem ZetaZerosNearPoint_finite (t : ℝ) : (ZetaZerosNearPoint t).Finite

theorem lem_Re1zge0 (z : ℂ) : z.re > 0 → (1 / z).re > 0

theorem lem_sigmage1 (sigma t : ℝ) (hsigma : sigma > 1) : riemannZeta (↑sigma + ↑t * Complex.I) ≠ 0

theorem lem_sigmale1 (sigma1 t1 : ℝ) : riemannZeta (↑sigma1 + ↑t1 * Complex.I) = 0 → sigma1 ≤ 1

theorem lem_sigmale1Zt (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : rho1.re ≤ 1

theorem lem_s_notin_Zt (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : 1 + ↑δ + ↑t * Complex.I ∉ ZetaZerosNearPoint t

theorem complex_abs_of_real (x : ℝ) : ‖↑x‖ = |x|

theorem complex_add_real_imag_parts (a b t : ℝ) : (↑a + ↑b + ↑t * Complex.I).re = a + b ∧ (↑a + ↑b + ↑t * Complex.I).im = t

theorem complex_abs_real_cast (r : ℝ) : ‖↑r‖ = |r|

theorem isBigO_comp_principal_domain {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : β → E} {g : β → F} {h : α → β} {l : Filter α} {s : Set β} (hfg : f =O[Filter.principal s] g) (h_domain : ∀ᶠ (x : α) in l, h x ∈ s) : (f ∘ h) =O[l] (g ∘ h)

theorem isBigOWith_comp_principal_domain {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {C : ℝ} {f : β → E} {g : β → F} {h : α → β} {l : Filter α} {s : Set β} (hfg : Asymptotics.IsBigOWith C (Filter.principal s) f g) (h_domain : ∀ᶠ (x : α) in l, h x ∈ s) : Asymptotics.IsBigOWith C l (f ∘ h) (g ∘ h)

theorem s_in_D12 (delta : ℝ) (hdelta_pos : 0 < delta) (t : ℝ) (hdelta_lt : delta < 1) : 1 + ↑delta + ↑t * Complex.I ∈ Metric.ball (3 / 2 + ↑t * Complex.I) (1 / 2)

theorem zerosetKfRc_eq_ZetaZerosNearPoint (t : ℝ) : zerosetKfRc (5 / 6) (3 / 2 + ↑t * Complex.I) riemannZeta = ZetaZerosNearPoint t

theorem mem_closedBall_of_mem_ball {x c : ℂ} {r : ℝ} (hx : x ∈ Metric.ball c r) : x ∈ Metric.closedBall c r

theorem I_mul_real_eq_real_mul_I (t : ℝ) : Complex.I * ↑t = ↑t * Complex.I

theorem center_eq_comm (t : ℝ) : 3 / 2 + Complex.I * ↑t = 3 / 2 + ↑t * Complex.I

theorem log_abs_le_log_abs_add_two {t : ℝ} (ht : 2 < |t|) : Real.log |t| ≤ Real.log (|t| + 2)

theorem s_notin_ZetaZerosNearPoint (δ t : ℝ) (hδ_pos : 0 < δ) : 1 + ↑δ + ↑t * Complex.I ∉ ZetaZerosNearPoint t

theorem norm_sub_comm' (x y : ℂ) : ‖x - y‖ = ‖y - x‖

theorem s_in_closedBall_12 (δ t : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : 1 + ↑δ + ↑t * Complex.I ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (1 / 2)

theorem lem_explicit1deltat : ∃ C > 1, ∀ (t : ℝ), 2 < |t| → ∀ (δ : ℝ), 0 < δ ∧ δ < 1 → ‖∑ rho1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑δ + ↑t * Complex.I - rho1) - logDerivZeta (1 + ↑δ + ↑t * Complex.I)‖ ≤ C * Real.log (|t| + 2)

theorem lem_explicit1RealReal : ∃ C > 1, ∀ (t : ℝ), 2 < |t| → ∀ (δ : ℝ), 0 < δ ∧ δ < 1 → |(logDerivZeta (1 + ↑δ + ↑t * Complex.I)).re - ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑δ + ↑t * Complex.I - rho1)).re| ≤ C * Real.log (|t| + 2)

theorem lem_explicit2Real : ∃ C > 1, ∀ (t : ℝ), 2 < |t| → ∀ (δ : ℝ), 0 < δ ∧ δ < 1 → |(logDerivZeta (1 + ↑δ + 2 * ↑t * Complex.I)).re - ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑δ + 2 * ↑t * Complex.I - rho1)).re| ≤ C * Real.log (|2 * t| + 2)

theorem lem_Realsum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (s.sum f).re = ∑ i ∈ s, (f i).re

theorem lem_Ztfinite (t : ℝ) : (ZetaZerosNearPoint t).Finite

theorem lem_sumrho1 (t δ : ℝ) (hdelta_pos : δ > 0) (hdelta_lt1 : δ < 1) : (∑ rho1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑δ + ↑t * Complex.I - rho1)).re = ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑δ + ↑t * Complex.I - rho1)).re

theorem lem_sumrho2 (t delta : ℝ) (hdelta : delta > 0) (hdelta_lt1 : delta < 1) : (∑ rho1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + 2 * ↑t * Complex.I - rho1)).re = ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + 2 * ↑t * Complex.I - rho1)).re

theorem lem_1deltatrho1 (delta : ℝ) (_hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (_h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : 1 + ↑delta + ↑t * Complex.I - rho1 = ↑1 + ↑delta - ↑rho1.re + (↑t - ↑rho1.im) * Complex.I

theorem lem_Re1deltatrho1 (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : (1 + ↑delta + ↑t * Complex.I - rho1).re = 1 + delta - rho1.re

theorem lem_Re1delta1 (delta : ℝ) (_hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : 1 + delta - rho1.re ≥ delta

theorem lem_Re1deltatge (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : (1 + ↑delta + ↑t * Complex.I - rho1).re ≥ delta

theorem lem_Re1deltatneq0 (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : (1 + ↑delta + ↑t * Complex.I - rho1).re > 0

theorem lem_Re1deltatge0 (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : (1 / (1 + ↑delta + ↑t * Complex.I - rho1)).re ≥ 0

theorem lem_Re1deltatge0m (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (hdelta_lt_1 : delta < 1) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint t) : (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑t * Complex.I - rho1)).re ≥ 0

theorem lem_Re1delta2tge0 (delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) (t : ℝ) (rho1 : ℂ) (h_rho1_in_Zt : rho1 ∈ ZetaZerosNearPoint (2 * t)) : (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + 2 * ↑t * Complex.I - rho1)).re ≥ 0

theorem lem_sumrho2ge (t delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) : ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + 2 * ↑t * Complex.I - rho1)).re ≥ 0

theorem lem_sumrho2ge02 (t delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) : (∑ rho1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + 2 * ↑t * Complex.I - rho1)).re ≥ 0

theorem lem_explicit2Real2 : ∃ C > 1, ∀ (t : ℝ), 2 < |t| → ∀ (δ : ℝ), 0 < δ ∧ δ < 1 → (-logDerivZeta (1 + ↑δ + 2 * ↑t * Complex.I)).re ≤ C * Real.log (|2 * t| + 2)

theorem lem_log2Olog : (fun (t : ℝ) => Real.log (2 * t)) =O[Filter.atTop] fun (t : ℝ) => Real.log t

theorem lem_w2t (t : ℝ) : |2 * t| + 2 ≥ 0

theorem lem_log2Olog2 : (fun (t : ℝ) => Real.log (|2 * t| + 4)) =O[Filter.atTop ⊔ Filter.atBot] fun (t : ℝ) => Real.log (|t| + 2)

theorem lem_Z2bound : ∃ C > 1, ∀ (t : ℝ), 2 < |t| → ∀ (δ : ℝ), 0 < δ ∧ δ < 1 → (-logDerivZeta (1 + ↑δ + 2 * ↑t * Complex.I)).re ≤ C * Real.log (|t| + 2)

theorem lem_Z1split (delta : ℝ) (_hdelta : delta > 0) (hdelta : delta < 1) (rho : ℂ) (_h_rho_in_zeroZ : rho ∈ zeroZ) (h_rho_in_Zt : rho ∈ ZetaZerosNearPoint rho.im) : ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑rho.im * Complex.I - rho1)).re = (↑(analyticOrderAt riemannZeta rho).toNat / (1 + ↑delta + ↑rho.im * Complex.I - rho)).re + ∑ rho1 ∈ ⋯.toFinset.erase rho, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑rho.im * Complex.I - rho1)).re

theorem re_ofReal_mul_eq (a : ℝ) (z : ℂ) : (↑a * z).re = a * z.re

theorem re_ofReal_div_eq (a : ℝ) (z : ℂ) : (↑a / z).re = a * (1 / z).re

theorem re_ofReal_div_ge_one (a : ℝ) (z : ℂ) (ha : 1 ≤ a) (hz : 0 ≤ (1 / z).re) : (↑a / z).re ≥ (1 / z).re

theorem analyticAt_riemannZeta_of_ne_one {s : ℂ} (hs : s ≠ 1) : AnalyticAt ℂ riemannZeta s

theorem riemannZeta_not_eventually_zero_of_ne_one {s : ℂ} (hs : s ≠ 1) : ¬∀ᶠ (z : ℂ) in nhds s, riemannZeta z = 0

theorem analyticOrderAt_pos_toNat_of_zero_of_analytic_not_eventually_zero {f : ℂ → ℂ} {z0 : ℂ} (hf : AnalyticAt ℂ f z0) (hzero : f z0 = 0) (hnot : ¬∀ᶠ (z : ℂ) in nhds z0, f z = 0) : 1 ≤ (analyticOrderAt f z0).toNat

theorem lem_Z1splitge (delta : ℝ) (hdelta_pos : delta > 0) (hdelta : delta < 1) (rho : ℂ) (h_rho_in_zeroZ : rho ∈ zeroZ) (h_rho_in_Zt : rho ∈ ZetaZerosNearPoint rho.im) : ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑rho.im * Complex.I - rho1)).re ≥ (1 / (1 + ↑delta + ↑rho.im * Complex.I - rho)).re

theorem lem_1deltatrho0 (delta : ℝ) (_hdelta : delta > 0) (rho : ℂ) (_h_rho_in_zeroZ : rho ∈ zeroZ) : 1 + ↑delta + ↑rho.im * Complex.I - rho = ↑1 + ↑delta - ↑rho.re

theorem lem_1delsigReal (delta : ℝ) (hdelta_pos : delta > 0) (hdelta : delta < 1) (rho : ℂ) (h_rho_in_zeroZ : rho ∈ zeroZ) : (1 / (1 + ↑delta + ↑rho.im * Complex.I - rho)).re = 1 / (1 + delta - rho.re)

theorem lem_11delsiginR (delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) (sigma : ℝ) (hsigma : sigma ≤ 1) : (1 / (1 + ↑delta - ↑sigma)).im = 0

theorem lem_11delsiginR2 (delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) (rho : ℂ) (h_rho_in_zeroZ : rho ∈ zeroZ) : (1 / (1 + ↑delta - ↑rho.re)).im = 0

theorem lem_ReReal (x : ℝ) : (↑x).re = x

theorem lem_1delsigReal2 (delta : ℝ) (_hdelta : delta > 0) (rho : ℂ) (_h_rho_in_zeroZ : rho ∈ zeroZ) : (1 / (1 + ↑delta - ↑rho.re)).re = 1 / (1 + delta - rho.re)

theorem lem_re_inv_one_plus_delta_minus_rho_real (delta : ℝ) (hdelta : delta > 0) (rho : ℂ) (h_rho_in_zeroZ : rho ∈ zeroZ) : (1 / (1 + ↑delta + ↑rho.im * Complex.I - rho)).re = 1 / (1 + delta - rho.re)

theorem lem_Z1splitge2 (delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) (rho : ℂ) (h_rho_in_zeroZ : rho ∈ zeroZ) (h_rho_in_Zt : rho ∈ ZetaZerosNearPoint rho.im) : ∑ rho1 ∈ ⋯.toFinset, (↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑rho.im * Complex.I - rho1)).re ≥ 1 / (1 + delta - rho.re)

theorem lem_Z1splitge3 (delta : ℝ) (hdelta : delta > 0) (hdelta_lt_1 : delta < 1) (sigma t : ℝ) (rho : ℂ) (h_rho_eq : rho = ↑sigma + ↑t * Complex.I) (h_rho_in_zeroZ : rho ∈ zeroZ) (h_rho_in_Zt : rho ∈ ZetaZerosNearPoint t) : (∑ rho1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta rho1).toNat / (1 + ↑delta + ↑t * Complex.I - rho1)).re ≥ 1 / (1 + delta - sigma)

theorem lem_rho_in_Zt (delta : ℝ) (hdelta : delta > 0) (t : ℝ) (h_rho_zero : 1 + ↑delta + ↑t * Complex.I ∈ zeroZ) : 1 + ↑delta + ↑t * Complex.I ∈ ZetaZerosNearPoint t

theorem Z1bound : ∃ C > 1, ∀ (delta : ℝ), 0 < delta ∧ delta < 1 → ∀ (t : ℝ), 2 < |t| → ∀ (s : ℂ), s ∈ zeroZ ∧ s.im = t → (-logDerivZeta (1 + ↑delta + ↑t * Complex.I)).re ≤ -(1 / (1 + delta - s.re)) + C * Real.log (|t| + 2)

theorem Z0boundRe : (fun (delta : ℝ) => (-logDerivZeta (1 + ↑delta)).re - 1 / delta) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1

theorem extract_bigO_bound_Z0 (delta : ℝ) (_hdelta : delta > 0) : ∃ C0 > 0, (-logDerivZeta (1 + ↑delta)).re ≤ 1 / delta + C0

theorem uniform_bound_Z0 : ∃ δ0 > 0, ∃ C0 ≥ 0, ∀ (δ : ℝ), 0 < δ → δ < δ0 → (-logDerivZeta (1 + ↑δ)).re ≤ 1 / δ + C0

theorem eventually_atTop_sup_atBot_iff_abs {P : ℝ → Prop} : (∀ᶠ (t : ℝ) in Filter.atTop ⊔ Filter.atBot, P t) ↔ ∃ (T : ℝ), ∀ (t : ℝ), T ≤ |t| → P t

theorem re_sum_three (a b : ℝ) (x y z : ℂ) : (↑a * x + ↑b * y + z).re = a * x.re + b * y.re + z.re

theorem log_abs_add_two_ge_one (t : ℝ) (ht : Real.exp 1 - 2 ≤ |t|) : 1 ≤ Real.log (|t| + 2)

theorem log_abs_add_two_ge_of_threshold (K t : ℝ) (ht : Real.exp K - 2 ≤ |t|) : K ≤ Real.log (|t| + 2)

theorem re_ofReal_add_ofReal_add (a b : ℝ) (z : ℂ) : (↑a + ↑b + z).re = a + b + z.re

theorem algebraic_rewrite_RHS (δ s L C0 C1 C2 : ℝ) : 3 * (1 / δ + C0) + 4 * (-(1 / (1 + δ - s)) + C1 * L) + C2 * L = 3 / δ - 4 / (1 + δ - s) + (4 * C1 + C2) * L + 3 * C0

theorem absorb_pos_constant_into_log {L A c : ℝ} (hL : 1 ≤ L) (hc : 0 ≤ c) : A * L + c ≤ (A + c) * L

theorem neg_logDeriv_zeta_eq_vonMangoldt_sum (s : ℂ) (hs : 1 < s.re) : -(deriv riemannZeta s / riemannZeta s) = ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) * ↑n ^ (-s)

theorem zeta1zetaseries {s : ℂ} (hs : 1 < s.re) : -logDerivZeta s = ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) * ↑n ^ (-s)

theorem zeta1zetaseriesxy (x y : ℝ) (hx : 1 < x) : -logDerivZeta (↑x + ↑y * I) = ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) * ↑n ^ (-(↑x + ↑y * I))

theorem Zconverges1 (x y : ℝ) (hx : 1 < x) : riemannZeta (↑x + ↑y * I) ≠ 0

theorem complex_re_of_real_add_imag (x y : ℝ) : (↑x + ↑y * I).re = x

theorem vonMangoldt_LSeriesSummable (s : ℂ) (hs : 1 < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s

theorem summable_of_support_singleton {α : Type u_1} [SeminormedAddCommGroup α] (f : ℕ → α) (n₀ : ℕ) (h : ∀ (n : ℕ), n ≠ n₀ → f n = 0) : Summable f

theorem summable_of_summable_add_sub {α : Type u_1} [SeminormedAddCommGroup α] (f g h : ℕ → α) (h_eq : f = g + h) (hf : Summable f) (hh : Summable h) : Summable g

theorem LSeriesSummable_to_summable (f : ℕ → ℂ) (s : ℂ) (h : LSeriesSummable f s) : Summable fun (n : ℕ) => f n * ↑n ^ (-s)

theorem ReZconverges1 (x y : ℝ) (hx : 1 < x) : Summable fun (n : ℕ) => (↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-(↑x + ↑y * I))).re

theorem exprule (n : ℕ) (hn : n ≥ 1) (alpha beta : ℂ) : ↑n ^ (alpha + beta) = ↑n ^ alpha * ↑n ^ beta

theorem lem_nxy (n : ℕ) (hn : n ≥ 1) (x y : ℝ) : (↑n).cpow (-(↑x + ↑y * I)) = (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))

theorem lem_zeta1zetaseriesxy2 (x y : ℝ) (hx : 1 < x) : -logDerivZeta (↑x + ↑y * I) = ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))

theorem complex_add_re_ofReal_mul_I (x y : ℝ) : (↑x + ↑y * I).re = x

theorem LSeriesSummable_to_explicit_summable (x y : ℝ) (_hx : 1 < x) : LSeriesSummable (fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) (↑x + ↑y * I) → Summable fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))

theorem Zseriesconverges1 (x y : ℝ) (hx : 1 < x) : Summable fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))

theorem lem_realnx (n : ℕ) (x : ℝ) (_hn : n ≥ 1) (_hx : x ≥ 1) : ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) ≥ 0

theorem sumReal {v : ℕ → ℂ} {v_sum : ℂ} (h_sum : HasSum v v_sum) : HasSum (fun (n : ℕ) => (v n).re) v_sum.re

theorem sumRealLambda (x y : ℝ) (hx : 1 < x) : (∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))).re = ∑' (n : ℕ), (↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))).re

theorem lem_sumRealZ (x y : ℝ) (hx : 1 < x) : (-logDerivZeta (↑x + ↑y * I)).re = ∑' (n : ℕ), (↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))).re

theorem complex_cpow_neg_real (n : ℕ) (x : ℝ) (_hn : n ≥ 1) : (↑n).cpow (-↑x) = ↑(↑n ^ (-x))

theorem RealLambdaxy (n : ℕ) (x y : ℝ) (hn : n ≥ 1) (_hx : 1 < x) : (↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-↑x) * (↑n).cpow (-(↑y * I))).re = ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * ((↑n).cpow (-(↑y * I))).re

theorem ReZseriesRen (x y : ℝ) (hx : 1 < x) : (-logDerivZeta (↑x + ↑y * I)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * ((↑n).cpow (-(↑y * I))).re

theorem Rezeta1zetaseries (x y : ℝ) (hx : 1 < x) : (-logDerivZeta (↑x + ↑y * I)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * Real.cos (y * Real.log ↑n)

theorem complex_vonMangoldt_real_part_eq (n : ℕ) (x y : ℝ) (hn : n ≥ 1) (hx : 1 < x) : (↑(ArithmeticFunction.vonMangoldt n) * (↑n).cpow (-(↑x + ↑y * I))).re = ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * Real.cos (y * Real.log ↑n)

theorem Rezetaseries_convergence (x y : ℝ) (hx : 1 < x) : Summable fun (n : ℕ) => ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * Real.cos (y * Real.log ↑n)

theorem Rezetaseries2t (x t : ℝ) (hx : 1 < x) : Summable fun (n : ℕ) => ArithmeticFunction.vonMangoldt n * ↑n ^ (-x) * Real.cos (2 * t * Real.log ↑n)

theorem lem_cost0 (n : ℕ) (_hn : n ≥ 1) (t : ℝ) (ht : t = 0) : Real.cos (t * Real.log ↑n) = 1

theorem Rezetaseries0 (x : ℝ) (hx : 1 < x) : Summable fun (n : ℕ) => ArithmeticFunction.vonMangoldt n * ↑n ^ (-x)

theorem uniform_bound_Z0_complex : ∃ δ0 > 0, ∃ C0 ≥ 0, ∀ (δ : ℝ), 0 < δ → δ < δ0 → ‖-logDerivZeta (1 + ↑δ) - 1 / ↑δ‖ ≤ C0

theorem cpow_neg_zero_I (z : ℂ) : z ^ (-↑0 * Complex.I) = 1

theorem tsum_nonneg_of_nonneg {f : ℕ → ℝ} (hnon : ∀ (n : ℕ), 0 ≤ f n) : 0 ≤ ∑' (n : ℕ), f n

theorem vonMangoldt_rpow_nonneg (x : ℝ) (n : ℕ) : 0 ≤ ArithmeticFunction.vonMangoldt n * ↑n ^ (-x)

theorem cpow_neg_real_of_nat (n : ℕ) (x : ℝ) (hn : 1 ≤ n) : ↑n ^ (-↑x) = ↑(↑n ^ (-x))

theorem norm_negLogDerivZeta_real_eq_abs_tsum_vonMangoldt (x : ℝ) (hx : 1 < x) : ‖-logDerivZeta ↑x‖ = |∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-x)|

theorem tsum_le_of_nonneg_of_le {f g : ℕ → ℝ} (hf : Summable f) (hg : Summable g) (_hnonneg : ∀ (n : ℕ), 0 ≤ f n) (hle : ∀ (n : ℕ), f n ≤ g n) : ∑' (n : ℕ), f n ≤ ∑' (n : ℕ), g n

theorem rpow_neg_antitone {a x y : ℝ} (ha : 1 ≤ a) (hxy : x ≥ y) : a ^ (-x) ≤ a ^ (-y)

theorem isPrimePow_zero_false : IsPrimePow 0 = False

theorem bounded_on_compact_interval (a b : ℝ) (h0 : 0 < a) (_hle : a ≤ b) : ∃ Cmid ≥ 0, ∀ (δ : ℝ), a ≤ δ → δ ≤ b → ‖-logDerivZeta (1 + ↑δ) - 1 / ↑δ‖ ≤ Cmid

theorem norm_one_div_coe_real_le_one_of_one_le {δ : ℝ} (h : 1 ≤ δ) : ‖1 / ↑δ‖ ≤ 1

theorem Z0bound_const : ∃ C > 1, ∀ δ > 0, ‖-logDerivZeta (1 + ↑δ) - 1 / ↑δ‖ ≤ C

There exists a constant C > 0 such that for all δ > 0, ‖ -logDerivZeta (1 + δ) - 1/δ ‖ ≤ C.

theorem Z0boundRe_const : ∃ C > 1, ∀ δ > 0, (-logDerivZeta (1 + ↑δ) - 1 / ↑δ).re ≤ C

There exists a constant C > 0 such that for all δ > 0, Re(-logDerivZeta (1 + δ) - 1/δ) ≤ C.

theorem Z0boundRe_const2 : ∃ C > 1, ∀ δ > 0, (-logDerivZeta (1 + ↑δ)).re + (-(1 / ↑δ)).re ≤ C

There exists a constant C > 0 such that for all δ > 0, Re(-logDerivZeta (1 + δ)) + Re(- 1/δ) ≤ C.

theorem Z0boundRe_const3 : ∃ C > 1, ∀ δ > 0, (-logDerivZeta (1 + ↑δ)).re - 1 / δ ≤ C

There exists a constant C > 0 such that for all δ > 0, Re(-logDerivZeta (1 + δ)) - 1/δ ≤ C.

theorem Z341bounds_const : ∃ C > 1, ∀ δ > 0, δ < 1 → ∀ (t : ℝ), 2 < |t| → ∀ (σ : ℝ), ↑σ + ↑t * Complex.I ∈ zeroZ → 3 * (-logDerivZeta (1 + ↑δ)).re + 4 * (-logDerivZeta (1 + ↑δ + ↑t * Complex.I)).re + (-logDerivZeta (1 + ↑δ + 2 * ↑t * Complex.I)).re ≤ 3 / δ - 4 / (1 + δ - σ) + C * Real.log (|t| + 2)

def ZeroAt (σ t : ℝ) : Prop

Equations

• ZeroAt σ t = (↑σ + ↑t * I ∈ zeroZ)

def Ft (σ : ℝ) : Filter ℝ

Equations

• Ft σ = (Filter.atTop ⊔ Filter.atBot) ⊓ Filter.principal {t : ℝ | ZeroAt σ t}

def Fδ : Filter ℝ

Filter on δ: approach 0⁺.

Equations

• Fδ = nhdsWithin 0 (Set.Ioi 0)

theorem Rezeta1zetaseries1 (t delta : ℝ) (hdelta : delta > 0) : (-logDerivZeta (1 + ↑delta + ↑t * I)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (t * Real.log ↑n)

theorem Rezeta1zetaseries2 (t delta : ℝ) (hdelta : delta > 0) : (-logDerivZeta (1 + ↑delta + 2 * ↑t * I)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (2 * t * Real.log ↑n)

theorem Rezeta1zetaseries0 (delta : ℝ) (hdelta : delta > 0) : (-logDerivZeta (1 + ↑delta)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta))

theorem Z341series (t delta : ℝ) (hdelta : delta > 0) : 3 * (-logDerivZeta (1 + ↑delta)).re + 4 * (-logDerivZeta (1 + ↑delta + ↑t * I)).re + (-logDerivZeta (1 + ↑delta + 2 * ↑t * I)).re = 3 * ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) + 4 * ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (t * Real.log ↑n) + ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (2 * t * Real.log ↑n)

theorem lem341seriesConv (t delta : ℝ) (hdelta : delta > 0) : Summable fun (n : ℕ) => 3 * ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) + 4 * ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (t * Real.log ↑n) + ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (2 * t * Real.log ↑n)

theorem lem341series (t delta : ℝ) (hdelta : delta > 0) : 3 * ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) + 4 * ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (t * Real.log ↑n) + ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * Real.cos (2 * t * Real.log ↑n) = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * (3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n))

theorem lem_341seriesConverge (t delta : ℝ) (hdelta : delta > 0) : Summable fun (n : ℕ) => ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * (3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n))

theorem lem_341series2 (t delta : ℝ) (hdelta : delta > 0) : 3 * (-logDerivZeta (1 + ↑delta)).re + 4 * (-logDerivZeta (1 + ↑delta + ↑t * I)).re + (-logDerivZeta (1 + ↑delta + 2 * ↑t * I)).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * (3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n))

theorem lem_Lambda_pos_trig_sum (n : ℕ) (delta t : ℝ) (hn : n ≥ 1) (hdelta : delta > 0) : 0 ≤ ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * (3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n))

theorem seriesPos {f : ℕ → ℝ} (_h_summable : Summable fun (n : ℕ) => if 1 ≤ n then f n else 0) (h_nonneg : ∀ (n : ℕ), 1 ≤ n → 0 ≤ f n) : 0 ≤ ∑' (n : ℕ), if 1 ≤ n then f n else 0

theorem lem_seriespos (t delta : ℝ) (hdelta : delta > 0) : 0 ≤ ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * ↑n ^ (-(1 + delta)) * (3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n))

theorem Z341pos (t delta : ℝ) (hdelta : delta > 0) : 0 ≤ 3 * (-logDerivZeta (1 + ↑delta)).re + 4 * (-logDerivZeta (1 + ↑delta + ↑t * I)).re + (-logDerivZeta (1 + ↑delta + 2 * ↑t * I)).re

theorem frac_den_increase_bound {a b c : ℝ} (hpos : 0 < a + b) (hc : 0 ≤ c) : 4 / (a + b + c) ≤ 4 / (a + b)

theorem log_abs_add_two_pos (t : ℝ) : 0 < Real.log (|t| + 2)

theorem log_gt_of_gt_exp {x y : ℝ} (h : Real.exp y < x) : y < Real.log x

theorem denom_rewrite (σ C L : ℝ) : 1 - σ + 1 / (2 * C * L) = 1 + 1 / (2 * C * L) - σ

theorem pos_delta_from_C_L {C L : ℝ} (hC : 0 < C) (hL : 0 < L) : 0 < 1 / (2 * C * L)

theorem add_two_pos_of_abs (t : ℝ) : 0 < |t| + 2

theorem log_abs_two_pos (t : ℝ) : 0 < Real.log (|t| + 2)

theorem two_C_log_pos {C t : ℝ} (hC : 0 < C) : 0 < 2 * C * Real.log (|t| + 2)

theorem mul_one_div_self_of_pos {a : ℝ} (ha : 0 < a) : a * (1 / a) = 1

theorem mul_one_div_mul_right {A b : ℝ} (hA : A ≠ 0) : A * (1 / (A * b)) = 1 / b

theorem one_div_mul_one_div_mul_right {A b : ℝ} (hA : A ≠ 0) (_hb : b ≠ 0) : 1 / (A * (1 / (A * b))) = b

theorem inv_of_delta_def (C L δ : ℝ) (hδ : δ = 1 / (2 * C * L)) : 1 / δ = 2 * C * L

theorem rhs_eval_of_inv (C L δ : ℝ) (h : 1 / δ = 2 * C * L) : 3 / δ + C * L = 7 * C * L

theorem lem341tsC : ∃ C > 1, ∀ (s : ℂ), s ∈ zeroZ ∧ 0 < s.re ∧ s.re < 1 → 2 < |s.im| → 4 / (1 - s.re + 1 / (2 * C * Real.log (|s.im| + 2))) ≤ 7 * C * Real.log (|s.im| + 2)

theorem zeta_zero_re_lt_one (s : ℂ) (hs : s ∈ zeroZ) : s.re < 1

theorem div_le_to_le_mul (x y z : ℝ) (hy : 0 < y) (h : x / y ≤ z) : x ≤ z * y

theorem le_mul_to_le_div (x y z : ℝ) (hy : 0 < y) (h : x ≤ z * y) : x / y ≤ z

theorem reciprocal_div_inequality (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (h : 4 / a ≤ b) : a ≥ 4 / b

theorem lem341tsC2 : ∃ C > 1, ∀ (s : ℂ), s ∈ zeroZ ∧ 0 < s.re ∧ s.re < 1 → 2 < |s.im| → 1 - s.re + 1 / (2 * C * Real.log (|s.im| + 2)) ≥ 4 / (7 * C * Real.log (|s.im| + 2))

theorem simplify_4_7_2 (C L : ℝ) : 4 / (7 * C * L) - 1 / (2 * C * L) = 1 / (14 * C * L)

theorem fraction_diff_lower_bound (C L a : ℝ) : 4 / (7 * C * L) ≤ a + 1 / (2 * C * L) → 1 / (14 * C * L) ≤ a

theorem lem341tsC3 : ∃ C > 1, ∀ (s : ℂ), s ∈ zeroZ ∧ 0 < s.re ∧ s.re < 1 → 2 < |s.im| → 1 - s.re ≥ 1 / (14 * C * Real.log (|s.im| + 2))

theorem zerofree : ∃ c > 0, c < 1 ∧ ∀ (s : ℂ), s ∈ zeroZ ∧ 0 < s.re ∧ s.re < 1 → 2 < |s.im| → s.re ≤ 1 - c / Real.log (|s.im| + 2)

def Yt (t δ : ℝ) : Set ℂ

For $t\in\R$ and $\delta >0$, define $\mathcal{Y}_t(\delta) = \{\rho_1\in\C : \zeta(\rho_1) = 0 \,\text{and} \, |\rho_1-(1-\delta+it)|\le \delta/2\}.$

Equations

• Yt t δ = {ρ_1 : ℂ | riemannZeta ρ_1 = 0 ∧ ‖ρ_1 - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ}

noncomputable def zerofree_constant : ℝ

Equations

• zerofree_constant = Classical.choose zerofree

theorem zerofree_constant_pos : 0 < zerofree_constant

theorem zerofree_constant_lt_one : zerofree_constant < 1

noncomputable def deltaz (z : ℂ) : ℝ

Equations

• deltaz z = zerofree_constant / 20 / Real.log (|z.im| + 2)

noncomputable def deltaz_t (t : ℝ) : ℝ

Equations

• deltaz_t t = deltaz (↑t * Complex.I)

theorem lem_delta19 : (∀ (z : ℂ), |z.im| > 2 → 0 < deltaz z ∧ deltaz z < 1 / 9) ∧ ∀ (t : ℝ), |t| > 2 → 0 < deltaz_t t ∧ deltaz_t t < 1 / 9

theorem closedBall_compact_complex (c : ℂ) (r : ℝ) : IsCompact (Metric.closedBall c r)

theorem riemannZeta_no_zeros_accumulate_at_one (Z : Set ℂ) : (∀ z ∈ Z, riemannZeta z = 0) → ¬AccPt 1 (Filter.principal Z)

theorem complex_minus_singleton_connected : IsPreconnected {s : ℂ | s ≠ 1}

theorem eventually_eq_zero_implies_frequently_eq_zero_punctured (f : ℂ → ℂ) (z₀ : ℂ) : (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) → ∃ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0

theorem riemannZeta_zeros_finite_of_compact (K : Set ℂ) (hK : IsCompact K) : {z : ℂ | z ∈ K ∧ riemannZeta z = 0}.Finite

theorem lem_ZFRdelta (z : ℂ) : 2 < |z.im| → z.re > 1 - 9 * deltaz z → riemannZeta z ≠ 0

theorem complex_re_add_I_mul_real (a t : ℝ) : (↑a + Complex.I * ↑t).re = a

theorem complex_im_add_I_mul_real (a t : ℝ) : (↑a + Complex.I * ↑t).im = t

theorem complex_sub_ofReal_I_real_eq_ofReal (z : ℂ) (a t : ℝ) (him : z.im = t) : z - (↑a + Complex.I * ↑t) = ↑z.re - ↑a

theorem lem_ZFRinD (t : ℝ) (ht : |t| > 2) (z : ℂ) : let c := 3 / 2 + I * ↑t; 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → z ∈ Metric.closedBall c (2 / 3)

theorem lem_ZFRnotK (t : ℝ) (ht : |t| > 2) (z : ℂ) : let c := 3 / 2 + I * ↑t; 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → z ∉ zerosetKfRc (5 / 6) c riemannZeta

theorem lem_Zeta_Expansion_ZFR : ∃ C_1 > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite) (z : ℂ), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ‖deriv riemannZeta z / riemannZeta z - ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ ≤ C_1 * Real.log |t|

theorem lem_abszrhoReRe (z ρ : ℂ) : ‖z - ρ‖ ≥ z.re - ρ.re

theorem lem_Rerhotodeltarho {ρ : ℂ} (t : ℝ) : |t| > 3 → ρ ∈ zerosetKfRc (5 / 6) (3 / 2 + ↑t * Complex.I) riemannZeta → ρ.re ≤ 1 - 9 * deltaz ρ

theorem lem_DImt2d (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (5 / 6), |z.im| ≤ |t| + 5 / 6

theorem lem_DIMt2 (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (5 / 6), |z.im| + 2 ≤ (|t| + 2) ^ 3

theorem lem_DlogImlog (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (5 / 6), Real.log (|z.im| + 2) ≤ 3 * Real.log (|t| + 2)

theorem lem_D1logtlog (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (5 / 6), 1 / Real.log (|t| + 2) ≤ 3 / Real.log (|z.im| + 2)

theorem lem_Ddt2dz (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (3 / 2 + ↑t * Complex.I) (5 / 6), deltaz_t t ≤ 3 * deltaz z

theorem lem_deltarhotodeltat (t : ℝ) (ht : |t| > 3) (ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → deltaz ρ ≥ 1 / 3 * deltaz_t t

theorem lem_Rerhotodeltat (t : ℝ) (ht : |t| > 3) (ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → ρ.re ≤ 1 - 3 * deltaz_t t

theorem lem_RezRerho (t : ℝ) (ht : |t| > 3) (z ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → z.re - ρ.re ≥ 2 * deltaz_t t

theorem lem_abszrhodelta (t : ℝ) (ht : |t| > 3) (z ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ‖z - ρ‖ ≥ 2 * deltaz_t t

theorem lem_abszrhodeltanot0 (t : ℝ) (ht : |t| > 3) (z ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ‖z - ρ‖ > 0

theorem lem_1abszrho (t : ℝ) (ht : |t| > 3) (z ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → 1 / ‖z - ρ‖ ≤ 1 / (2 * deltaz_t t)

theorem lem_m_rho_zeta_nat (t : ℝ) (ht : |t| > 3) (ρ : ℂ) : let c := 3 / 2 + I * ↑t; ρ ∈ zerosetKfRc (5 / 6) c riemannZeta → ∃ (n : ℕ), analyticOrderAt riemannZeta ρ = ↑n

theorem lem_finiteKzeta (t : ℝ) (ht : |t| > 3) : let c := 3 / 2 + I * ↑t; (zerosetKfRc (5 / 6) c riemannZeta).Finite

theorem lem_triangle_ZFR (t : ℝ) (ht : |t| > 3) (z : ℂ) : let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ‖∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ ≤ ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / ‖z - ρ‖

theorem lem_Zeta_Triangle_ZFR : ∃ C_1 > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite) (z : ℂ), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ‖deriv riemannZeta z / riemannZeta z‖ ≤ ‖∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ + C_1 * Real.log |t|

theorem lem_sumK1abs (t : ℝ) (ht : |t| > 3) (z : ℂ) : let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / ‖z - ρ‖ ≤ 1 / (2 * deltaz_t t) * ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat

theorem helper_analyticOnNhd_shift_div (f : ℂ → ℂ) (c : ℂ) (h : ∀ z ∈ Metric.closedBall c 1, AnalyticAt ℂ f z) (hc : f c ≠ 0) : AnalyticOnNhd ℂ (fun (z : ℂ) => f (z + c) / f c) (Metric.closedBall 0 1)

theorem helper_finite_zeros_shift (r : ℝ) (hr : r > 0) (c : ℂ) (f : ℂ → ℂ) (hc : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (hfin : (zerosetKfRc r c f).Finite) : (zerosetKfRc r 0 fun (z : ℂ) => f (z + c) / f c).Finite

theorem helper_bound_shifted (B R : ℝ) (hB : 1 < B) (hRpos : 0 < R) (hRlt1 : R < 1) (c : ℂ) (f : ℂ → ℂ) (hc : f c ≠ 0) (h_bound : ∀ z ∈ Metric.closedBall c R, ‖f z‖ ≤ B) (z : ℂ) : z ∈ Metric.closedBall 0 R → ‖(fun (w : ℂ) => f (w + c) / f c) z‖ ≤ B / ‖f c‖

theorem helper_g_zero_eq_one (f : ℂ → ℂ) (c : ℂ) (hc : f c ≠ 0) : (fun (z : ℂ) => f (z + c) / f c) 0 = 1

theorem helper_zerosetKfR_eq_center0 (r : ℝ) (hr : r > 0) (f : ℂ → ℂ) : zerosetKfR r hr f = zerosetKfRc r 0 f

theorem helper_sum_nonneg_nat (ι : Type u_1) (s : Finset ι) (f : ι → ℕ) : 0 ≤ ∑ i ∈ s, ↑(f i)

theorem helper_one_le_Bdivfc2 (B R : ℝ) (hB : 1 < B) (hRpos : 0 < R) (hRlt1 : R < 1) (f : ℂ → ℂ) (c : ℂ) (hc : f c ≠ 0) (h_bound : ∀ z ∈ Metric.closedBall c R, ‖f z‖ ≤ B) : 1 ≤ B / ‖f c‖

theorem helper_sum_over_equal_finite_sets {α : Type u_1} (S T : Set α) (hS : S.Finite) (hT : T.Finite) (hST : S = T) (φ : α → ℝ) : ∑ x ∈ hS.toFinset, φ x = ∑ x ∈ hT.toFinset, φ x

theorem helper_apply_jensen_to_g (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (g : ℂ → ℂ) (h_g_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ g z) (hg0_ne : g 0 ≠ 0) (hg0_one : g 0 = 1) (hfin_g : (zerosetKfR R1 ⋯ g).Finite) (hg_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖g z‖ ≤ B) : ∑ ρ ∈ hfin_g.toFinset, ↑(analyticOrderAt g ρ).toNat ≤ Real.log B / Real.log (R / R1)

theorem helper_sum_f_equals_sum_g (r : ℝ) (hr : r > 0) (c : ℂ) (f : ℂ → ℂ) (hc : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (hfin : (zerosetKfRc r c f).Finite) : ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt f ρ).toNat = ∑ ρ' ∈ ⋯.toFinset, ↑(analyticOrderAt (fun (z : ℂ) => f (z + c) / f c) ρ').toNat

theorem helper_zero_set_shift_eq (r : ℝ) (hr : r > 0) (c : ℂ) (f : ℂ → ℂ) (hc : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) : (zerosetKfRc r 0 fun (z : ℂ) => f (z + c) / f c) = (fun (ρ : ℂ) => ρ - c) '' zerosetKfRc r c f

theorem helper_fin_zero_g_is_image (r : ℝ) (hr : r > 0) (c : ℂ) (f : ℂ → ℂ) (hc : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (hfin : (zerosetKfRc r c f).Finite) : (zerosetKfRc r 0 fun (z : ℂ) => f (z + c) / f c).Finite

theorem helper_AnalyticOnNhd_to_pointwise {S : Set ℂ} {f : ℂ → ℂ} (h : AnalyticOnNhd ℂ f S) (z : ℂ) : z ∈ S → AnalyticAt ℂ f z

theorem jensen_sum_bound_strict (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (g : ℂ → ℂ) (h_g_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ g z) (hg0_ne : g 0 ≠ 0) (hg0_one : g 0 = 1) (hfin_g : (zerosetKfR R1 ⋯ g).Finite) (hg_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖g z‖ ≤ B) : ∑ ρ ∈ hfin_g.toFinset, ↑(analyticOrderAt g ρ).toNat ≤ Real.log B / Real.log (R / R1)

theorem no_zero_of_bound_one_and_center_one (R : ℝ) (hR_lt_1 : R < 1) (g : ℂ → ℂ) (h_g_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ g z) (hg0_one : g 0 = 1) (hg_le_one : ∀ (z : ℂ), ‖z‖ ≤ R → ‖g z‖ ≤ 1) (z : ℂ) : z ∈ Metric.closedBall 0 R → g z ≠ 0

theorem helper_sum_over_equal_finite_sets_orders {S T : Set ℂ} (g : ℂ → ℂ) (hS : S.Finite) (hT : T.Finite) (hST : S = T) : ∑ x ∈ hS.toFinset, ↑(analyticOrderAt g x).toNat = ∑ x ∈ hT.toFinset, ↑(analyticOrderAt g x).toNat

theorem helper_mem_closedBall_zero_iff_norm_le (z : ℂ) (R : ℝ) : z ∈ Metric.closedBall 0 R ↔ ‖z‖ ≤ R

theorem helper_bound_on_ball_to_norm_imp {R : ℝ} {g : ℂ → ℂ} {M : ℝ} (hg : ∀ z ∈ Metric.closedBall 0 R, ‖g z‖ ≤ M) (z : ℂ) : ‖z‖ ≤ R → ‖g z‖ ≤ M

theorem helper_pointwise_to_AnalyticOnNhd {S : Set ℂ} {f : ℂ → ℂ} (h : ∀ z ∈ S, AnalyticAt ℂ f z) : AnalyticOnNhd ℂ f S

theorem lem_sum_m_rho_bound_c (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (c : ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall c 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f c ≠ 0) (hf_le_B : ∀ z ∈ Metric.closedBall c R, ‖f z‖ ≤ B) (hfin : (zerosetKfRc R1 c f).Finite) : ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt f ρ).toNat ≤ Real.log (B / ‖f c‖) / Real.log (R / R1)

theorem lem_sum_m_rho_zeta : ∃ C_2 > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite), ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat ≤ C_2 * Real.log |t|

theorem lem_sumKdeltatlogt : ∃ C_3 > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite) (z : ℂ), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / ‖z - ρ‖ ≤ C_3 / deltaz_t t * Real.log |t|

theorem lem_sumKlogt2 : ∃ C_4 > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite) (z : ℂ), 1 - deltaz_t t ≤ z.re ∧ z.re ≤ 3 / 2 ∧ z.im = t → ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / ‖z - ρ‖ ≤ C_4 * Real.log |t| ^ 2

theorem lem_logDerivZetalogt0 : ∃ C > 1, ∀ (t : ℝ), |t| > 3 → ∀ (s : ℂ), 1 - deltaz_t t ≤ s.re ∧ s.re ≤ 3 / 2 ∧ s.im = t → ‖deriv riemannZeta s / riemannZeta s‖ ≤ C * Real.log |t| ^ 2

theorem lem_logDerivZetalogt2 : ∃ A > 0, A < 1 ∧ ∃ C > 1, ∀ (t : ℝ), |t| > 3 → ∀ (s : ℂ), 1 - A / Real.log (|t| + 2) ≤ s.re ∧ s.re ≤ 3 / 2 ∧ s.im = t → ‖deriv riemannZeta s / riemannZeta s‖ ≤ C * Real.log |t| ^ 2

theorem lem_rhoDRe4 (t : ℝ) (z : ℂ) : z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t) → z.re > 1 - 4 * deltaz_t t

theorem helper_absIm_le_add_smallball (t : ℝ) (z : ℂ) (hz : z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t)) : |z.im| ≤ |t| + 2 * deltaz_t t

theorem helper_log_le_two_log_smallball (t : ℝ) (ht : |t| > 3) (z : ℂ) (hz : z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t)) : Real.log (|z.im| + 2) ≤ 2 * Real.log (|t| + 2)

theorem helper_one_div_log_le_two_div_smallball (t : ℝ) (ht : |t| > 3) (z : ℂ) (hz : z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t)) : 1 / Real.log (|t| + 2) ≤ 2 / Real.log (|z.im| + 2)

theorem helper_deltaz_t_le_two_deltaz_smallball (t : ℝ) (ht : |t| > 3) (z : ℂ) (hz : z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t)) : deltaz_t t ≤ 2 * deltaz z

theorem lem_DRez6dz (t : ℝ) : |t| > 3 → ∀ z ∈ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t), z.re ≥ 1 - 6 * deltaz z

theorem lem_YinD (t : ℝ) : |t| > 3 → Yt t (deltaz_t t) ⊆ Metric.closedBall (1 - ↑(deltaz_t t) + ↑t * Complex.I) (2 * deltaz_t t)

theorem lem_rhoYzero (t δ : ℝ) (ρ_1 : ℂ) (h_rho_1_in_Yt : ρ_1 ∈ Yt t δ) : riemannZeta ρ_1 = 0

theorem lem_absReabs (w : ℂ) : |w.re| ≤ ‖w‖

theorem lem_zRe (t δ : ℝ) (z : ℂ) : |(z - (1 - ↑δ + ↑t * Complex.I)).re| ≤ ‖z - (1 - ↑δ + ↑t * Complex.I)‖

theorem lem_zRe2 (t δ : ℝ) (z : ℂ) (h_le : ‖z - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ) : |(z - (1 - ↑δ + ↑t * Complex.I)).re| ≤ 2 * δ

theorem lem_Rezit (t δ : ℝ) (z : ℂ) : (z - (1 - ↑δ + ↑t * Complex.I)).re = z.re - (1 - δ)

theorem lem_zRe3 (t δ : ℝ) (z : ℂ) (h_le : ‖z - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ) : |z.re - (1 - δ)| ≤ 2 * δ

theorem lem_negleabs (a b : ℝ) (h_abs : |a| ≤ b) : a ≥ -b

Let $a\in\R$ and $b>0$. If $|a|\le b$ then $a\ge -b$.

theorem lem_absrez1d (δ : ℝ) (z : ℂ) (h_le : |z.re - (1 - δ)| ≤ 2 * δ) : z.re - (1 - δ) ≥ -(2 * δ)

Let $\delta >0$ and $z\in \C$. If $|\Re(z)-(1-\delta)| \le \delta/2$ then $\Re(z)-(1-\delta) \ge -\delta/2$

theorem lem_absrez1d2 (δ : ℝ) (z : ℂ) (h_le : |z.re - (1 - δ)| ≤ 2 * δ) : z.re ≥ 1 - 3 * δ

Let $\delta >0$ and $z\in \C$. If $|\Re(z)-(1-\delta)| \le \delta/2$ then $\Re(z) \ge 1-\frac{3}{2}\delta$

theorem lem_absrez1d3 (δ : ℝ) (z : ℂ) (hδ : δ > 0) (h_le : |z.re - (1 - δ)| ≤ 2 * δ) : z.re > 1 - 4 * δ

theorem lem_zRe4 (t δ : ℝ) (hδ : δ > 0) (z : ℂ) (h_le : ‖z - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ) : z.re > 1 - 4 * δ

theorem riemannZeta_no_zeros_left_halfplane_off_real_axis (s : ℂ) (h_re : s.re ≤ 0) (h_im : s.im ≠ 0) : riemannZeta s ≠ 0

theorem lem_Imzit (t δ : ℝ) (z : ℂ) : (z - (1 - ↑δ + ↑t * Complex.I)).im = z.im - t

theorem lem_zIm2 (t δ : ℝ) (z : ℂ) (h_le : ‖z - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ) : |(z - (1 - ↑δ + ↑t * Complex.I)).im| ≤ 2 * δ

theorem lem_zIm3 (t δ : ℝ) (z : ℂ) (h_le : ‖z - (1 - ↑δ + ↑t * Complex.I)‖ ≤ 2 * δ) : |z.im - t| ≤ 2 * δ

theorem abs_le_add_of_abs_sub_le {a b ε : ℝ} (h : |a - b| ≤ ε) : |a| ≤ |b| + ε

theorem log_add_lt_log_add_div {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : Real.log (x + y) < Real.log x + y / x

theorem abs_le_add_of_abs_sub_le' {a b ε : ℝ} (h : |a - b| ≤ ε) : |a| ≤ |b| + ε

theorem delta_half_eq (c t : ℝ) : c / 2 / Real.log (|t| + 2) / 2 = c / 4 / Real.log (|t| + 2)

theorem log_abs_im_le (t t1 δ : ℝ) (h : |t1 - t| ≤ δ) : Real.log (|t1| + 2) ≤ Real.log (|t| + 2) + δ / (|t| + 2)

theorem combine_re_bounds_to_c_over_log_le {ρre c δ L1 : ℝ} (h_ge : ρre ≥ 1 - 3 / 2 * δ) (h_le : ρre ≤ 1 - c / L1) : c / L1 ≤ 3 / 2 * δ

theorem core_contradiction2 {L t c δ : ℝ} (hLpos : 0 < L) (hpos : 0 < |t| + 2) (hδ : δ = c / 2 / L) (h : L ≤ 3 / 2 * δ / (|t| + 2)) : L ^ 2 * (|t| + 2) ≤ 3 * c / 4

theorem abs_lower_bound_sub (x y : ℝ) : |x| ≥ |y| - |x - y|

theorem abs_im_ge_T0_from_close {t : ℝ} {ρ : ℂ} {δ T0 : ℝ} (hclose : |ρ.im - t| ≤ 2 * δ) (hineq : |t| - 2 * δ ≥ T0) : T0 ≤ |ρ.im|

theorem lem_Kzetaempty (t : ℝ) : |t| > 3 → Yt t (deltaz_t t) = ∅

theorem Yt_subset_closedBall (t δ : ℝ) : Yt t δ ⊆ Metric.closedBall (1 - ↑δ + ↑t * Complex.I) (2 * δ)

theorem Yt_finite (t δ : ℝ) : (Yt t δ).Finite

theorem lem_sumempty (g : ℂ → ℂ) : ∑ s ∈ ∅, g s = 0

For any $g:\C\to\C$, if $S=\emptyset$ then $\sum_{s\in S}g(s) = 0$

theorem lem_Ksumempty (t : ℝ) : |t| > 3 → ∑ ρ_1 ∈ ⋯.toFinset, ↑(analyticOrderAt riemannZeta ρ_1).toNat / (1 - ↑(deltaz_t t) + ↑t * Complex.I - ρ_1) = 0

theorem norm_div_cast_vonMangoldt (s : ℂ) : (fun (n : ℕ) => ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s‖) = fun (n : ℕ) => |ArithmeticFunction.vonMangoldt n| / ‖↑n ^ s‖

theorem ArithmeticFunction.summable_vonMangoldt_norm_rw {s : ℂ} : (Summable fun (n : ℕ) => ‖↑(vonMangoldt n) / ↑n ^ s‖) ↔ Summable fun (n : ℕ) => |vonMangoldt n| / ‖↑n ^ s‖

theorem lem_norm_cpow_nat (n : ℕ) (s : ℂ) (hn : 1 ≤ n) : ‖↑n ^ s‖ = ↑n ^ s.re

theorem lem_vonMangoldt_nonneg (n : ℕ) : 0 ≤ ArithmeticFunction.vonMangoldt n

theorem lem_term_real_nonneg (n : ℕ) (σ : ℝ) (hσ : 1 < σ) : ∃ r ≥ 0, ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ ↑σ = ↑r

theorem lem_tsum_norm_vonMangoldt_depends_on_Re (s : ℂ) (σ : ℝ) (hσ : σ = s.re) (hs : 1 < s.re) : ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s‖ = ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ ↑σ‖

theorem helper_LSeries_vonMangoldt_tsum (σ : ℝ) (hσ : 1 < σ) : ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ ↑σ = -deriv riemannZeta ↑σ / riemannZeta ↑σ

theorem summable_ofReal_iff {f : ℕ → ℝ} : (Summable fun (n : ℕ) => ↑(f n)) ↔ Summable f

theorem helper_summable_of_summable_norm {u : ℕ → ℂ} (h : Summable fun (n : ℕ) => ‖u n‖) : Summable u

theorem helper_norm_tsum_eq_tsum_norm_of_nonneg_real {u : ℕ → ℂ} {r : ℕ → ℝ} (h : ∀ (n : ℕ), u n = ↑(r n)) (hr : ∀ (n : ℕ), 0 ≤ r n) (hu : Summable u) : ‖∑' (n : ℕ), u n‖ = ∑' (n : ℕ), ‖u n‖

theorem lem_norm_logDeriv_le_tsum (s : ℂ) (hs : 1 < s.re) : ‖deriv riemannZeta s / riemannZeta s‖ ≤ ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s‖

theorem lem_tsum_norm_vonMangoldt_depends_on_Re_cast (s : ℂ) (σ : ℝ) (hσ : σ = s.re) (hs : 1 < s.re) : ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s‖ = ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ ↑σ‖

theorem helper_norm_neg_logDeriv_eq_tsum_norm (σ : ℝ) (hσ : 1 < σ) : ‖-deriv riemannZeta ↑σ / riemannZeta ↑σ‖ = ∑' (n : ℕ), ‖↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ ↑σ‖

theorem lem_zetacenterbd (t σ : ℝ) : σ ≥ 3 / 2 → ‖deriv riemannZeta { re := σ, im := t } / riemannZeta { re := σ, im := t }‖ ≤ ‖deriv riemannZeta ↑σ / riemannZeta ↑σ‖

theorem lem_logDerivZetalogt32 : ∃ C > 1, ∀ (t : ℝ), |t| > 3 → ∀ σ ≥ 3 / 2, ‖deriv riemannZeta { re := σ, im := t } / riemannZeta { re := σ, im := t }‖ ≤ C

theorem thm_final_result : ∃ A > 0, A < 1 ∧ ∃ C > 1, ∀ (t : ℝ), |t| > 3 → ∀ σ ≥ 1 - A / Real.log (|t| + 2), ‖deriv riemannZeta { re := σ, im := t } / riemannZeta { re := σ, im := t }‖ ≤ C * Real.log |t| ^ 2

theorem ZetaZeroFree_p : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 1) 1 → riemannZeta (↑σ + ↑t * Complex.I) ≠ 0

theorem LogDerivZetaBndUnif2 : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ici (1 - A / Real.log |t| ^ 1) → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2