English
The binomial series is equal to the ordinary hypergeometric series composed with a linear map; more precisely, binomialSeries equals (ordinaryHypergeometricSeries).compContinuousLinearMap (−id).
Русский
Биномиальный ряд равен обычному гипергипергеометрическому ряду, композиции с линейным отображением; то есть binomialSeries = (ordinaryHypergeometricSeries).compContinuousLinearMap (−id).
LaTeX
$$$ binomialSeries 𝔸 a = (ordinaryHypergeometricSeries 𝔸 (-a) b b).compContinuousLinearMap (- (id)) $$$
Lean4
theorem binomialSeries_eq_ordinaryHypergeometricSeries {𝕂 : Type u} [Field 𝕂] [CharZero 𝕂] {𝔸 : Type v} [Ring 𝔸]
[Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] {a b : 𝕂} (h : ∀ (k : ℕ), (k : 𝕂) ≠ -b) :
binomialSeries 𝔸 a = (ordinaryHypergeometricSeries 𝔸 (-a) b b).compContinuousLinearMap (-(.id _ _)) :=
by
simp only [binomialSeries, ordinaryHypergeometricSeries, FormalMultilinearSeries.ofScalars_comp_neg_id]
congr! with n
rw [ordinaryHypergeometricCoefficient, mul_inv_cancel_right₀ (by simp [ascPochhammer_eval_eq_zero_iff]; grind)]
simp only [Ring.choose_eq_smul, Polynomial.descPochhammer_smeval_eq_ascPochhammer,
Polynomial.ascPochhammer_smeval_cast, Polynomial.ascPochhammer_smeval_eq_eval,
ascPochhammer_eval_neg_eq_descPochhammer, descPochhammer_eval_eq_ascPochhammer]
ring_nf
simp
