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 ton
is(n + 1) * X^n
.polynomial.bernoulli_generating_function
: The Bernoulli polynomials act as generating functions for the exponential.
TODO #
bernoulli_eval_one_neg
: $$ B_n(1 - x) = (-1)^n B_n(x) $$
The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers.
Equations
- polynomial.bernoulli n = (finset.range (n + 1)).sum (λ (i : ℕ), ⇑(polynomial.monomial (n - i)) (bernoulli i * ↑(n.choose i)))
theorem
polynomial.bernoulli_def
(n : ℕ) :
polynomial.bernoulli n = (finset.range (n + 1)).sum (λ (i : ℕ), ⇑(polynomial.monomial i) (bernoulli (n - i) * ↑(n.choose i)))
@[simp]
@[simp]
theorem
polynomial.derivative_bernoulli_add_one
(k : ℕ) :
⇑polynomial.derivative (polynomial.bernoulli (k + 1)) = (↑k + 1) * polynomial.bernoulli k
theorem
polynomial.derivative_bernoulli
(k : ℕ) :
⇑polynomial.derivative (polynomial.bernoulli k) = ↑k * polynomial.bernoulli (k - 1)
@[simp]
theorem
polynomial.sum_bernoulli
(n : ℕ) :
(finset.range (n + 1)).sum (λ (k : ℕ), ↑((n + 1).choose k) • polynomial.bernoulli k) = ⇑(polynomial.monomial n) (↑n + 1)
theorem
polynomial.bernoulli_eq_sub_sum
(n : ℕ) :
↑(n.succ) • polynomial.bernoulli n = ⇑(polynomial.monomial n) ↑(n.succ) - (finset.range n).sum (λ (k : ℕ), ↑((n + 1).choose k) • polynomial.bernoulli k)
Another version of polynomial.sum_bernoulli
.
Another version of bernoulli.sum_range_pow
.
Rearrangement of polynomial.sum_range_pow_eq_bernoulli_sub
.
theorem
polynomial.bernoulli_eval_one_add
(n : ℕ)
(x : ℚ) :
polynomial.eval (1 + x) (polynomial.bernoulli n) = polynomial.eval x (polynomial.bernoulli n) + ↑n * x ^ (n - 1)
theorem
polynomial.bernoulli_generating_function
{A : Type u_1}
[comm_ring A]
[algebra ℚ A]
(t : A) :
power_series.mk (λ (n : ℕ), ⇑(polynomial.aeval t) ((1 / ↑(n.factorial)) • polynomial.bernoulli 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}