English
If a is not a natural number, the radius of binomialSeries is 1.
Русский
Если a не натуральное число, радиус биномиального ряда равен 1.
LaTeX
$$$ (binomialSeries 𝔸 a).radius = 1 $$$
Lean4
/-- The radius of convergence of `binomialSeries 𝔸 a` is `1`, when `a` is not natural. -/
theorem binomialSeries_radius_eq_one {𝕂 : Type v} [RCLike 𝕂] {𝔸 : Type u} [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸]
{a : 𝕂} (ha : ∀ (k : ℕ), a ≠ k) : (binomialSeries 𝔸 a).radius = 1 :=
by
simp only [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
FormalMultilinearSeries.radius_compNeg]
conv at ha => ext; rw [ne_comm]
exact ordinaryHypergeometricSeries_radius_eq_one _ _ _ _ (by norm_cast; grind)