# mathlib3documentation

number_theory.zeta_values

# Critical values of the Riemann zeta function #

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

In this file we prove formulae for the critical values of ζ(s), and more generally of Hurwitz zeta functions, in terms of Bernoulli polynomials.

## Main results: #

• has_sum_zeta_nat: the final formula for zeta values, $$\zeta(2k) = \frac{(-1)^{(k + 1)} 2 ^ {2k - 1} \pi^{2k} B_{2 k}}{(2 k)!}.$$
• has_sum_zeta_two and has_sum_zeta_four: special cases given explicitly.
• has_sum_one_div_nat_pow_mul_cos: a formula for the sum ∑ (n : ℕ), cos (2 π i n x) / n ^ k as an explicit multiple of Bₖ(x), for any x ∈ [0, 1] and k ≥ 2 even.
• has_sum_one_div_nat_pow_mul_sin: a formula for the sum ∑ (n : ℕ), sin (2 π i n x) / n ^ k as an explicit multiple of Bₖ(x), for any x ∈ [0, 1] and k ≥ 3 odd.

Simple properties of the Bernoulli polynomial, as a function ℝ → ℝ.

noncomputable def bernoulli_fun (k : ) (x : ) :

The function x ↦ Bₖ(x) : ℝ → ℝ.

Equations
theorem bernoulli_fun_endpoints_eq_of_ne_one {k : } (hk : k 1) :
=
theorem bernoulli_fun_eval_one (k : ) :
= + ite (k = 1) 1 0
theorem has_deriv_at_bernoulli_fun (k : ) (x : ) :
(k * bernoulli_fun (k - 1) x) x
theorem antideriv_bernoulli_fun (k : ) (x : ) :
has_deriv_at (λ (x : ), bernoulli_fun (k + 1) x / (k + 1)) x) x
theorem integral_bernoulli_fun_eq_zero {k : } (hk : k 0) :
(x : ) in 0..1, = 0

Compute the Fourier coefficients of the Bernoulli functions via integration by parts.

noncomputable def bernoulli_fourier_coeff (k : ) (n : ) :

The n-th Fourier coefficient of the k-th Bernoulli function on the interval [0, 1].

Equations
theorem bernoulli_fourier_coeff_recurrence (k : ) {n : } (hn : n 0) :
= 1 / ((-2) * real.pi * complex.I * n) * (ite (k = 1) 1 0 - k * bernoulli_fourier_coeff (k - 1) n)

Recurrence relation (in k) for the n-th Fourier coefficient of Bₖ.

theorem bernoulli_zero_fourier_coeff {n : } (hn : n 0) :

The Fourier coefficients of B₀(x) = 1.

theorem bernoulli_fourier_coeff_zero {k : } (hk : k 0) :

The 0-th Fourier coefficient of Bₖ(x).

theorem bernoulli_fourier_coeff_eq {k : } (hk : k 0) (n : ) :
= -(k.factorial) / * n) ^ k

In this section we use the above evaluations of the Fourier coefficients of Bernoulli polynomials, together with the theorem has_pointwise_sum_fourier_series_of_summable from Fourier theory, to obtain an explicit formula for ∑ (n:ℤ), 1 / n ^ k * fourier n x.

noncomputable def periodized_bernoulli (k : ) :

The Bernoulli polynomial, extended from [0, 1) to the unit circle.

Equations
theorem periodized_bernoulli.continuous {k : } (hk : k 1) :
theorem fourier_coeff_bernoulli_eq {k : } (hk : k 0) (n : ) :
= -(k.factorial) / * n) ^ k
theorem summable_bernoulli_fourier {k : } (hk : 2 k) :
summable (λ (n : ), -(k.factorial) / * n) ^ k)
theorem has_sum_one_div_pow_mul_fourier_mul_bernoulli_fun {k : } (hk : 2 k) {x : } (hx : x 1) :
has_sum (λ (n : ), 1 / n ^ k * (fourier n) x) (- * complex.I) ^ k / (k.factorial) * x))
theorem has_sum_one_div_nat_pow_mul_fourier {k : } (hk : 2 k) {x : } (hx : x 1) :
has_sum (λ (n : ), 1 / n ^ k * ((fourier n) x + (-1) ^ k * (fourier (-n)) x)) (- * complex.I) ^ k / (k.factorial) * x))
theorem has_sum_one_div_nat_pow_mul_cos {k : } (hk : k 0) {x : } (hx : x 1) :
has_sum (λ (n : ), 1 / n ^ (2 * k) * real.cos (2 * real.pi * n * x)) ((-1) ^ (k + 1) * (2 * real.pi) ^ (2 * k) / 2 / ((2 * k).factorial) * (polynomial.bernoulli (2 * k))))
theorem has_sum_one_div_nat_pow_mul_sin {k : } (hk : k 0) {x : } (hx : x 1) :
has_sum (λ (n : ), 1 / n ^ (2 * k + 1) * real.sin (2 * real.pi * n * x)) ((-1) ^ (k + 1) * (2 * real.pi) ^ (2 * k + 1) / 2 / ((2 * k + 1).factorial) * (polynomial.bernoulli (2 * k + 1))))
theorem has_sum_zeta_nat {k : } (hk : k 0) :
has_sum (λ (n : ), 1 / n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * real.pi ^ (2 * k) * (bernoulli (2 * k)) / ((2 * k).factorial))
theorem has_sum_zeta_two  :
has_sum (λ (n : ), 1 / n ^ 2) (real.pi ^ 2 / 6)
theorem has_sum_zeta_four  :
has_sum (λ (n : ), 1 / n ^ 4) (real.pi ^ 4 / 90)
theorem has_sum_L_function_mod_four_eval_three  :
has_sum (λ (n : ), 1 / n ^ 3 * real.sin / 2)) (real.pi ^ 3 / 32)

Explicit formula for L(χ, 3), where χ is the unique nontrivial Dirichlet character modulo 4.