mathlib3 documentation


Representation of formal_multilinear_series.radius as a liminf #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.