FormalMultilinearSeries.radius_eq_liminf

theorem FormalMultilinearSeries.radius_eq_liminf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F), p.radius = Filter.liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop

The theorem `FormalMultilinearSeries.radius_eq_liminf` states that for a formal multilinear series `p` over a non-trivially normed field `𝕜` and normed additively commutative groups `E` and `F` which are also normed spaces over `𝕜`, the radius of the series is equal to the limit inferior, as `n` goes to positive infinity, of the reciprocal of the n-th root of the norm of the n-th term of the series. The limit inferior, in this context, means the greatest lower bound (or infimum) of the set of limits of all subsequences of the sequence. The actual statement uses non-negative real numbers and some coercions.

More concisely: The radius of a formal multilinear series over a non-trivially normed field is equal to the lim inf of the reciprocal of the n-th term's norm raised to the power of 1/n, as n goes to infinity.