binomialSeries_radius_eq_top_of_nat

English

The radius of convergence of binomialSeries 𝔸 a is top (i.e., infinite) when a is a natural number.

Русский

Радиус сходимости биномиального ряда 𝔸 a бесконечен, когда a натурально.

LaTeX

$$$ (binomialSeries 𝔸 (a : 𝕂)).radius = \top $$$

Lean4

/-- The radius of convergence of `binomialSeries 𝔸 a` is `⊤` for natural `a`. -/
theorem binomialSeries_radius_eq_top_of_nat {𝕂 : Type v} [RCLike 𝕂] {𝔸 : Type u} [NormedDivisionRing 𝔸]
    [NormedAlgebra 𝕂 𝔸] {a : ℕ} : (binomialSeries 𝔸 (a : 𝕂)).radius = ⊤ := by
  simp [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    ordinaryHypergeometric_radius_top_of_neg_nat₁]

Похожие утверждения