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