Definition of the Riemann zeta function

Main definitions:

• riemannZeta: the Riemann zeta function ζ : ℂ → ℂ.
• riemannCompletedZeta: the completed zeta function Λ : ℂ → ℂ, which satisfies Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s) (away from the poles of Γ(s / 2)).
• riemannCompletedZeta₀: the entire function Λ₀ satisfying Λ₀(s) = Λ(s) + 1 / (s - 1) - 1 / s wherever the RHS is defined.

Note that mathematically ζ(s) is undefined at s = 1, while Λ(s) is undefined at both s = 0 and s = 1. Our construction assigns some values at these points (which are not arbitrary, but I haven't checked exactly what they are).

Main results:

• differentiable_completed_zeta₀ : the function Λ₀(s) is entire.
• differentiableAt_completed_zeta : the function Λ(s) is differentiable away from s = 0 and s = 1.
• differentiableAt_riemannZeta : the function ζ(s) is differentiable away from s = 1.
• zeta_eq_tsum_one_div_nat_add_one_cpow : for 1 < re s, we have ζ(s) = ∑' (n : ℕ), 1 / (n + 1) ^ s.
• riemannCompletedZeta₀_one_sub, riemannCompletedZeta_one_sub, and riemannZeta_one_sub : functional equation relating values at s and 1 - s
• riemannZeta_neg_nat_eq_bernoulli : for any k ∈ ℕ we have the formula riemannZeta (-k) = (-1) ^ k * bernoulli (k + 1) / (k + 1)
• riemannZeta_two_mul_nat: formula for ζ(2 * k) for k ∈ ℕ, k ≠ 0 in terms of Bernoulli numbers

Outline of proofs:

We define two related functions on the reals, zetaKernel₁ and zetaKernel₂. The first is (θ (t * I) - 1) / 2, where θ is Jacobi's theta function; its Mellin transform is exactly the completed zeta function. The second is obtained by subtracting a linear combination of powers on the interval Ioc 0 1 to give a function with exponential decay at both 0 and ∞. We then define riemannCompletedZeta₀ as the Mellin transform of the second zeta kernel, and define riemannCompletedZeta and riemannZeta from this.

Since zetaKernel₂ has rapid decay and satisfies a functional equation relating its values at t and 1 / t, we deduce the analyticity of riemannCompletedZeta₀ and the functional equation relating its values at s and 1 - s. On the other hand, since zetaKernel₁ can be expanded in powers of exp (-π * t) and the Mellin transform integrated term-by-term, we obtain the relation to the naive Dirichlet series ∑' (n : ℕ), 1 / (n + 1) ^ s.

Definition of the Riemann zeta function and related functions

def zetaKernel₁ (t : ℝ) : ℂ

Function whose Mellin transform is π ^ (-s) * Γ(s) * zeta (2 * s), for 1 / 2 < Re s.

Equations

• zetaKernel₁ t = ∑' (n : ℕ), ↑(Real.exp (-Real.pi * t * (↑n + 1) ^ 2))

def zetaKernel₂ : ℝ → ℂ

Modified zeta kernel, whose Mellin transform is entire. -

Equations

• zetaKernel₂ = zetaKernel₁ + Set.indicator (Set.Ioc 0 1) fun (t : ℝ) => (1 - 1 / ↑√t) / 2

def riemannCompletedZeta₀ (s : ℂ) : ℂ

The completed Riemann zeta function with its poles removed, Λ(s) + 1 / s - 1 / (s - 1).

Equations

• riemannCompletedZeta₀ s = mellin zetaKernel₂ (s / 2)

def riemannCompletedZeta (s : ℂ) : ℂ

The completed Riemann zeta function, Λ(s), which satisfies Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s) (up to a minor correction at s = 0).

Equations

• riemannCompletedZeta s = riemannCompletedZeta₀ s - 1 / s + 1 / (s - 1)

theorem riemannZeta_def : riemannZeta = Function.update (fun (s : ℂ) => ↑Real.pi ^ (s / 2) * riemannCompletedZeta s / Complex.Gamma (s / 2)) 0 (-1 / 2)

@[irreducible]

def riemannZeta (a : ℂ) : ℂ

The Riemann zeta function ζ(s). We set this to be irreducible to hide messy implementation details.

Equations

• riemannZeta = wrapped✝.1

theorem riemannZeta_zero : riemannZeta 0 = -1 / 2

We have ζ(0) = -1 / 2.

First properties of the zeta kernels

theorem summable_exp_neg_pi_mul_nat_sq {t : ℝ} (ht : 0 < t) : Summable fun (n : ℕ) => Real.exp (-Real.pi * t * (↑n + 1) ^ 2)

