PrimeNumberTheoremAnd.ZetaBounds

theorem nonZeroOfBddAbove {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) :

∃ V ∈ nhds p, IsOpen V ∧ ∀ s ∈ V \ {p}, f s ≠ 0

Inspect dependencies

nonZeroOfBddAbove · compiled type and proof/definition references.

source

theorem logDerivResidue' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_is_open : IsOpen U) (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) :

(deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

Inspect dependencies

logDerivResidue' · compiled type and proof/definition references.

source

theorem logDerivResidue {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) :

(deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

Inspect dependencies

logDerivResidue · compiled type and proof/definition references.

source

theorem BddAbove_to_IsBigO {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (hU : U ∈ nhds p) (bdd : BddAbove (norm ∘ f '' (U \ {p}))) :

f =O[nhdsWithin p {p}ᶜ] 1

Inspect dependencies

BddAbove_to_IsBigO · compiled type and proof/definition references.

source

theorem logDerivResidue'' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) :

∃ V ∈ nhds p, BddAbove (norm ∘ (deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) '' (V \ {p}))

Inspect dependencies

logDerivResidue'' · compiled type and proof/definition references.

source

theorem ResidueMult {f g : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (g_holc : HolomorphicOn g U) (U_in_nhds : U ∈ nhds p) {A : ℂ} (f_near_p : (f - fun (s : ℂ) => A * (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1) :

(f * g - fun (s : ℂ) => A * g p * (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

Inspect dependencies

ResidueMult · compiled type and proof/definition references.

source

theorem riemannZetaLogDerivResidue :

∃ U ∈ nhds 1, BddAbove (norm ∘ (-(deriv riemannZeta / riemannZeta) - fun (s : ℂ) => (s - 1)⁻¹) '' (U \ {1}))

Inspect dependencies

riemannZetaLogDerivResidue · compiled type and proof/definition references.

source

theorem riemannZetaLogDerivResidueBigO :

(-deriv riemannZeta / riemannZeta - fun (z : ℂ) => (z - 1)⁻¹) =O[nhdsWithin 1 {1}ᶜ] 1

Inspect dependencies

riemannZetaLogDerivResidueBigO · compiled type and proof/definition references.

source

noncomputable def riemannZeta0 (N : ℕ) (s : ℂ) :

ℂ

Equations

riemannZeta0 N s = ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)

Instances For

Inspect dependencies

riemannZeta0 · compiled type and proof/definition references.

source

theorem riemannZeta0_apply (N : ℕ) (s : ℂ) :

riemannZeta0 N s = ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))

Inspect dependencies

riemannZeta0_apply · compiled type and proof/definition references.

source

theorem Real.differentiableAt_cpow_const_of_ne (s : ℂ) {x : ℝ} (xpos : 0 < x) :

DifferentiableAt ℝ (fun (x : ℝ) => ↑x ^ s) x

Inspect dependencies

Real.differentiableAt_cpow_const_of_ne · compiled type and proof/definition references.

source

theorem Complex.one_div_cpow_eq {s : ℂ} {x : ℝ} (x_ne : x ≠ 0) :

1 / ↑x ^ s = ↑x ^ (-s)

Inspect dependencies

Complex.one_div_cpow_eq · compiled type and proof/definition references.

source

theorem sum_eq_int_deriv {φ : ℝ → ℂ} {a b : ℝ} (apos : 0 ≤ a) (a_lt_b : a < b) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) :

∑ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋₊ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋₊ + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

Inspect dependencies

sum_eq_int_deriv · compiled type and proof/definition references.

source

theorem xpos_of_uIcc {a b : ℕ} (ha : a ∈ Set.Ioo 0 b) {x : ℝ} (x_in : x ∈ Set.uIcc ↑a ↑b) :

0 < x

Inspect dependencies

xpos_of_uIcc · compiled type and proof/definition references.

source

theorem ZetaSum_aux1₁ {a b : ℕ} {s : ℂ} (s_ne_one : s ≠ 1) (ha : a ∈ Set.Ioo 0 b) :

∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s)

Inspect dependencies

ZetaSum_aux1₁ · compiled type and proof/definition references.

source

theorem ZetaSum_aux1φDiff {s : ℂ} {x : ℝ} (xpos : 0 < x) :

HasDerivAt (fun (t : ℝ) => 1 / ↑t ^ s) (deriv (fun (t : ℝ) => 1 / ↑t ^ s) x) x

Inspect dependencies

ZetaSum_aux1φDiff · compiled type and proof/definition references.

source

theorem ZetaSum_aux1φderiv {s : ℂ} (s_ne_zero : s ≠ 0) {x : ℝ} (xpos : 0 < x) :

deriv (fun (t : ℝ) => 1 / ↑t ^ s) x = (fun (x : ℝ) => -s * ↑x ^ (-(s + 1))) x

Inspect dependencies

ZetaSum_aux1φderiv · compiled type and proof/definition references.

source

theorem ZetaSum_aux1derivφCont {s : ℂ} (s_ne_zero : s ≠ 0) {a b : ℕ} (ha : a ∈ Set.Ioo 0 b) :

ContinuousOn (deriv fun (t : ℝ) => 1 / ↑t ^ s) (Set.uIcc ↑a ↑b)

Inspect dependencies

ZetaSum_aux1derivφCont · compiled type and proof/definition references.

source

theorem ZetaSum_aux1 {a b : ℕ} {s : ℂ} (s_ne_one : s ≠ 1) (s_ne_zero : s ≠ 0) (ha : a ∈ Set.Ioo 0 b) :

∑ n ∈ Finset.Ioc a b, 1 / ↑n ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) + s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

Inspect dependencies

ZetaSum_aux1 · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_1' {a b x : ℝ} (apos : 0 < a) (hx : x ∈ Set.Icc a b) :

0 < x

Inspect dependencies

ZetaSum_aux1_1' · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_1 {a b x : ℝ} (apos : 0 < a) (a_lt_b : a < b) (hx : x ∈ Set.uIcc a b) :

0 < x

Inspect dependencies

ZetaSum_aux1_1 · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_2 {a b c : ℝ} (apos : 0 < a) (a_lt_b : a < b) (h : c ≠ 0 ∧ 0 ∉ Set.uIcc a b) :

∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (a ^ (-c) - b ^ (-c)) / c

Inspect dependencies

ZetaSum_aux1_2 · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_3 (x : ℝ) :

‖↑⌊x⌋ + 1 / 2 - x‖ ≤ 1 / 2

Inspect dependencies

ZetaSum_aux1_3 · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_4' (x : ℝ) (hx : 0 < x) (s : ℂ) :

‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ‖↑⌊x⌋ + 1 / 2 - x‖ / x ^ (s + 1).re

Inspect dependencies

ZetaSum_aux1_4' · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_4 {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} :

∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re

Inspect dependencies

ZetaSum_aux1_4 · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_5a {a b : ℝ} (apos : 0 < a) {s : ℂ} (x : ℝ) (h : x ∈ Set.Icc a b) :

|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)

