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.