binomialSeries_radius_eq_one — Mathlib

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)

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