Inspect dependencies

ZetaSum_aux1_5a · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_5b {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :

IntervalIntegrable (fun (u : ℝ) => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b

Inspect dependencies

ZetaSum_aux1_5b · compiled type and proof/definition references.

source

theorem measurable_floor_add_half_sub :

Measurable fun (u : ℝ) => ↑⌊u⌋ + 1 / 2 - u

Inspect dependencies

measurable_floor_add_half_sub · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_5c {a b : ℝ} {s : ℂ} :

have g := fun (u : ℝ) => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1); MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Set.uIoc a b))

Inspect dependencies

ZetaSum_aux1_5c · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_5d {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :

IntervalIntegrable (fun (u : ℝ) => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b

Inspect dependencies

ZetaSum_aux1_5d · compiled type and proof/definition references.

source

theorem ZetaSum_aux1_5 {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :

∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1)

Inspect dependencies

ZetaSum_aux1_5 · compiled type and proof/definition references.

source

theorem ZetaBnd_aux1a {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :

∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ (a ^ (-s.re) - b ^ (-s.re)) / s.re

Inspect dependencies

ZetaBnd_aux1a · compiled type and proof/definition references.

source

theorem Finset.Ioc_eq_Ico (M N : ℕ) :

Ioc N M = Ico (N + 1) (M + 1)

Inspect dependencies

Finset.Ioc_eq_Ico · compiled type and proof/definition references.

source

theorem Finset.Ioc_eq_Icc (M N : ℕ) :

Ioc N M = Icc (N + 1) M

Inspect dependencies

Finset.Ioc_eq_Icc · compiled type and proof/definition references.

source

theorem Finset.Icc_eq_Ico (M N : ℕ) :

Icc N M = Ico N (M + 1)

Inspect dependencies

Finset.Icc_eq_Ico · compiled type and proof/definition references.

source

theorem finsetSum_tendsto_tsum {N : ℕ} {f : ℕ → ℂ} (hf : Summable f) :

Filter.Tendsto (fun (k : ℕ) => ∑ n ∈ Finset.Ico N k, f n) Filter.atTop (nhds (∑' (n : ℕ), f (n + N)))

Inspect dependencies

finsetSum_tendsto_tsum · compiled type and proof/definition references.

source

theorem Complex.cpow_tendsto {s : ℂ} (s_re_gt : 1 < s.re) :

Filter.Tendsto (fun (x : ℕ) => ↑x ^ (1 - s)) Filter.atTop (nhds 0)

Inspect dependencies

Complex.cpow_tendsto · compiled type and proof/definition references.

source

theorem Complex.cpow_inv_tendsto {s : ℂ} (hs : 0 < s.re) :

Filter.Tendsto (fun (x : ℕ) => (↑x ^ s)⁻¹) Filter.atTop (nhds 0)

Inspect dependencies

Complex.cpow_inv_tendsto · compiled type and proof/definition references.

source

theorem ZetaSum_aux2a :

∃ (C : ℝ), ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - x‖ ≤ C

Inspect dependencies

ZetaSum_aux2a · compiled type and proof/definition references.

source

theorem ZetaSum_aux3 {N : ℕ} {s : ℂ} (s_re_gt : 1 < s.re) :

Filter.Tendsto (fun (k : ℕ) => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) Filter.atTop (nhds (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))

Inspect dependencies

ZetaSum_aux3 · compiled type and proof/definition references.

source

theorem integrableOn_of_Zeta0_fun {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 0 < s.re) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) (Set.Ioi ↑N) MeasureTheory.volume

Inspect dependencies

integrableOn_of_Zeta0_fun · compiled type and proof/definition references.

source

theorem ZetaSum_aux2 {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 1 < s.re) :

∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s = -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

Inspect dependencies

ZetaSum_aux2 · compiled type and proof/definition references.

source

theorem ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (σpos : 0 < σ) :

‖∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖ ≤ ↑N ^ (-σ) / σ

Inspect dependencies

ZetaBnd_aux1b · compiled type and proof/definition references.

source

theorem ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (hσ : σ ∈ Set.Ioc 0 2) (ht : 2 ≤ |t|) :

‖(↑σ + ↑t * Complex.I) * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ

Inspect dependencies

ZetaBnd_aux1 · compiled type and proof/definition references.

source

theorem ZetaBnd_aux1p (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Set.Ioc 0 2) :

(fun (t : ℝ) => ‖(↑σ + ↑t * Complex.I) * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖) =O[Filter.principal {t : ℝ | 2 ≤ |t|}] fun (t : ℝ) => |t| * ↑N ^ (-σ) / σ

Inspect dependencies

ZetaBnd_aux1p · compiled type and proof/definition references.

source

theorem isOpen_aux :

IsOpen {z : ℂ | z ≠ 1 ∧ 0 < z.re}

Inspect dependencies

isOpen_aux · compiled type and proof/definition references.

source

theorem integrable_log_over_pow {r : ℝ} (rneg : r < 0) {N : ℕ} (Npos : 0 < N) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => ‖x ^ (r - 1)‖ * ‖Real.log x‖) (Set.Ioi ↑N) MeasureTheory.volume

Inspect dependencies

integrable_log_over_pow · compiled type and proof/definition references.

source

theorem integrableOn_of_Zeta0_fun_log {N : ℕ} (Npos : 0 < N) {s : ℂ} (s_re_gt : 0 < s.re) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑(Real.log x)) (Set.Ioi ↑N) MeasureTheory.volume

Inspect dependencies

integrableOn_of_Zeta0_fun_log · compiled type and proof/definition references.

source

theorem hasDerivAt_Zeta0Integral {N : ℕ} (Npos : 0 < N) {s : ℂ} (hs : s ∈ {s : ℂ | 0 < s.re}) :

HasDerivAt (fun (z : ℂ) => ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1)) (∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)) s

