Theorems · Theorem · complex analysis

FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal

∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E] {r : ENNReal},
  Filter.Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) Filter.atTop (nhds r) →
    (FormalMultilinearSeries.ofScalars E c).radius = r⁻¹

This theorem combines the results of the special cases above, using ENNReal division to remove the requirement that the ratio is eventually non-zero.

Defined in

Mathlib.Analysis.Analytic.OfScalars

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraNormOneClass