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

• bernoulliFun k x = Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k))

theorem bernoulliFun_eval_zero (k : ℕ) : bernoulliFun k 0 = ↑(bernoulli k)

theorem bernoulliFun_endpoints_eq_of_ne_one {k : ℕ} (hk : k ≠ 1) : bernoulliFun k 1 = bernoulliFun k 0

theorem bernoulliFun_eval_one (k : ℕ) : bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

theorem hasDerivAt_bernoulliFun (k : ℕ) (x : ℝ) : HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x

theorem antideriv_bernoulliFun (k : ℕ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x

theorem integral_bernoulliFun_eq_zero {k : ℕ} (hk : k ≠ 0) : ∫ (x : ℝ) in 0 ..1, bernoulliFun k x = 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

• bernoulliFourierCoeff k n = fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun (x : ℝ) => ↑(bernoulliFun k x)) n

theorem bernoulliFourierCoeff_recurrence (k : ℕ) {n : ℤ} (hn : n ≠ 0) : bernoulliFourierCoeff k n = 1 / (-2 * ↑Real.pi * 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) : bernoulliFourierCoeff 0 n = 0

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

theorem bernoulliFourierCoeff_zero {k : ℕ} (hk : k ≠ 0) : bernoulliFourierCoeff k 0 = 0

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

theorem bernoulliFourierCoeff_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) : bernoulliFourierCoeff k n = -↑(Nat.factorial k) / (2 * ↑Real.pi * Complex.I * ↑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.

def periodizedBernoulli (k : ℕ) : UnitAddCircle → ℝ

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

Equations

• periodizedBernoulli k = AddCircle.liftIco 1 0 (bernoulliFun k)

theorem periodizedBernoulli.continuous {k : ℕ} (hk : k ≠ 1) : Continuous (periodizedBernoulli k)

theorem fourierCoeff_bernoulli_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) : fourierCoeff (Complex.ofReal' ∘ periodizedBernoulli k) n = -↑(Nat.factorial k) / (2 * ↑Real.pi * Complex.I * ↑n) ^ k

theorem summable_bernoulli_fourier {k : ℕ} (hk : 2 ≤ k) : Summable fun (n : ℤ) => -↑(Nat.factorial k) / (2 * ↑Real.pi * Complex.I * ↑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 * (fourier n) ↑x) (-(2 * ↑Real.pi * Complex.I) ^ k / ↑(Nat.factorial k) * ↑(bernoulliFun k x))

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)) (-(2 * ↑Real.pi * Complex.I) ^ k / ↑(Nat.factorial k) * ↑(bernoulliFun k x))

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) * Real.cos (2 * Real.pi * ↑n * x)) ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k) / 2 / ↑(Nat.factorial (2 * k)) * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (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) * Real.sin (2 * Real.pi * ↑n * x)) ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k + 1) / 2 / ↑(Nat.factorial (2 * k + 1)) * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (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)) / ↑(Nat.factorial (2 * k)))

theorem hasSum_zeta_two : HasSum (fun (n : ℕ) => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)

theorem hasSum_zeta_four : HasSum (fun (n : ℕ) => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90)

theorem Polynomial.bernoulli_three_eval_one_quarter : Polynomial.eval (1 / 4) (Polynomial.bernoulli 3) = 3 / 64

theorem hasSum_L_function_mod_four_eval_three : HasSum (fun (n : ℕ) => 1 / ↑n ^ 3 * Real.sin (Real.pi * ↑n / 2)) (Real.pi ^ 3 / 32)

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