# mathlib3documentation

number_theory.zeta_function

# Definition of the Riemann zeta function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions: #

• riemann_zeta: the Riemann zeta function ζ : ℂ → ℂ.
• riemann_completed_zeta: the completed zeta function Λ : ℂ → ℂ, which satisfies Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s) (away from the poles of Γ(s / 2)).
• riemann_completed_zeta₀: 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).

## Outline of proofs: #

We define two related functions on the reals, zeta_kernel₁ and zeta_kernel₂. 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 riemann_completed_zeta₀ as the Mellin transform of the second zeta kernel, and define riemann_completed_zeta and riemann_zeta from this.

Since zeta_kernel₂ has rapid decay and satisfies a functional equation relating its values at t and 1 / t, we deduce the analyticity of riemann_completed_zeta₀ and the functional equation relating its values at s and 1 - s. On the other hand, since zeta_kernel₁ 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.

noncomputable def zeta_kernel₁ (t : ) :

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

Equations
noncomputable def zeta_kernel₂  :

Modified zeta kernel, whose Mellin transform is entire. -

Equations
noncomputable def riemann_completed_zeta₀ (s : ) :

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

Equations
noncomputable def riemann_completed_zeta (s : ) :

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

Equations
@[irreducible]
noncomputable def riemann_zeta (a : ) :

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

Equations
theorem riemann_zeta_zero  :
= (-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 (λ (n : ), rexp * (n + 1) ^ 2))

The sum defining zeta_kernel₁ is convergent.

theorem zeta_kernel₁_eq_jacobi_theta {t : } (ht : 0 < t) :

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

theorem continuous_at_zeta_kernel₁ {t : } (ht : 0 < t) :

Continuity of zeta_kernel₁.

Local integrability of zeta_kernel₁.

Local integrability of zeta_kernel₂.

theorem zeta_kernel₂_one_div {t : } (ht : 0 < t) :

Functional equation for zeta_kernel₂.

## 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 zeta_kernel₁, and all s for zeta_kernel₂).

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

theorem is_O_zero_zeta_kernel₂_rpow (a : ) :
zeta_kernel₂ =O[ (set.Ioi 0)] λ (t : ), t ^ a

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

theorem is_O_zero_zeta_kernel₁  :
zeta_kernel₁ =O[ (set.Ioi 0)] λ (t : ), t ^ -(1 / 2)

Bound for zeta_kernel₁ for t → 0.

## Differentiability of the completed zeta function #

theorem differentiable_at_mellin_zeta_kernel₁ {s : } (hs : 1 / 2 < s.re) :

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

The Mellin transform of the second zeta kernel is entire.

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

theorem differentiable_at_completed_zeta {s : } (hs : s 0) (hs' : s 1) :

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

theorem differentiable_at_riemann_zeta {s : } (hs' : s 1) :

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

theorem riemann_zeta_neg_two_mul_nat_add_one (n : ) :
riemann_zeta ((-2) * (n + 1)) = 0

The trivial zeroes of the zeta function.

def riemann_hypothesis  :
Prop

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

Equations

## Relating the Mellin transforms of the two zeta kernels #

theorem has_mellin_one_div_sqrt_Ioc {s : } (hs : 1 / 2 < s.re) :
has_mellin ((set.Ioc 0 1).indicator (λ (t : ), 1 / ( t))) s (1 / (s - 1 / 2))
theorem has_mellin_one_div_sqrt_sub_one_div_two_Ioc {s : } (hs : 1 / 2 < s.re) :
has_mellin ((set.Ioc 0 1).indicator (λ (t : ), (1 - 1 / ( t)) / 2)) s (1 / (2 * s) - 1 / (2 * s - 1))

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

theorem mellin_zeta_kernel₂_eq_of_lt_re {s : } (hs : 1 / 2 < s.re) :
= + 1 / (2 * s) - 1 / (2 * s - 1)
theorem completed_zeta_eq_mellin_of_one_lt_re {s : } (hs : 1 < s.re) :

## 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 , t ^ (s - 1) * (rexp * (n + 1) ^ 2)) = * (1 / (n + 1) ^ (2 * s))

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

theorem mellin_zeta_kernel₁_eq_tsum {s : } (hs : 1 / 2 < s.re) :
= * ∑' (n : ), 1 / (n + 1) ^ (2 * s)
theorem completed_zeta_eq_tsum_of_one_lt_re {s : } (hs : 1 < s.re) :
= 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) :
= ∑' (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) :
= ∑' (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) :
= ∑' (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 riemann_zeta_two_mul_nat {k : } (hk : k 0) :
riemann_zeta (2 * k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * real.pi ^ (2 * k) * (bernoulli (2 * k)) / ((2 * k).factorial)

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 has_sum_zeta_nat for a version formulated explicitly as a sum, and riemann_zeta_neg_nat_eq_bernoulli for values at negative integers (equivalent to the above via the functional equation).

theorem riemann_zeta_two  :
= / 6
theorem riemann_zeta_four  :
= / 90

## Functional equation #

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

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

theorem riemann_zeta_one_sub {s : } (hs : (n : ), s -n) (hs' : s 1) :
riemann_zeta (1 - s) = 2 ^ (1 - s) * * * complex.sin (real.pi * (1 - s) / 2) *

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 riemann_zeta_neg_nat_eq_bernoulli (k : ) :
= (-1) ^ k * (bernoulli (k + 1)) / (k + 1)