Polynomial.bernoulli_eq_sub_sum
theorem Polynomial.bernoulli_eq_sub_sum :
∀ (n : ℕ),
↑n.succ • Polynomial.bernoulli n =
(Polynomial.monomial n) ↑n.succ - (Finset.range n).sum fun k => ↑((n + 1).choose k) • Polynomial.bernoulli k
This theorem, `Polynomial.bernoulli_eq_sub_sum`, states that for every natural number `n`, the Bernoulli polynomial `n.succ • Polynomial.bernoulli n` (where `n.succ` denotes the successor of `n`, i.e., `n+1`) is equal to the difference between the monomial `Polynomial.monomial n` with coefficient `n.succ` and the sum, over all natural numbers `k` less than `n`, of the product of the binomial coefficient `((n + 1).choose k)` and the Bernoulli polynomial `Polynomial.bernoulli k`. In other words, it expresses the Bernoulli polynomials in terms of a difference of a monomial and a sum over lower-order Bernoulli polynomials, with coefficients given by binomial coefficients.
More concisely: For every natural number `n`, the Bernoulli polynomial `n.succ * Polynomial.bernoulli n` equals the `n`-th degree monomial with coefficient `n.succ` minus the sum, over all natural numbers `k` less than `n`, of the product of the binomial coefficient `((n + 1).choose k)` and the Bernoulli polynomial `Polynomial.bernoulli k`.
|
Polynomial.sum_range_pow_eq_bernoulli_sub
theorem Polynomial.sum_range_pow_eq_bernoulli_sub :
∀ (n p : ℕ),
((↑p + 1) * (Finset.range n).sum fun k => ↑k ^ p) =
Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) - bernoulli p.succ
This theorem, named `Polynomial.sum_range_pow_eq_bernoulli_sub`, states that for any two natural numbers `n` and `p`, the product of `p+1` and the sum of the `p`-th powers of all natural numbers less than `n` is equal to the evaluation of the `p+1`-th Bernoulli polynomial at `n` minus the `p+1`-th Bernoulli number. In mathematical terms, it's expressing the relationship:
∀n, p ∈ ℕ, (p + 1) ∑_{k=0}^{n-1} k^p = B_{p+1}(n) - b_{p+1}
where B_{p+1}(n) represents the evaluation of the `p+1`-th Bernoulli polynomial at `n`, and b_{p+1} represents the `p+1`-th Bernoulli number.
More concisely: For any natural numbers `n` and `p`, the product of `p+1` and the sum of the `p`-th powers of the first `n` natural numbers equals the `p+1`-th Bernoulli number times `n` minus the `p+1`-th Bernoulli number. In Lean notation: `(p + 1) ∑ₙ k in n, k ^ p = B_(p+1) n - b_(p+1)`.
|
Polynomial.bernoulli_generating_function
theorem Polynomial.bernoulli_generating_function :
∀ {A : Type u_1} [inst : CommRing A] [inst_1 : 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 `Polynomial.bernoulli_generating_function` states that for any commutative ring `A` with an algebra structure over the rational numbers, and any element `t` in `A`, the power series obtained by multiplying `(e^X - 1)` and the series generated by evaluating the Bernoulli polynomials at `t` and scaling by the reciprocal of the factorial, equals to `X` times the power series for the exponential function, rescaled by `t`. In mathematical notation, this is saying that $(e^X - 1) * ∑ Bₙ(t)* X^n/n! = Xe^{tX}$. The Bernoulli polynomials, the exponential function, and the factorial function are all standard mathematical constructs which have been defined in the context of power series in Lean 4.
More concisely: For any commutative ring `A` with an algebra structure over the rational numbers and any element `t` in `A`, the generating function of Bernoulli polynomials evaluated at `t` multiplied by `(e^X - 1)` and scaled by `X/n!` equals `Xe^(tX)`.
|
Polynomial.bernoulli_succ_eval
theorem Polynomial.bernoulli_succ_eval :
∀ (n p : ℕ),
Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) =
bernoulli p.succ + (↑p + 1) * (Finset.range n).sum fun k => ↑k ^ p
The theorem `Polynomial.bernoulli_succ_eval` states that for any natural numbers `n` and `p`, the evaluation of the `p+1`-th Bernoulli polynomial at `n` is equal to the `p+1`-th Bernoulli number plus `(p+1)` times the sum of the `p`-th power of all the numbers in the range from `0` to `n-1`. The Bernoulli polynomials, Bernoulli numbers, and the range of numbers are defined according to the provided definitions in Lean 4.
More concisely: The `(p+1)`-th Bernoulli polynomial `Bernoulli (p+1) n` equals the `(p+1)`-th Bernoulli number `Bernoulli_num (p+1)` plus `(p+1)` times the sum of the `p`-th powers of numbers from `0` to `n-1`.
|