Inspect dependencies

hasDerivAt_Zeta0Integral · compiled type and proof/definition references.

source

noncomputable def ζ₀' (N : ℕ) (s : ℂ) :

ℂ

Equations

ζ₀' N s = ∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(Real.log ↑n) + (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(Real.log ↑N) * ↑N ^ (1 - s) / (1 - s)) + ↑(Real.log ↑N) * ↑N ^ (-s) / 2 + ((1 * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x))

Instances For

Inspect dependencies

ζ₀' · compiled type and proof/definition references.

source

theorem HasDerivAt_neg_cpow_over2 {N : ℕ} (Npos : 0 < N) (s : ℂ) :

HasDerivAt (fun (x : ℂ) => -↑N ^ (-x) / 2) (-(-↑(Real.log ↑N) * ↑N ^ (-s)) / 2) s

Inspect dependencies

HasDerivAt_neg_cpow_over2 · compiled type and proof/definition references.

source

theorem HasDerivAt_cpow_over_var (N : ℕ) {z : ℂ} (z_ne_zero : z ≠ 0) :

HasDerivAt (fun (z : ℂ) => -↑N ^ z / z) (↑N ^ z / z ^ 2 - ↑(Real.log ↑N) * ↑N ^ z / z) z

Inspect dependencies

HasDerivAt_cpow_over_var · compiled type and proof/definition references.

