ordinaryHypergeometric_radius_top_of_neg_nat₁

English

The radius of the hypergeometric series with a negated natural parameter equals infinity.

Русский

Радиус гипергеометрического ряда при отрицательном натуральном параметре бесконечен.

LaTeX

$$$\\text{radius}(\\ordinaryHypergeometricSeries( a, -k, b, c )) = \\top$$$

Lean4

theorem ordinaryHypergeometric_radius_top_of_neg_nat₁ {k : ℕ} :
    (ordinaryHypergeometricSeries 𝔸 (-(k : 𝕂)) b c).radius = ⊤ :=
  by
  refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_
  exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat (-(k : 𝕂)) b c (by aesop) (by cutsat)

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