Representation of FormalMultilinearSeries.radius as a liminf

In this file we prove that the radius of convergence of a FormalMultilinearSeries is equal to $\underset{n\to \mathrm{\infty }}{lim inf}\frac{1}{\sqrt[n]{\Vert pn\Vert }}$. This lemma can't go to Analysis.Analytic.Basic because this would create a circular dependency once we redefine exp using FormalMultilinearSeries.

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

The radius of a formal multilinear series is equal to $\underset{n\to \mathrm{\infty }}{lim inf}\frac{1}{\sqrt[n]{\Vert pn\Vert }}$. The actual statement uses ℝ≥0 and some coercions.