source

theorem HasDerivAtZeta0 {N : ℕ} (Npos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) :

HasDerivAt (riemannZeta0 N) (ζ₀' N s) s

Inspect dependencies

HasDerivAtZeta0 · compiled type and proof/definition references.

source

theorem HolomorphicOn_riemannZeta0 {N : ℕ} (N_pos : 0 < N) :

HolomorphicOn (riemannZeta0 N) {s : ℂ | s ≠ 1 ∧ 0 < s.re}

Inspect dependencies

HolomorphicOn_riemannZeta0 · compiled type and proof/definition references.

source

theorem HolomorphicOn_riemannZeta :

HolomorphicOn riemannZeta {s : ℂ | s ≠ 1}

Inspect dependencies

HolomorphicOn_riemannZeta · compiled type and proof/definition references.

source

theorem isPathConnected_aux :

IsPathConnected {z : ℂ | z ≠ 1 ∧ 0 < z.re}

Inspect dependencies

isPathConnected_aux · compiled type and proof/definition references.

source

theorem Zeta0EqZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) :

riemannZeta0 N s = riemannZeta s

Inspect dependencies

Zeta0EqZeta · compiled type and proof/definition references.

source

theorem DerivZeta0EqDerivZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) :

deriv (riemannZeta0 N) s = deriv riemannZeta s

Inspect dependencies

DerivZeta0EqDerivZeta · compiled type and proof/definition references.

source

theorem le_trans₄ {α : Type u_1} [Preorder α] {a b c d : α} :

a ≤ b → b ≤ c → c ≤ d → a ≤ d

Inspect dependencies

le_trans₄ · compiled type and proof/definition references.

source

theorem lt_trans₄ {α : Type u_1} [Preorder α] {a b c d : α} :

a < b → b < c → c < d → a < d

Inspect dependencies

lt_trans₄ · compiled type and proof/definition references.

source

theorem norm_add₅_le {E : Type u_1} [SeminormedAddGroup E] (a b c d e : E) :

‖a + b + c + d + e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖

Inspect dependencies

norm_add₅_le · compiled type and proof/definition references.

source

theorem norm_add₆_le {E : Type u_1} [SeminormedAddGroup E] (a b c d e f : E) :

‖a + b + c + d + e + f‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖ + ‖f‖

Inspect dependencies

norm_add₆_le · compiled type and proof/definition references.

source

theorem mul_le_mul₃ {α : Type u_1} {a b c d e f : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : e ≤ f) (c0 : 0 ≤ c) (b0 : 0 ≤ b) (e0 : 0 ≤ e) :

a * c * e ≤ b * d * f

Inspect dependencies

mul_le_mul₃ · compiled type and proof/definition references.

source

theorem ZetaBnd_aux2 {n : ℕ} {t A σ : ℝ} (Apos : 0 < A) (σpos : 0 < σ) (n_le_t : ↑n ≤ |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) :

‖↑n ^ (-(↑σ + ↑t * Complex.I))‖ ≤ (↑n)⁻¹ * Real.exp A

Inspect dependencies

ZetaBnd_aux2 · compiled type and proof/definition references.

source

theorem logt_gt_one {t : ℝ} (t_ge : 3 ≤ t) :

1 < Real.log t

Inspect dependencies

logt_gt_one · compiled type and proof/definition references.

source

theorem UpperBnd_aux {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) :

have N := ⌊|t|⌋₊; 0 < N ∧ ↑N ≤ |t| ∧ 1 < Real.log |t| ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * Complex.I ≠ 1

Inspect dependencies

UpperBnd_aux · compiled type and proof/definition references.

source

theorem UpperBnd_aux2 {A σ t : ℝ} (t_ge : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) :

|t| ^ (1 - σ) ≤ Real.exp A

Inspect dependencies

UpperBnd_aux2 · compiled type and proof/definition references.

source

theorem riemannZeta0_zero_aux (N : ℕ) (Npos : 0 < N) :

∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

Inspect dependencies

riemannZeta0_zero_aux · compiled type and proof/definition references.

source

theorem UpperBnd_aux3 {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) :

have N := ⌊|t|⌋₊; ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * Complex.I))‖ ≤ Real.exp A * C * Real.log |t|

Inspect dependencies

UpperBnd_aux3 · compiled type and proof/definition references.

source

theorem Nat.self_div_floor_bound {t : ℝ} (t_ge : 1 ≤ |t|) :

have N := ⌊|t|⌋₊; |t| / ↑N ∈ Set.Icc 1 2

Inspect dependencies

Nat.self_div_floor_bound · compiled type and proof/definition references.

source

theorem UpperBnd_aux5 {σ t : ℝ} (t_ge : 3 < |t|) (σ_le : σ ≤ 2) :

