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
.
theorem
formal_multilinear_series.radius_eq_liminf
{š : Type u_1}
[nontrivially_normed_field š]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space š E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space š F]
(p : formal_multilinear_series š E F) :
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.