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.
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.