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 #

sum_bernoulli_poly: The sum of the $k^\mathrm{th}$ Bernoulli polynomial with binomial coefficients up to n is (n + 1) * X^n.
exp_bernoulli_poly: The Bernoulli polynomials act as generating functions for the exponential.

TODO #

bernoulli_poly_eval_one_neg : $$ B_n(1 - x) = (-1)^n*B_n(x) $$
``bernoulli_poly_eval_one: Follows as a consequence ofbernoulli_poly_eval_one_neg`.

source

def bernoulli_poly (n : ℕ) :

polynomial ℚ

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

Equations

bernoulli_poly n = ∑ (i : ℕ) in finset.range (n + 1), ⇑(polynomial.monomial (n - i)) ((bernoulli i) * ↑(n.choose i))

source

theorem bernoulli_poly_def (n : ℕ) :

bernoulli_poly n = ∑ (i : ℕ) in finset.range (n + 1), ⇑(polynomial.monomial i) ((bernoulli (n - i)) * ↑(n.choose i))

source

@[simp]

theorem bernoulli_poly.bernoulli_poly_zero :

bernoulli_poly 0 = 1

source

@[simp]

theorem bernoulli_poly.bernoulli_poly_eval_zero (n : ℕ) :

polynomial.eval 0 (bernoulli_poly n) = bernoulli n

source

@[simp]

theorem bernoulli_poly.bernoulli_poly_eval_one (n : ℕ) :

polynomial.eval 1 (bernoulli_poly n) = bernoulli' n

source

@[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)

source

theorem bernoulli_poly.exp_bernoulli_poly' {A : Type u_1} [comm_ring A] [algebra ℚ A] (t : A) :

(power_series.mk (λ (n : ℕ), ⇑(polynomial.aeval t) ((1 / ↑n!) • bernoulli_poly n))) * (power_series.exp A - 1) = power_series.X * ⇑(power_series.rescale t) (power_series.exp A)

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