mathlib documentation

number_theory.bernoulli_polynomials

Bernoulli polynomials #

The Bernoulli polynomials (defined here : https://en.wikipedia.org/wiki/Bernoulli_polynomials) are an important tool obtained from Bernoulli numbers.

Mathematical overview #

The $n$-th Bernoulli polynomial is defined as $$ B_n(X) = ∑_{k = 0}^n {n \choose k} (-1)^k * B_k * X^{n - k} $$ where $B_k$ is the $k$-th Bernoulli number. The Bernoulli polynomials are generating functions, $$ t * e^{tX} / (e^t - 1) = ∑_{n = 0}^{\infty} B_n(X) * \frac{t^n}{n!} $$

Implementation detail #

Bernoulli polynomials are defined using bernoulli, the Bernoulli numbers.

Main theorems #

TODO #

The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers.

Equations
theorem bernoulli_poly_def (n : ) :
bernoulli_poly n = ∑ (i : ) in finset.range (n + 1), (polynomial.monomial i) ((bernoulli (n - i)) * (n.choose i))
@[simp]
theorem bernoulli_poly.sum_bernoulli_poly (n : ) :
∑ (k : ) in finset.range (n + 1), ((n + 1).choose k) bernoulli_poly k = (polynomial.monomial n) (n + 1)

The theorem that ∑ Bₙ(t)X^n/n!)(e^X-1)=Xe^{tX}