# 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.

## 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
Instances For
theorem Polynomial.bernoulli_def (n : ) :
= Finset.sum (Finset.range (n + 1)) fun (i : ) => (bernoulli (n - i) * ())
theorem Polynomial.derivative_bernoulli_add_one (k : ) :
Polynomial.derivative (Polynomial.bernoulli (k + 1)) = (k + 1) *
theorem Polynomial.derivative_bernoulli (k : ) :
Polynomial.derivative = k * Polynomial.bernoulli (k - 1)
@[simp]
theorem Polynomial.sum_bernoulli (n : ) :
(Finset.sum (Finset.range (n + 1)) fun (k : ) => (Nat.choose (n + 1) k) ) = (n + 1)
theorem Polynomial.bernoulli_eq_sub_sum (n : ) :
= () - Finset.sum () fun (k : ) => (Nat.choose (n + 1) k)

Another version of Polynomial.sum_bernoulli.

theorem Polynomial.sum_range_pow_eq_bernoulli_sub (n : ) (p : ) :
((p + 1) * Finset.sum () fun (k : ) => k ^ p) = Polynomial.eval (n) () -

Another version of sum_range_pow.

theorem Polynomial.bernoulli_succ_eval (n : ) (p : ) :
Polynomial.eval (n) () = + (p + 1) * Finset.sum () fun (k : ) => k ^ p

Rearrangement of Polynomial.sum_range_pow_eq_bernoulli_sub.

theorem Polynomial.bernoulli_eval_one_add (n : ) (x : ) :
Polynomial.eval (1 + x) = + n * x ^ (n - 1)
theorem Polynomial.bernoulli_generating_function {A : Type u_1} [] [] (t : A) :
(PowerSeries.mk fun (n : ) => () ((1 / ()) )) * () = PowerSeries.X *

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