English
The binomial series for a parameter a is the scalar formal multilinear series whose coefficients are given by Ring.choose a; its sum is the function x ↦ (1+x)^a on its radius of convergence.
Русский
Степенной биномиальный ряд для параметра a — это скалярный формальный многочленный ряд с коэффициентами Ring.choose a; его сумма задаёт функцию x ↦ (1+x)^a на радиусе сходимости.
LaTeX
$$$ binomialSeries 𝔸 a \text{ sums to } x \mapsto (1+x)^a \text{ on its radius of convergence} $$$
Lean4
/-- **Binomial series**: the (scalar) formal multilinear series with coefficients given
by `Ring.choose a`. The sum of this series is `fun x ↦ (1 + x) ^ a` within the radius
of convergence. -/
noncomputable def binomialSeries {𝕂 : Type u} [Field 𝕂] [CharZero 𝕂] (𝔸 : Type v) [Ring 𝔸] [Algebra 𝕂 𝔸]
[TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (a : 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸 :=
.ofScalars 𝔸 (Ring.choose a ·)