The sum defining zetaKernel₁ is convergent.

theorem zetaKernel₁_eq_jacobiTheta {t : ℝ} (ht : 0 < t) : zetaKernel₁ t = (jacobiTheta (↑t * Complex.I) - 1) / 2

Relate zetaKernel₁ to the Jacobi theta function on ℍ. (We don't use this as the definition of zetaKernel₁, since the sum over ℕ rather than ℤ is more convenient for relating zeta to the Dirichlet series for re s > 1.)

theorem continuousAt_zetaKernel₁ {t : ℝ} (ht : 0 < t) : ContinuousAt zetaKernel₁ t

Continuity of zetaKernel₁.

theorem locally_integrable_zetaKernel₁ : MeasureTheory.LocallyIntegrableOn zetaKernel₁ (Set.Ioi 0) MeasureTheory.volume

Local integrability of zetaKernel₁.

theorem locally_integrable_zetaKernel₂ : MeasureTheory.LocallyIntegrableOn zetaKernel₂ (Set.Ioi 0) MeasureTheory.volume

Local integrability of zetaKernel₂.

theorem zetaKernel₂_one_div {t : ℝ} (ht : 0 ≤ t) : zetaKernel₂ (1 / t) = ↑√t * zetaKernel₂ t

Functional equation for zetaKernel₂.

## Bounds for zeta kernels

We now establish asymptotic bounds for the zeta kernels as t → ∞ and t → 0, and use these to show holomorphy of their Mellin transforms (for 1 / 2 < re s for zetaKernel₁, and all s for zetaKernel₂).

theorem isBigO_atTop_zetaKernel₁ : zetaKernel₁ =O[Filter.atTop] fun (t : ℝ) => Real.exp (-Real.pi * t)

Bound for zetaKernel₁ for large t.

theorem isBigO_atTop_zetaKernel₂ : zetaKernel₂ =O[Filter.atTop] fun (t : ℝ) => Real.exp (-Real.pi * t)

Bound for zetaKernel₂ for large t.

theorem isBigO_zero_zetaKernel₂ : zetaKernel₂ =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => Real.exp (-Real.pi / t) / √t

Precise but awkward-to-use bound for zetaKernel₂ for t → 0.

theorem isBigO_zero_zetaKernel₂_rpow (a : ℝ) : zetaKernel₂ =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ a

Weaker but more usable bound for zetaKernel₂ for t → 0.

theorem isBigO_zero_zetaKernel₁ : zetaKernel₁ =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ (-(1 / 2))

Bound for zetaKernel₁ for t → 0.

Differentiability of the completed zeta function

theorem differentiableAt_mellin_zetaKernel₁ {s : ℂ} (hs : 1 / 2 < s.re) : DifferentiableAt ℂ (mellin zetaKernel₁) s

The Mellin transform of the first zeta kernel is holomorphic for 1 / 2 < re s.

theorem differentiable_mellin_zetaKernel₂ : Differentiable ℂ (mellin zetaKernel₂)

The Mellin transform of the second zeta kernel is entire.

theorem differentiable_completed_zeta₀ : Differentiable ℂ riemannCompletedZeta₀

The modified completed Riemann zeta function Λ(s) + 1 / s - 1 / (s - 1) is entire.

theorem differentiableAt_completed_zeta {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1) : DifferentiableAt ℂ riemannCompletedZeta s

The completed Riemann zeta function Λ(s) is differentiable away from s = 0 and s = 1 (where it has simple poles).

theorem differentiableAt_riemannZeta {s : ℂ} (hs' : s ≠ 1) : DifferentiableAt ℂ riemannZeta s

The Riemann zeta function is differentiable away from s = 1.

theorem riemannZeta_neg_two_mul_nat_add_one (n : ℕ) : riemannZeta (-2 * (↑n + 1)) = 0

The trivial zeroes of the zeta function.

def RiemannHypothesis : Prop

A formal statement of the Riemann hypothesis – constructing a term of this type is worth a million dollars.

Equations

• RiemannHypothesis = ∀ (s : ℂ), s ≠ 1 → riemannCompletedZeta s = 0 → (¬∃ (n : ℕ), s = -2 * (↑n + 1)) → s.re = 1 / 2

Relating the Mellin transforms of the two zeta kernels

theorem hasMellin_one_div_sqrt_Ioc {s : ℂ} (hs : 1 / 2 < s.re) : HasMellin (Set.indicator (Set.Ioc 0 1) fun (t : ℝ) => 1 / ↑√t) s (1 / (s - 1 / 2))

theorem hasMellin_one_div_sqrt_sub_one_div_two_Ioc {s : ℂ} (hs : 1 / 2 < s.re) : HasMellin (Set.indicator (Set.Ioc 0 1) fun (t : ℝ) => (1 - 1 / ↑√t) / 2) s (1 / (2 * s) - 1 / (2 * s - 1))

Evaluate the Mellin transform of the "fudge factor" in zetaKernel₂

theorem mellin_zetaKernel₂_eq_of_lt_re {s : ℂ} (hs : 1 / 2 < s.re) : mellin zetaKernel₂ s = mellin zetaKernel₁ s + 1 / (2 * s) - 1 / (2 * s - 1)

theorem completed_zeta_eq_mellin_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : riemannCompletedZeta s = mellin zetaKernel₁ (s / 2)

## Relating the first zeta kernel to the Dirichlet series

theorem integral_cpow_mul_exp_neg_pi_mul_sq {s : ℂ} (hs : 0 < s.re) (n : ℕ) : ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * ↑(Real.exp (-Real.pi * t * (↑n + 1) ^ 2)) = ↑Real.pi ^ (-s) * Complex.Gamma s * (1 / (↑n + 1) ^ (2 * s))

Auxiliary lemma for mellin_zetaKernel₁_eq_tsum, computing the Mellin transform of an individual term in the series.

theorem mellin_zetaKernel₁_eq_tsum {s : ℂ} (hs : 1 / 2 < s.re) : mellin zetaKernel₁ s = ↑Real.pi ^ (-s) * Complex.Gamma s * ∑' (n : ℕ), 1 / (↑n + 1) ^ (2 * s)

theorem completed_zeta_eq_tsum_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : riemannCompletedZeta s = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2) * ∑' (n : ℕ), 1 / (↑n + 1) ^ s

theorem zeta_eq_tsum_one_div_nat_add_one_cpow {s : ℂ} (hs : 1 < s.re) : riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

The Riemann zeta function agrees with the naive Dirichlet-series definition when the latter converges. (Note that this is false without the assumption: when re s ≤ 1 the sum is divergent, and we use a different definition to obtain the analytic continuation to all s.)

theorem zeta_eq_tsum_one_div_nat_cpow {s : ℂ} (hs : 1 < s.re) : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s

Alternate formulation of zeta_eq_tsum_one_div_nat_add_one_cpow without the + 1, using the fact that for s ≠ 0 we define 0 ^ s = 0.

theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) : riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k

