Theorems · Theorem · special functions

ordinaryHypergeometricSeries_radius_eq_one

∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  (a b c : 𝕂), (∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) → (ordinaryHypergeometricSeries 𝔸 a b c).radius = 1

The radius of convergence of ordinaryHypergeometricSeries is unity if none of the parameters are non-positive integers.

Defined in

Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Cited by

1 results in Mathlib

Foundations

Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedDivisionRingNormedAlgebra