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.

theorem formal_multilinear_series.radius_eq_liminf {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (p : formal_multilinear_series 𝕜 E F) :
p.radius = filter.at_top.liminf (λ (n : ), 1 / (nnnorm (p n) ^ (1 / n)))

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.