Documentation

Mathlib.NumberTheory.Bernoulli

Bernoulli numbers #

The Bernoulli numbers are a sequence of rational numbers that frequently show up in number theory.

Mathematical overview #

The Bernoulli numbers $(B_0, B_1, B_2, \ldots)=(1, -1/2, 1/6, 0, -1/30, \ldots)$ are a sequence of rational numbers. They show up in the formula for the sums of $k$th powers. They are related to the Taylor series expansions of $x/\tan(x)$ and of $\coth(x)$, and also show up in the values that the Riemann Zeta function takes both at both negative and positive integers (and hence in the theory of modular forms). For example, if $1 \leq n$ is even then

$$\zeta(2n)=\sum_{t\geq1}t^{-2n}=(-1)^{n+1}\frac{(2\pi)^{2n}B_{2n}}{2(2n)!}.$$

Note however that this result is not yet formalised in Lean.

The Bernoulli numbers can be formally defined using the power series

$$\sum B_n\frac{t^n}{n!}=\frac{t}{1-e^{-t}}$$

although that happens to not be the definition in mathlib (this is an implementation detail and need not concern the mathematician).

Note that $B_1=-1/2$, meaning that we are using the $B_n^-$ of from Wikipedia.

Implementation detail #

The Bernoulli numbers are defined using well-founded induction, by the formula $$B_n=1-\sum_{k\lt n}\frac{\binom{n}{k}}{n-k+1}B_k.$$ This formula is true for all $n$ and in particular $B_0=1$. Note that this is the definition for positive Bernoulli numbers, which we call bernoulli'. The negative Bernoulli numbers are then defined as bernoulli := (-1)^n * bernoulli'.

Main theorems #

sum_bernoulli : ∑ k in Finset.range n, (n.choose k : ℚ) * bernoulli k = if n = 1 then 1 else 0

Definitions #

source
def bernoulli' :
ℕ → ℚ

The Bernoulli numbers: the $n$-th Bernoulli number $B_n$ is defined recursively via $$B_n = 1 - \sum_{k < n} \binom{n}{k}\frac{B_k}{n+1-k}$$

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem bernoulli'_def' (n : ℕ) :
    bernoulli' n = 1 - Finset.sum Finset.univ fun (k : Fin n) => ↑(Nat.choose n ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k
    source
    theorem bernoulli'_def (n : ℕ) :
    bernoulli' n = 1 - Finset.sum (Finset.range n) fun (k : ℕ) => ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k
    source
    theorem bernoulli'_spec (n : ℕ) :
    (Finset.sum (Finset.range (Nat.succ n)) fun (k : ℕ) => ↑(Nat.choose n (n - k)) / (↑n - ↑k + 1) * bernoulli' k) = 1
    source
    theorem bernoulli'_spec' (n : ℕ) :
    (Finset.sum (Finset.antidiagonal n) fun (k : ℕ × ℕ) => ↑(Nat.choose (k.1 + k.2) k.2) / (↑k.2 + 1) * bernoulli' k.1) = 1

    Examples #

    source
    @[simp]
    theorem bernoulli'_zero :
    bernoulli' 0 = 1
    source
    @[simp]
    theorem bernoulli'_one :
    bernoulli' 1 = 1 / 2
    source
    @[simp]
    theorem bernoulli'_two :
    bernoulli' 2 = 1 / 6
    source
    @[simp]
    theorem bernoulli'_three :
    bernoulli' 3 = 0
    source
    @[simp]
    theorem bernoulli'_four :
    bernoulli' 4 = -1 / 30
    source
    @[simp]
    theorem sum_bernoulli' (n : ℕ) :
    (Finset.sum (Finset.range n) fun (k : ℕ) => ↑(Nat.choose n k) * bernoulli' k) = ↑n
    source
    def bernoulli'PowerSeries (A : Type u_1) [CommRing A] [Algebra ℚ A] :
    PowerSeries A

    The exponential generating function for the Bernoulli numbers bernoulli' n.

    Equations
    Instances For
      source
      theorem bernoulli'PowerSeries_mul_exp_sub_one (A : Type u_1) [CommRing A] [Algebra ℚ A] :
      bernoulli'PowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X * PowerSeries.exp A
      source
      theorem bernoulli'_odd_eq_zero {n : ℕ} (h_odd : Odd n) (hlt : 1 < n) :
      bernoulli' n = 0

      Odd Bernoulli numbers (greater than 1) are zero.

      source
      def bernoulli (n : ℕ) :
      ℚ

      The Bernoulli numbers are defined to be bernoulli' with a parity sign.

      Equations
      Instances For
        source
        theorem bernoulli'_eq_bernoulli (n : ℕ) :
        bernoulli' n = (-1) ^ n * bernoulli n
        source
        @[simp]
        theorem bernoulli_zero :
        bernoulli 0 = 1
        source
        @[simp]
        theorem bernoulli_one :
        bernoulli 1 = -1 / 2
        source
        theorem bernoulli_eq_bernoulli'_of_ne_one {n : ℕ} (hn : n ≠ 1) :
        bernoulli n = bernoulli' n
        source
        @[simp]
        theorem sum_bernoulli (n : ℕ) :
        (Finset.sum (Finset.range n) fun (k : ℕ) => ↑(Nat.choose n k) * bernoulli k) = if n = 1 then 1 else 0
        source
        theorem bernoulli_spec' (n : ℕ) :
        (Finset.sum (Finset.antidiagonal n) fun (k : ℕ × ℕ) => ↑(Nat.choose (k.1 + k.2) k.2) / (↑k.2 + 1) * bernoulli k.1) = if n = 0 then 1 else 0
        source
        def bernoulliPowerSeries (A : Type u_1) [CommRing A] [Algebra ℚ A] :
        PowerSeries A

        The exponential generating function for the Bernoulli numbers bernoulli n.

        Equations
        Instances For
          source
          theorem bernoulliPowerSeries_mul_exp_sub_one (A : Type u_1) [CommRing A] [Algebra ℚ A] :
          bernoulliPowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X
          source
          theorem sum_range_pow (n : ℕ) (p : ℕ) :
          (Finset.sum (Finset.range n) fun (k : ℕ) => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun (i : ℕ) => bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)

          Faulhaber's theorem relating the sum of p-th powers to the Bernoulli numbers: $$\sum_{k=0}^{n-1} k^p = \sum_{i=0}^p B_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$ See https://proofwiki.org/wiki/Faulhaber%27s_Formula and [orosi2018faulhaber] for the proof provided here.

          source
          theorem sum_Ico_pow (n : ℕ) (p : ℕ) :
          (Finset.sum (Finset.Ico 1 (n + 1)) fun (k : ℕ) => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun (i : ℕ) => bernoulli' i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)

          Alternate form of Faulhaber's theorem, relating the sum of p-th powers to the Bernoulli numbers: $$\sum_{k=1}^{n} k^p = \sum_{i=0}^p (-1)^iB_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$ Deduced from sum_range_pow.