mathlib documentation

number_theory.bernoulli

Bernoulli numbers

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

For example, they show up in the Taylor series of many trigonometric and hyperbolic functions, and also as (integral multiples of products of powers of π and) special values of the Riemann zeta function. (Note: these facts are not yet available in mathlib)

In this file, we provide the definition, and the basic fact (sum_bernoulli) that $$ \sum_{k < n} \binom{n}{k} * B_k = n, $$ where $B_k$ denotes the the $k$-th Bernoulli number.

source
def bernoulli  :
ℕ → ℚ

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

Equations
source
theorem bernoulli_def' (n : ℕ) :
bernoulli n = 1 - ∑ (k : fin n), (↑(n.choose ↑k)) * bernoulli ↑k / (↑n + 1 - ↑k)

source
theorem bernoulli_def (n : ℕ) :
bernoulli n = 1 - ∑ (k : ℕ) in finset.range n, (↑(n.choose k)) * bernoulli k / (↑n + 1 - ↑k)

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 : ℕ) :
∑ (k : ℕ) in finset.range n, (↑(n.choose k)) * bernoulli k = ↑n