mathlib3 documentation


Bernoulli polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The 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, $$ \frac{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 #


noncomputable def polynomial.bernoulli (n : ) :

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

theorem polynomial.sum_bernoulli (n : ) :

Another version of bernoulli.sum_range_pow.

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