Documentation

Mathlib.NumberTheory.BernoulliPolynomials

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 #

TODO #

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

Equations
Instances For
    theorem Polynomial.bernoulli_def (n : ) :
    Polynomial.bernoulli n = iFinset.range (n + 1), (Polynomial.monomial i) (bernoulli (n - i) * (n.choose i))
    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 : ) :
    kFinset.range (n + 1), ((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 - kFinset.range n, ((n + 1).choose k) Polynomial.bernoulli k

    Another version of Polynomial.sum_bernoulli.

    theorem Polynomial.sum_range_pow_eq_bernoulli_sub (n : ) (p : ) :
    (p + 1) * kFinset.range n, k ^ p = Polynomial.eval (n) (Polynomial.bernoulli p.succ) - bernoulli p.succ

    Another version of sum_range_pow.

    theorem Polynomial.bernoulli_succ_eval (n : ) (p : ) :
    Polynomial.eval (n) (Polynomial.bernoulli p.succ) = bernoulli p.succ + (p + 1) * kFinset.range n, k ^ p

    Rearrangement of Polynomial.sum_range_pow_eq_bernoulli_sub.

    theorem Polynomial.bernoulli_generating_function {A : Type u_1} [CommRing A] [Algebra A] (t : A) :
    (PowerSeries.mk fun (n : ) => (Polynomial.aeval t) ((1 / n.factorial) Polynomial.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}$