Statement of a version of the Wiener-Ikehara Theorem

def WienerIkeharaTheorem : Prop

A version of the Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic function whose L-series has a simple pole at s = 1 with residue A and otherwise extends continuously to the closed half-plane re s ≥ 1, then ∑ n < N, f n is asymptotic to A*N.

Equations

• One or more equations did not get rendered due to their size.

The Riemann Zeta Function does not vanish on Re(s) = 1

def rzeta : Lean.ParserDescr

We use ζ to denote the Riemann zeta function.

Equations

• rzeta = Lean.ParserDescr.node `rzeta 1024 (Lean.ParserDescr.symbol "ζ")

def Dchar_one' : Lean.ParserDescr

We use χ₁ to denote the (trivial) Dirichlet character modulo 1.

Equations

• Dchar_one' = Lean.ParserDescr.node `Dchar_one' 1024 (Lean.ParserDescr.symbol "χ₁")

theorem DirichletCharacter.LSeries_eulerProduct' {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun (n : ℕ) => χ ↑n) s

A variant of the Euler product for Dirichlet L-series.

theorem ArithmeticFunction.LSeries_zeta_eulerProduct' {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = LSeries 1 s

A variant of the Euler product for the L-series of ζ.

theorem riemannZeta_eulerProduct' {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = riemannZeta s

A variant of the Euler product for the Riemann zeta function.

theorem summable_neg_log_one_sub_char_mul_prime_cpow {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))

theorem re_log_comb_nonneg' {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ = 1) : 0 ≤ 3 * (-Complex.log (1 - ↑a)).re + 4 * (-Complex.log (1 - ↑a * z)).re + (-Complex.log (1 - ↑a * z ^ 2)).re

A technical lemma showing that a certain linear combination of real parts of logarithms is nonnegative. This is used to show non-vanishing of the Riemann zeta function and of Dirichlet L-series on the line re s = 1.

theorem re_log_comb_nonneg_dirichlet {N : ℕ} (χ : DirichletCharacter ℂ N) {n : ℕ} (hn : 2 ≤ n) {x : ℝ} {y : ℝ} (hx : 1 < x) : 0 ≤ 3 * (-Complex.log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-Complex.log (1 - χ ↑n * ↑n ^ (-(↑x + Complex.I * ↑y)))).re + (-Complex.log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * Complex.I * ↑y)))).re

The logarithm of an Euler factor of the product L(χ^0, x)^3 * L(χ, x+I*y)^4 * L(χ^2, x+2*I*y) has nonnegative real part when s = x + I*y has real part x > 1.

theorem one_lt_re_of_pos {x : ℝ} (y : ℝ) (hx : 0 < x) : 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + Complex.I * ↑y).re ∧ 1 < (1 + ↑x + 2 * Complex.I * ↑y).re

theorem norm_dirichlet_product_ge_one {N : ℕ} (χ : DirichletCharacter ℂ N) {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖LSeries (fun (n : ℕ) => 1 ↑n) (1 + ↑x) ^ 3 * LSeries (fun (n : ℕ) => χ ↑n) (1 + ↑x + Complex.I * ↑y) ^ 4 * LSeries (fun (n : ℕ) => (χ ^ 2) ↑n) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

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

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$.

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

theorem riemannZeta_isBigO_of_ne_one_horizontal {y : ℝ} (hy : y ≠ 0) : (fun (x : ℝ) => riemannZeta (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1

theorem riemannZeta_isBigO_near_root_horizontal {y : ℝ} (hy : y ≠ 0) (h : riemannZeta (1 + Complex.I * ↑y) = 0) : (fun (x : ℝ) => riemannZeta (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => ↑x

theorem riemannZeta_ne_zero_of_one_le_re ⦃z : ℂ⦄ (hz : z ≠ 1) (hz' : 1 ≤ z.re) : riemannZeta z ≠ 0

The Riemann Zeta Function does not vanish on the closed half-plane re z ≥ 1.

The logarithmic derivative of ζ has a simple pole at s = 1 with residue -1

We show that s ↦ ζ' s / ζ s + 1 / (s - 1) (or rather, its negative, which is the function we need for the Wiener-Ikehara Theorem) is continuous outside the zeros of ζ.

noncomputable def ζ₁ : ℂ → ℂ

The function obtained by "multiplying away" the pole of ζ. Its (negative) logarithmic derivative is the function used in the Wiener-Ikehara Theorem to prove the Prime Number Theorem.

Equations

• ζ₁ = Function.update (fun (z : ℂ) => riemannZeta z * (z - 1)) 1 1

theorem ζ₁_apply_of_ne_one {z : ℂ} (hz : z ≠ 1) : ζ₁ z = riemannZeta z * (z - 1)

theorem ζ₁_differentiable : Differentiable ℂ ζ₁

theorem deriv_ζ₁_apply_of_ne_one {z : ℂ} (hz : z ≠ 1) : deriv ζ₁ z = deriv riemannZeta z * (z - 1) + riemannZeta z

theorem neg_logDeriv_ζ₁_eq {z : ℂ} (hz₁ : z ≠ 1) (hz₂ : riemannZeta z ≠ 0) : -deriv ζ₁ z / ζ₁ z = -deriv riemannZeta z / riemannZeta z - 1 / (z - 1)

theorem continuousOn_neg_logDeriv_ζ₁ : ContinuousOn (fun (z : ℂ) => -deriv ζ₁ z / ζ₁ z) {z : ℂ | z = 1 ∨ riemannZeta z ≠ 0}

Derivation of the Prime Number Theorem from the Wiener-Ikehara Theorem

theorem PNT_vonMangoldt (WIT : WienerIkeharaTheorem) : Filter.Tendsto (fun (N : ℕ) => (Finset.range N).sum ⇑ArithmeticFunction.vonMangoldt / ↑N) Filter.atTop (nhds 1)

The Wiener-Ikehara Theorem implies the Prime Number Theorem in the form that ψ x ∼ x, where ψ x = ∑ n < x, Λ n and Λ is the von Mangoldt function.