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 ℝ → ℝ.

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

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.