English
Let A be a commutative ring with a ℚ-algebra structure. Then for t ∈ A, the generating function of Bernoulli polynomials B_n(t) satisfies (sum_{n≥0} B_n(t) X^n / n!) (e^X − 1) = X e^{tX}.
Русский
Пусть A — коммутативное кольцо с структурой алгебры над ℚ. Тогда для t ∈ A генерирующая функция Бернулли Б_n(t) удовлетворяет равенству (sum_{n≥0} B_n(t) X^n / n!) (e^X − 1) = X e^{tX}.
LaTeX
$$$$ \left( \sum_{n=0}^{\infty} \frac{B_n(t)}{n!} X^n \right) (e^{X} - 1) = X e^{tX} $$$$
Lean4
/-- The theorem that $(e^X - 1) * ∑ Bₙ(t)* X^n/n! = Xe^{tX}$ -/
theorem bernoulli_generating_function (t : A) :
(mk fun n => aeval t ((1 / n ! : ℚ) • bernoulli n)) * (exp A - 1) = PowerSeries.X * rescale t (exp A) := by
-- check equality of power series by checking coefficients of X^n
ext n
cases n with
| zero => simp
| succ n =>
-- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
-- last term plus sum to n+1
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
sum_range_succ]
-- last term is zero so kill with `add_zero`
simp only [RingHom.map_sub, tsub_self, constantCoeff_one, constantCoeff_exp, coeff_zero_eq_constantCoeff, mul_zero,
sub_self, add_zero]
-- Let's multiply both sides by (n+1)! (OK because it's a unit)
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
-- do trivial rearrangements to make RHS (n+1)*t^n
rw [mul_left_comm, ← RingHom.map_mul]
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
rw [cast_mul, mul_assoc, mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
-- But this is the RHS of `Polynomial.sum_bernoulli`
rw [← sum_bernoulli, Finset.mul_sum, map_sum]
-- and now we have to prove a sum is a sum, but all the terms are equal.
apply Finset.sum_congr rfl
intro i hi
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi), one_div,
PowerSeries.coeff_one, coeff_exp, sub_zero, LinearMap.map_sub, Algebra.smul_def, mul_right_comm _ ((aeval t) _),
← mul_assoc, ← RingHom.map_mul, ← Polynomial.C_eq_algebraMap, Polynomial.aeval_mul, Polynomial.aeval_C]
-- finally cancel the Bernoulli polynomial and the algebra_map
field_simp