(|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4

Inspect dependencies

UpperBnd_aux5 · compiled type and proof/definition references.

source

theorem UpperBnd_aux6 {σ t : ℝ} (t_ge : 3 < |t|) (hσ : σ ∈ Set.Ioc (1 / 2) 2) (neOne : ↑σ + ↑t * Complex.I ≠ 1) (Npos : 0 < ⌊|t|⌋₊) (N_le_t : ↑⌊|t|⌋₊ ≤ |t|) :

↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * Complex.I)‖ ≤ |t| ^ (1 - σ) * 2 ∧ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)

Inspect dependencies

UpperBnd_aux6 · compiled type and proof/definition references.

source

theorem ZetaUpperBnd' {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have C := Real.exp A * (5 + 8 * 2); have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ C * Real.log |t|

Inspect dependencies

ZetaUpperBnd' · compiled type and proof/definition references.

source

theorem ZetaUpperBnd :

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

Inspect dependencies

ZetaUpperBnd · compiled type and proof/definition references.

source

theorem norm_complex_log_ofNat (n : ℕ) :

‖Complex.log ↑n‖ = Real.log ↑n

Inspect dependencies

norm_complex_log_ofNat · compiled type and proof/definition references.

source

theorem Real.log_natCast_monotone :

Monotone fun (n : ℕ) => log ↑n

Inspect dependencies

Real.log_natCast_monotone · compiled type and proof/definition references.

source

theorem Finset.Icc0_eq (N : ℕ) :

Icc 0 N = {0} ∪ Icc 1 N

Inspect dependencies

Finset.Icc0_eq · compiled type and proof/definition references.

source

theorem harmonic_eq_sum_Icc0_aux (N : ℕ) :

∑ i ∈ Finset.Icc 0 N, (↑i)⁻¹ = ∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹

Inspect dependencies

harmonic_eq_sum_Icc0_aux · compiled type and proof/definition references.

source

theorem harmonic_eq_sum_Icc0 (N : ℕ) :

∑ i ∈ Finset.Icc 0 N, (↑i)⁻¹ = ↑(harmonic N)

Inspect dependencies

harmonic_eq_sum_Icc0 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux1 {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) :

have N := ⌊|t|⌋₊; ‖∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ (↑σ + ↑t * Complex.I) * ↑(Real.log ↑n)‖ ≤ Real.exp A * C * Real.log |t| ^ 2

Inspect dependencies

DerivUpperBnd_aux1 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux2 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖-↑N ^ (1 - s) / (1 - s) ^ 2‖ ≤ Real.exp A * 2 * (1 / 3)

Inspect dependencies

DerivUpperBnd_aux2 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux3 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖↑(Real.log ↑N) * ↑N ^ (1 - s) / (1 - s)‖ ≤ Real.exp A * 2 * Real.log |t|

Inspect dependencies

DerivUpperBnd_aux3 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux4 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖↑(Real.log ↑N) * ↑N ^ (-s) / 2‖ ≤ Real.exp A * Real.log |t|

Inspect dependencies

DerivUpperBnd_aux4 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux5 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; 0 < N → 1 / 2 < σ → ‖1 * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)‖ ≤ 1 / 3 * (2 * |t| * ↑N ^ (-σ) / σ)

Inspect dependencies

DerivUpperBnd_aux5 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux6 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; 0 < N → ↑N ≤ |t| → ↑σ + ↑t * Complex.I ≠ 1 → 1 / 2 < σ → 2 * |t| * ↑N ^ (-σ) / σ ≤ 2 * (8 * Real.exp A)

Inspect dependencies

DerivUpperBnd_aux6 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_1 {x σ t : ℝ} (hx : 1 ≤ x) :

have s := ↑σ + ↑t * Complex.I; ‖(↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ = |↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x

Inspect dependencies

DerivUpperBnd_aux7_1 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_2 {x σ : ℝ} (hx : 1 ≤ x) :

|↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x ≤ x ^ (-σ - 1) * Real.log x

Inspect dependencies

DerivUpperBnd_aux7_2 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_3 {x σ : ℝ} (xpos : 0 < x) (σnz : σ ≠ 0) :

HasDerivAt (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) (x ^ (-σ - 1) * Real.log x) x

Inspect dependencies

DerivUpperBnd_aux7_3 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_3' {a σ : ℝ} (apos : 0 < a) (σnz : σ ≠ 0) (x : ℝ) :

x ∈ Set.Ici a → HasDerivAt (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) (x ^ (-σ - 1) * Real.log x) x

Inspect dependencies

DerivUpperBnd_aux7_3' · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_nonneg {a σ : ℝ} (ha : 1 ≤ a) (x : ℝ) :

x ∈ Set.Ioi a → 0 ≤ x ^ (-σ - 1) * Real.log x

Inspect dependencies

DerivUpperBnd_aux7_nonneg · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_tendsto {σ : ℝ} (σpos : 0 < σ) :

Filter.Tendsto (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) Filter.atTop (nhds 0)

Inspect dependencies

DerivUpperBnd_aux7_tendsto · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_4 {a σ : ℝ} (σpos : 0 < σ) (ha : 1 ≤ a) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (-σ - 1) * Real.log x) (Set.Ioi a) MeasureTheory.volume

