mathlib3 documentation

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

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

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

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

Equations
theorem bernoulli_fun_eval_one (k : ) :
bernoulli_fun k 1 = bernoulli_fun k 0 + ite (k = 1) 1 0
theorem antideriv_bernoulli_fun (k : ) (x : ) :
has_deriv_at (λ (x : ), bernoulli_fun (k + 1) x / (k + 1)) (bernoulli_fun k x) x
theorem integral_bernoulli_fun_eq_zero {k : } (hk : k 0) :
(x : ) in 0..1, bernoulli_fun k x = 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) :

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).

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 summable_bernoulli_fourier {k : } (hk : 2 k) :
theorem has_sum_one_div_pow_mul_fourier_mul_bernoulli_fun {k : } (hk : 2 k) {x : } (hx : x set.Icc 0 1) :
has_sum (λ (n : ), 1 / n ^ k * (fourier n) x) (-(2 * real.pi * complex.I) ^ k / (k.factorial) * (bernoulli_fun k x))
theorem has_sum_one_div_nat_pow_mul_fourier {k : } (hk : 2 k) {x : } (hx : x set.Icc 0 1) :
has_sum (λ (n : ), 1 / n ^ k * ((fourier n) x + (-1) ^ k * (fourier (-n)) x)) (-(2 * real.pi * complex.I) ^ k / (k.factorial) * (bernoulli_fun k x))
theorem has_sum_one_div_nat_pow_mul_cos {k : } (hk : k 0) {x : } (hx : x set.Icc 0 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.eval x (polynomial.map (algebra_map ) (polynomial.bernoulli (2 * k))))
theorem has_sum_one_div_nat_pow_mul_sin {k : } (hk : k 0) {x : } (hx : x set.Icc 0 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.eval x (polynomial.map (algebra_map ) (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 (real.pi * n / 2)) (real.pi ^ 3 / 32)

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