# mathlib3documentation

number_theory.bernoulli_polynomials

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

## TODO #

• bernoulli_eval_one_neg : $$B_n(1 - x) = (-1)^n B_n(x)$$
noncomputable def polynomial.bernoulli (n : ) :

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

Equations
theorem polynomial.bernoulli_def (n : ) :
= (finset.range (n + 1)).sum (λ (i : ), (bernoulli (n - i) * (n.choose i)))
@[simp]
@[simp]
@[simp]
@[simp]
theorem polynomial.sum_bernoulli (n : ) :
(finset.range (n + 1)).sum (λ (k : ), ((n + 1).choose k) = (n + 1)
theorem polynomial.bernoulli_eq_sub_sum (n : ) :
= (n.succ) - (finset.range n).sum (λ (k : ), ((n + 1).choose k)

Another version of polynomial.sum_bernoulli.

theorem polynomial.sum_range_pow_eq_bernoulli_sub (n p : ) :
(p + 1) * (finset.range n).sum (λ (k : ), k ^ p) =

Another version of bernoulli.sum_range_pow.

theorem polynomial.bernoulli_succ_eval (n p : ) :
= + (p + 1) * (finset.range n).sum (λ (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} [comm_ring A] [ A] (t : A) :
power_series.mk (λ (n : ), ((1 / (n.factorial)) * - 1) =

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