Inspect dependencies

DerivUpperBnd_aux7_4 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_5 {a σ : ℝ} (σpos : 0 < σ) (ha : 1 ≤ a) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => |↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x) (Set.Ioi a) MeasureTheory.volume

Inspect dependencies

DerivUpperBnd_aux7_5 · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7_integral_eq {a σ : ℝ} (ha : 1 ≤ a) (σpos : 0 < σ) :

∫ (x : ℝ) in Set.Ioi a, x ^ (-σ - 1) * Real.log x = 1 / σ ^ 2 * a ^ (-σ) + 1 / σ * a ^ (-σ) * Real.log a

Inspect dependencies

DerivUpperBnd_aux7_integral_eq · compiled type and proof/definition references.

source

theorem DerivUpperBnd_aux7 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ ≤ 6 * |t| * ↑N ^ (-σ) / σ * Real.log |t|

Inspect dependencies

DerivUpperBnd_aux7 · compiled type and proof/definition references.

source

theorem ZetaDerivUpperBnd' {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) :

have C := Real.exp A * 59; have N := ⌊|t|⌋₊; have s := ↑σ + ↑t * Complex.I; ‖∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(Real.log ↑n)‖ + ‖-↑N ^ (1 - s) / (1 - s) ^ 2‖ + ‖↑(Real.log ↑N) * ↑N ^ (1 - s) / (1 - s)‖ + ‖↑(Real.log ↑N) * ↑N ^ (-s) / 2‖ + ‖1 * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)‖ + ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ ≤ C * Real.log |t| ^ 2

Inspect dependencies

ZetaDerivUpperBnd' · compiled type and proof/definition references.

source

theorem ZetaDerivUpperBnd :

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

Inspect dependencies

ZetaDerivUpperBnd · compiled type and proof/definition references.

source

theorem Tendsto_nhdsWithin_punctured_map_add {f : ℝ → ℝ} (a x : ℝ) (f_mono : StrictMono f) (f_iso : Isometry f) :

Filter.Tendsto (fun (y : ℝ) => f y + a) (nhdsWithin x (Set.Ioi x)) (nhdsWithin (f x + a) (Set.Ioi (f x + a)))

Inspect dependencies

Tendsto_nhdsWithin_punctured_map_add · compiled type and proof/definition references.

source

theorem Tendsto_nhdsWithin_punctured_add (a x : ℝ) :

Filter.Tendsto (fun (y : ℝ) => y + a) (nhdsWithin x (Set.Ioi x)) (nhdsWithin (x + a) (Set.Ioi (x + a)))

Inspect dependencies

Tendsto_nhdsWithin_punctured_add · compiled type and proof/definition references.

source

theorem riemannZeta_isBigO_near_one_horizontal :

