English
Let A be a commutative ring equipped with a rational (ℚ) algebra structure, and let n be a natural number. Then the finite sum of powers of the exponential series satisfies the identity
∑_{k=0}^{n-1} (e^{X})^{k} = ∑_{p=0}^{∞} (∑_{k=0}^{n-1} k^{p} / p!) X^{p},
where the right-hand side is the formal power series with coefficients given by the sums ∑_{k=0}^{n-1} k^{p} divided by p!.
Русский
Пусть A — коммутативное кольцо, имеющее структуру ℚ-алгебры, и пусть n ∈ ℕ. Тогда верна тождь для формальных степенных рядов:
∑_{k=0}^{n-1} (e^{X})^{k} = ∑_{p=0}^{∞} (∑_{k=0}^{n-1} k^{p} / p!) X^{p},
где правая часть является формальным степенным рядом с коэффициентами ∑_{k=0}^{n-1} k^{p} / p!.
LaTeX
$$$\sum_{k=0}^{n-1} (e^{X})^{k} = \sum_{p=0}^{\infty} \left( \sum_{k=0}^{n-1} \frac{k^{p}}{p!} \right) X^{p}$$$
Lean4
/-- Shows that
$\sum_{k = 0}^{n - 1} (e^{X})^k = \sum_{p = 0}^{\infty} \sum_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$. -/
theorem exp_pow_sum [Algebra ℚ A] (n : ℕ) :
((Finset.range n).sum fun k => exp A ^ k) =
PowerSeries.mk fun p => (Finset.range n).sum fun k => (k ^ p : A) * algebraMap ℚ A p.factorial⁻¹ :=
by
simp only [exp_pow_eq_rescale_exp, rescale]
ext
simp only [one_div, coeff_mk, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, map_sum]
