Bernoulli polynomials

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

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

noncomputable def Polynomial.bernoulli (n : ℕ) : Polynomial ℚ

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

Equations

• Polynomial.bernoulli n = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial (n - i)) (bernoulli i * ↑(n.choose i))

theorem Polynomial.bernoulli_def (n : ℕ) : bernoulli n = ∑ i ∈ Finset.range (n + 1), (monomial i) (_root_.bernoulli (n - i) * ↑(n.choose i))

theorem Polynomial.coeff_bernoulli (n i : ℕ) : (bernoulli n).coeff i = if i ≤ n then _root_.bernoulli (n - i) * ↑(n.choose i) else 0

@[simp]

theorem Polynomial.bernoulli_zero : bernoulli 0 = 1

@[simp]

theorem Polynomial.bernoulli_one : bernoulli 1 = X - C 2⁻¹

@[simp]

theorem Polynomial.bernoulli_eval_zero (n : ℕ) : eval 0 (bernoulli n) = _root_.bernoulli n

@[simp]

theorem Polynomial.bernoulli_eval_one (n : ℕ) : eval 1 (bernoulli n) = bernoulli' n

theorem Polynomial.bernoulli_three_eval_one_quarter : eval (1 / 4) (bernoulli 3) = 3 / 64

theorem Polynomial.derivative_bernoulli_add_one (k : ℕ) : derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k

theorem Polynomial.derivative_bernoulli (k : ℕ) : derivative (bernoulli k) = ↑k * bernoulli (k - 1)

@[simp]

theorem Polynomial.sum_bernoulli (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑((n + 1).choose k) • bernoulli k = (monomial n) (↑n + 1)

theorem Polynomial.bernoulli_eq_sub_sum (n : ℕ) : (n + 1) • bernoulli n = (n + 1) • X ^ n - ∑ k ∈ Finset.range n, (n + 1).choose k • bernoulli k

Another version of Polynomial.sum_bernoulli.

theorem Polynomial.sum_range_pow_eq_bernoulli_sub (n p : ℕ) : (↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ

Another version of sum_range_pow.

theorem Polynomial.bernoulli_succ_eval (n p : ℕ) : eval (↑n) (bernoulli p.succ) = _root_.bernoulli p.succ + (↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p

Rearrangement of Polynomial.sum_range_pow_eq_bernoulli_sub.

theorem Polynomial.bernoulli_comp_one_add_X (n : ℕ) : (bernoulli n).comp (1 + X) = bernoulli n + n • X ^ (n - 1)

theorem Polynomial.bernoulli_eval_one_add (n : ℕ) (x : ℚ) : eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)

theorem Polynomial.bernoulli_comp_neg_X (n : ℕ) : (bernoulli n).comp (-X) = (-1) ^ n • (bernoulli n + n • X ^ (n - 1))

theorem Polynomial.bernoulli_eval_neg (n : ℕ) (x : ℚ) : eval (-x) (bernoulli n) = (-1) ^ n * (eval x (bernoulli n) + ↑n * x ^ (n - 1))

theorem Polynomial.bernoulli_comp_one_sub_X (n : ℕ) : (bernoulli n).comp (1 - X) = (-1) ^ n * bernoulli n

theorem Polynomial.bernoulli_eval_one_sub (n : ℕ) (x : ℚ) : eval (1 - x) (bernoulli n) = (-1) ^ n * eval x (bernoulli n)

theorem Polynomial.bernoulli_generating_function {A : Type u_1} [CommRing A] [Algebra ℚ A] (t : A) : (PowerSeries.mk fun (n : ℕ) => (aeval t) ((1 / ↑n.factorial) • bernoulli n)) * (PowerSeries.exp A - 1) = PowerSeries.X * (PowerSeries.rescale t) (PowerSeries.exp A)

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