# Critical values of the Riemann zeta function #

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: #

• hasSum_zeta_nat: the final formula for zeta values, $$\zeta(2k) = \frac{(-1)^{(k + 1)} 2 ^ {2k - 1} \pi^{2k} B_{2 k}}{(2 k)!}.$$
• hasSum_zeta_two and hasSum_zeta_four: special cases given explicitly.
• hasSum_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.
• hasSum_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 ℝ → ℝ.

def bernoulliFun (k : ) (x : ) :

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

Equations
Instances For
theorem bernoulliFun_eval_zero (k : ) :
= ()
theorem bernoulliFun_eval_one (k : ) :
= + if k = 1 then 1 else 0
theorem hasDerivAt_bernoulliFun (k : ) (x : ) :
HasDerivAt () (k * bernoulliFun (k - 1) x) x
theorem antideriv_bernoulliFun (k : ) (x : ) :
HasDerivAt (fun (x : ) => bernoulliFun (k + 1) x / (k + 1)) () x
theorem integral_bernoulliFun_eq_zero {k : } (hk : k 0) :
∫ (x : ) in 0 ..1, = 0

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

def bernoulliFourierCoeff (k : ) (n : ) :

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

Equations
Instances For
theorem bernoulliFourierCoeff_recurrence (k : ) {n : } (hn : n 0) :
= 1 / (-2 * * Complex.I * n) * ((if k = 1 then 1 else 0) - k * bernoulliFourierCoeff (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 bernoulliFourierCoeff_zero {k : } (hk : k 0) :

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

theorem bernoulliFourierCoeff_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.

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

Equations
Instances For
theorem periodizedBernoulli.continuous {k : } (hk : k 1) :
theorem fourierCoeff_bernoulli_eq {k : } (hk : k 0) (n : ) :
= -k.factorial / ( * n) ^ k
theorem summable_bernoulli_fourier {k : } (hk : 2 k) :
Summable fun (n : ) => -k.factorial / ( * n) ^ k
theorem hasSum_one_div_pow_mul_fourier_mul_bernoulliFun {k : } (hk : 2 k) {x : } (hx : x Set.Icc 0 1) :
HasSum (fun (n : ) => 1 / n ^ k * () x) (-() ^ k / k.factorial * ())
theorem hasSum_one_div_nat_pow_mul_fourier {k : } (hk : 2 k) {x : } (hx : x Set.Icc 0 1) :
HasSum (fun (n : ) => 1 / n ^ k * ((fourier n) x + (-1) ^ k * (fourier (-n)) x)) (-() ^ k / k.factorial * ())
theorem hasSum_one_div_nat_pow_mul_cos {k : } (hk : k 0) {x : } (hx : x Set.Icc 0 1) :
HasSum (fun (n : ) => 1 / n ^ (2 * k) * ( * n * x).cos) ((-1) ^ (k + 1) * () ^ (2 * k) / 2 / (2 * k).factorial * Polynomial.eval x (Polynomial.map () (Polynomial.bernoulli (2 * k))))
theorem hasSum_one_div_nat_pow_mul_sin {k : } (hk : k 0) {x : } (hx : x Set.Icc 0 1) :
HasSum (fun (n : ) => 1 / n ^ (2 * k + 1) * ( * n * x).sin) ((-1) ^ (k + 1) * () ^ (2 * k + 1) / 2 / (2 * k + 1).factorial * Polynomial.eval x (Polynomial.map () (Polynomial.bernoulli (2 * k + 1))))
theorem hasSum_zeta_nat {k : } (hk : k 0) :
HasSum (fun (n : ) => 1 / n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * Real.pi ^ (2 * k) * (bernoulli (2 * k)) / (2 * k).factorial)
theorem hasSum_zeta_two :
HasSum (fun (n : ) => 1 / n ^ 2) ( / 6)
theorem hasSum_zeta_four :
HasSum (fun (n : ) => 1 / n ^ 4) ( / 90)
theorem hasSum_L_function_mod_four_eval_three :
HasSum (fun (n : ) => 1 / n ^ 3 * (Real.pi * n / 2).sin) ( / 32)

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