Special case of zeta_eq_tsum_one_div_nat_cpow when the argument is in ℕ, so the power function can be expressed using naïve pow rather than cpow.

theorem riemannZeta_two_mul_nat {k : ℕ} (hk : k ≠ 0) : riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(Nat.factorial (2 * k))

Explicit formula for ζ (2 * k), for k ∈ ℕ with k ≠ 0: we have ζ (2 * k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * bernoulli (2 * k) / (2 * k)!. Compare hasSum_zeta_nat for a version formulated explicitly as a sum, and riemannZeta_neg_nat_eq_bernoulli for values at negative integers (equivalent to the above via the functional equation).

theorem riemannZeta_two : riemannZeta 2 = ↑Real.pi ^ 2 / 6

theorem riemannZeta_four : riemannZeta 4 = ↑Real.pi ^ 4 / 90

Functional equation

theorem riemannCompletedZeta₀_one_sub (s : ℂ) : riemannCompletedZeta₀ (1 - s) = riemannCompletedZeta₀ s

Riemann zeta functional equation, formulated for Λ₀: for any complex s we have Λ₀(1 - s) = Λ₀ s.

theorem riemannCompletedZeta_one_sub (s : ℂ) : riemannCompletedZeta (1 - s) = riemannCompletedZeta s

Riemann zeta functional equation, formulated for Λ: for any complex s we have Λ (1 - s) = Λ s.

theorem riemannZeta_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) (hs' : s ≠ 1) : riemannZeta (1 - s) = 2 ^ (1 - s) * ↑Real.pi ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * (1 - s) / 2) * riemannZeta s

Riemann zeta functional equation, formulated for ζ: if 1 - s ∉ ℕ, then we have ζ (1 - s) = 2 ^ (1 - s) * π ^ (-s) * Γ s * sin (π * (1 - s) / 2) * ζ s.

theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) : riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)

theorem riemannCompletedZeta_residue_one : Filter.Tendsto (fun (s : ℂ) => (s - 1) * riemannCompletedZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

The residue of Λ(s) at s = 1 is equal to 1.

theorem riemannZeta_residue_one : Filter.Tendsto (fun (s : ℂ) => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

The residue of ζ(s) at s = 1 is equal to 1.