Representation of FormalMultilinearSeries.radius as a liminf

In this file we prove that the radius of convergence of a FormalMultilinearSeries is equal to $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{‖p n‖}}$. 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 $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{‖p n‖}}$. The actual statement uses ℝ≥0 and some coercions.

theorem FormalMultilinearSeries.radius_inv_eq_limsup {𝕜 : 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.limsup (fun (n : ℕ) => ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop

The Cauchy-Hadamard theorem for formal multilinear series: The inverse of the radius is equal to $\limsup_{n\to\infty} \sqrt[n]{‖p n‖}$.