(fun (x : ℝ) => riemannZeta (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1 / ↑x

Inspect dependencies

riemannZeta_isBigO_near_one_horizontal · compiled type and proof/definition references.

source

theorem ZetaNear1BndFilter :

(fun (σ : ℝ) => riemannZeta ↑σ) =O[nhdsWithin 1 (Set.Ioi 1)] fun (σ : ℝ) => 1 / (↑σ - 1)

Inspect dependencies

ZetaNear1BndFilter · compiled type and proof/definition references.

source

theorem ZetaNear1BndExact :

∃ (c : ℝ) (_ : 0 < c), ∀ σ ∈ Set.Ioc 1 2, ‖riemannZeta ↑σ‖ ≤ c / (σ - 1)

Inspect dependencies

ZetaNear1BndExact · compiled type and proof/definition references.

source

theorem norm_zeta_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :

‖riemannZeta (1 + ↑x) ^ 3 * riemannZeta (1 + ↑x + Complex.I * ↑y) ^ 4 * riemannZeta (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

For positive x and nonzero y we have that $|\zeta(x)^3 \cdot \zeta(x+iy)^4 \cdot \zeta(x+2iy)| \ge 1$.

Inspect dependencies

norm_zeta_product_ge_one · compiled type and proof/definition references.

source

theorem ZetaLowerBound1_aux1 {σ t : ℝ} (this : 1 ≤ ‖riemannZeta ↑σ‖ ^ 3 * ‖riemannZeta (↑σ + Complex.I * ↑t)‖ ^ 4 * ‖riemannZeta (↑σ + 2 * Complex.I * ↑t)‖) :

‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1

Inspect dependencies

ZetaLowerBound1_aux1 · compiled type and proof/definition references.

source

theorem ZetaLowerBound1 {σ t : ℝ} (σ_gt : 1 < σ) :

‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1

Inspect dependencies

ZetaLowerBound1 · compiled type and proof/definition references.

source

theorem ZetaLowerBound2 {σ t : ℝ} (σ_gt : 1 < σ) :

1 / (‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)) ≤ ‖riemannZeta (↑σ + ↑t * Complex.I)‖

Inspect dependencies

ZetaLowerBound2 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3_aux1 (A : ℝ) (ha : A ∈ Set.Ioc 0 (1 / 2)) (t : ℝ) (ht_2 : 3 < |2 * t|) :

0 < A / Real.log |2 * t|

Inspect dependencies

ZetaLowerBound3_aux1 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3_aux2 {C σ t : ℝ} (ζ_2t_bound : ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ≤ C * Real.log |2 * t|) :

‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) ≤ (C * Real.log |2 * t|) ^ (1 / 4)

Inspect dependencies

ZetaLowerBound3_aux2 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3_aux3 (C c_near : ℝ) {σ : ℝ} (t : ℝ) (σ_gt : 1 < σ) :

c_near ^ (3 / 4) * ((-1 + σ) ^ (3 / 4))⁻¹ * C ^ (1 / 4) * Real.log |t * 2| ^ (1 / 4) = c_near ^ (3 / 4) * C ^ (1 / 4) * Real.log |t * 2| ^ (1 / 4) * (-1 + σ) ^ (-3 / 4)

Inspect dependencies

ZetaLowerBound3_aux3 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3_aux4 (C : ℝ) (hC : 0 < C) (c_near : ℝ) (hc_near : 0 < c_near) {σ : ℝ} (t : ℝ) (ht : 3 < |t|) (σ_gt : 1 < σ) :

0 < c_near ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * C ^ (1 / 4) * Real.log |2 * t| ^ (1 / 4)

Inspect dependencies

ZetaLowerBound3_aux4 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3_aux5 {σ : ℝ} (t : ℝ) (this : ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1) :

0 < ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)

Inspect dependencies

ZetaLowerBound3_aux5 · compiled type and proof/definition references.

source

theorem ZetaLowerBound3 :

∃ c > 0, ∀ {σ : ℝ}, σ ∈ Set.Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → c * (σ - 1) ^ (3 / 4) / Real.log |t| ^ (1 / 4) ≤ ‖riemannZeta (↑σ + ↑t * Complex.I)‖

Inspect dependencies

ZetaLowerBound3 · compiled type and proof/definition references.

source

theorem ZetaInvBound1 {σ t : ℝ} (σ_gt : 1 < σ) :

1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)

Inspect dependencies

ZetaInvBound1 · compiled type and proof/definition references.

source

theorem Ioi_union_Iio_mem_cocompact {a : ℝ} (ha : 0 ≤ a) :

Set.Ioi a ∪ Set.Iio (-a) ∈ Filter.cocompact ℝ

Inspect dependencies

Ioi_union_Iio_mem_cocompact · compiled type and proof/definition references.

source

theorem lt_abs_mem_cocompact {a : ℝ} (ha : 0 ≤ a) :

{t : ℝ | a < |t|} ∈ Filter.cocompact ℝ

Inspect dependencies

lt_abs_mem_cocompact · compiled type and proof/definition references.

source

theorem ZetaInvBound2 :

∃ C > 0, ∀ {σ : ℝ}, σ ∈ Set.Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * Real.log |t| ^ (1 / 4)

Inspect dependencies

ZetaInvBound2 · compiled type and proof/definition references.

source

theorem deriv_fun_re {t : ℝ} {f : ℂ → ℂ} (diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * Complex.I)) :

(deriv fun {σ₂ : ℝ} => f (↑σ₂ + ↑t * Complex.I)) = fun (σ : ℝ) => deriv f (↑σ + ↑t * Complex.I)

Inspect dependencies

deriv_fun_re · compiled type and proof/definition references.

source

theorem Zeta_eq_int_derivZeta {σ₁ σ₂ t : ℝ} (t_ne_zero : t ≠ 0) :

∫ (σ : ℝ) in σ₁..σ₂, deriv riemannZeta (↑σ + ↑t * Complex.I) = riemannZeta (↑σ₂ + ↑t * Complex.I) - riemannZeta (↑σ₁ + ↑t * Complex.I)

Inspect dependencies

Zeta_eq_int_derivZeta · compiled type and proof/definition references.

