ordinaryHypergeometric_radius_top_of_neg_nat₃

English

Let k be a natural number. Then the ordinary hypergeometric series with the third parameter negated by k has infinite radius of convergence.

Русский

Пусть k — натуральное число. Тогда радиус схождения обыкновенной гипергеометрической серии с третьим параметром, равным -(k), равен бесконечности.

LaTeX

$$$$ \operatorname{radius}\big(\mathrm{ordinaryHypergeometricSeries} \; \mathbb{A} \; a \; b \; (-k)\big) = \top $$$$

Lean4

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

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