Documentation

Mathlib.NumberTheory.ZetaValues

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

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

def bernoulliFun (k : ) (x : ) :

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

Equations
Instances For
    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
    Instances For
      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ₖ.

      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 : ) :
      bernoulliFourierCoeff k n = -k.factorial / (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.

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

      Equations
      Instances For
        theorem fourierCoeff_bernoulli_eq {k : } (hk : k 0) (n : ) :
        theorem summable_bernoulli_fourier {k : } (hk : 2 k) :
        Summable fun (n : ) => -k.factorial / (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 / k.factorial * (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 / k.factorial * (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) * (2 * Real.pi * n * x).cos) ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k) / 2 / (2 * k).factorial * 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) * (2 * Real.pi * n * x).sin) ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k + 1) / 2 / (2 * k + 1).factorial * 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)) / (2 * k).factorial)
        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 hasSum_L_function_mod_four_eval_three :
        HasSum (fun (n : ) => 1 / n ^ 3 * (Real.pi * n / 2).sin) (Real.pi ^ 3 / 32)

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