source

theorem Zeta_diff_Bnd :

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

Inspect dependencies

Zeta_diff_Bnd · compiled type and proof/definition references.

source

theorem ZetaInvBnd_aux' {t : ℝ} (logt_gt_one : 1 < Real.log |t|) :

Real.log |t| < Real.log |t| ^ 9

Inspect dependencies

ZetaInvBnd_aux' · compiled type and proof/definition references.

source

theorem ZetaInvBnd_aux {t : ℝ} (logt_gt_one : 1 < Real.log |t|) :

Real.log |t| ≤ Real.log |t| ^ 9

Inspect dependencies

ZetaInvBnd_aux · compiled type and proof/definition references.

source

theorem ZetaInvBnd_aux2 {A C₁ C₂ : ℝ} (Apos : 0 < A) (C₁pos : 0 < C₁) (C₂pos : 0 < C₂) (hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4) :

0 < (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹

Inspect dependencies

ZetaInvBnd_aux2 · compiled type and proof/definition references.

source

theorem ZetaInvBnd :

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

Inspect dependencies

ZetaInvBnd · compiled type and proof/definition references.

source

theorem ZetaLowerBnd :

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

Inspect dependencies

ZetaLowerBnd · compiled type and proof/definition references.

source

theorem ZetaZeroFree :

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

Inspect dependencies

ZetaZeroFree · compiled type and proof/definition references.

source

theorem LogDerivZetaBnd :

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

Inspect dependencies

LogDerivZetaBnd · compiled type and proof/definition references.

source

theorem ZetaNoZerosOn1Line (t : ℝ) :

riemannZeta (1 + ↑t * Complex.I) ≠ 0

Inspect dependencies

ZetaNoZerosOn1Line · compiled type and proof/definition references.

source

theorem ZetaCont :

ContinuousOn riemannZeta (Set.univ \ {1})

Inspect dependencies

ZetaCont · compiled type and proof/definition references.

source

theorem ZetaNoZerosInBox (T : ℝ) :

∃ (σ : ℝ) (_ : σ < 1), ∀ (t : ℝ), |t| ≤ T → ∀ σ' ≥ σ, riemannZeta (↑σ' + ↑t * Complex.I) ≠ 0

Inspect dependencies

ZetaNoZerosInBox · compiled type and proof/definition references.

source

theorem LogDerivZetaHoloOn {S : Set ℂ} (s_ne_one : 1 ∉ S) (nonzero : ∀ s ∈ S, riemannZeta s ≠ 0) :

HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) S

Inspect dependencies

LogDerivZetaHoloOn · compiled type and proof/definition references.

source

theorem LogDerivZetaHolcSmallT :

∃ (σ₂ : ℝ) (_ : σ₂ < 1), HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.uIcc σ₂ 2 ×ℂ Set.uIcc (-3) 3 \ {1})

Inspect dependencies

LogDerivZetaHolcSmallT · compiled type and proof/definition references.

source

theorem LogDerivZetaHolcLargeT :

∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)), ∀ (T : ℝ), 3 ≤ T → HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.Icc (1 - A / Real.log T ^ 9) 2 ×ℂ Set.Icc (-T) T \ {1})

Inspect dependencies

LogDerivZetaHolcLargeT · compiled type and proof/definition references.

source

theorem summable_complex_then_summable_real_part (f : ℕ → ℂ) (h : Summable f) :

Summable fun (n : ℕ) => (f n).re

Inspect dependencies

summable_complex_then_summable_real_part · compiled type and proof/definition references.

source

theorem dlog_riemannZeta_bdd_on_vertical_lines_generalized (σ₀ σ₁ t : ℝ) (σ₀_gt_one : 1 < σ₀) (σ₀_lt_σ₁ : σ₀ ≤ σ₁) :

‖-deriv riemannZeta (↑σ₁ + ↑t * Complex.I) / riemannZeta (↑σ₁ + ↑t * Complex.I)‖ ≤ ‖deriv riemannZeta ↑σ₀ / riemannZeta ↑σ₀‖

Inspect dependencies

dlog_riemannZeta_bdd_on_vertical_lines_generalized · compiled type and proof/definition references.

source

theorem triv_bound_zeta :

∃ C ≥ 0, ∀ (σ₀ t : ℝ), 1 < σ₀ → ‖-deriv riemannZeta (↑σ₀ + ↑t * Complex.I) / riemannZeta (↑σ₀ + ↑t * Complex.I)‖ ≤ (σ₀ - 1)⁻¹ + C

Inspect dependencies

triv_bound_zeta · compiled type and proof/definition references.

source

theorem LogDerivZetaBndUnif :

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

Inspect dependencies

LogDerivZetaBndUnif · compiled type and proof/definition references.