mathlib documentation


Representation of formal_multilinear_series.radius as a liminf #

In this file we prove that the radius of convergence of a formal_multilinear_series is equal to $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{ā€–p nā€–}}$. This lemma can't go to basic.lean because this would create a circular dependency once we redefine exp using formal_multilinear_series.

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.