Radius of convergence of a power series

This file introduces the notion of the radius of convergence of a power series.

Main definitions

Let p be a formal multilinear series from E to F, i.e., p n is a multilinear map on E^n for n : ℕ.

• p.radius: the largest r : ℝ≥0∞ such that ‖p n‖ * r^n grows subexponentially.
• p.le_radius_of_bound, p.le_radius_of_bound_nnreal, p.le_radius_of_isBigO: if ‖p n‖ * r ^ n is bounded above, then r ≤ p.radius;
• p.isLittleO_of_lt_radius, p.norm_mul_pow_le_mul_pow_of_lt_radius, p.isLittleO_one_of_lt_radius, p.norm_mul_pow_le_of_lt_radius, p.nnnorm_mul_pow_le_of_lt_radius: if r < p.radius, then ‖p n‖ * r ^ n tends to zero exponentially;
• p.lt_radius_of_isBigO: if r ≠ 0 and ‖p n‖ * r ^ n = O(a ^ n) for some -1 < a < 1, then r < p.radius;
• p.partialSum n x: the sum ∑_{i = 0}^{n-1} pᵢ xⁱ.
• p.sum x: the sum ∑'_{i = 0}^{∞} pᵢ xⁱ.

Implementation details

We only introduce the radius of convergence of a power series, as p.radius. For a power series in finitely many dimensions, there is a finer (directional, coordinate-dependent) notion, describing the polydisk of convergence. This notion is more specific, and not necessary to build the general theory. We do not define it here.

def FormalMultilinearSeries.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) : F

Given a formal multilinear series p and a vector x, then p.sum x is the sum Σ pₙ xⁿ. A priori, it only behaves well when ‖x‖ < p.radius.

def FormalMultilinearSeries.partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (x : E) : F

Given a formal multilinear series p and a vector x, then p.partialSum n x is the sum Σ pₖ xᵏ for k ∈ {0,..., n-1}.

theorem FormalMultilinearSeries.partialSum_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : Continuous (p.partialSum n)

The partial sums of a formal multilinear series are continuous.

The radius of a formal multilinear series

def FormalMultilinearSeries.radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : ENNReal

The radius of a formal multilinear series is the largest r such that the sum Σ ‖pₙ‖ ‖y‖ⁿ converges for all ‖y‖ < r. This implies that Σ pₙ yⁿ converges for all ‖y‖ < r, but these definitions are not equivalent in general.

theorem FormalMultilinearSeries.le_radius_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (C : ℝ) {r : NNReal} (h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C) : ↑r ≤ p.radius

If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.

theorem FormalMultilinearSeries.le_radius_of_bound_nnreal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (C : NNReal) {r : NNReal} (h : ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C) : ↑r ≤ p.radius

If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.

theorem FormalMultilinearSeries.le_radius_of_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun (x : ℕ) => 1) : ↑r ≤ p.radius

If ‖pₙ‖ rⁿ = O(1), as n → ∞, then the radius of p is at least r.

theorem FormalMultilinearSeries.le_radius_of_eventually_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (C : ℝ) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ‖p n‖ * ↑r ^ n ≤ C) : ↑r ≤ p.radius

theorem FormalMultilinearSeries.le_radius_of_summable_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : Summable fun (n : ℕ) => ‖p n‖₊ * r ^ n) : ↑r ≤ p.radius

theorem FormalMultilinearSeries.le_radius_of_summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : Summable fun (n : ℕ) => ‖p n‖ * ↑r ^ n) : ↑r ≤ p.radius

theorem FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : ∀ (r : NNReal), (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun (x : ℕ) => 1) : p.radius = ⊤

theorem FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : ∀ᶠ (n : ℕ) in Filter.atTop, p n = 0) : p.radius = ⊤

theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (hn : ∀ (m : ℕ), p (m + n) = 0) : p.radius = ⊤

@[simp]

theorem FormalMultilinearSeries.constFormalMultilinearSeries_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {v : F} : (constFormalMultilinearSeries 𝕜 E v).radius = ⊤

@[simp]

theorem FormalMultilinearSeries.zero_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : radius 0 = ⊤

0 has infinite radius of convergence

theorem FormalMultilinearSeries.isLittleO_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : ∃ a ∈ Set.Ioo 0 1, (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun (x : ℕ) => a ^ x

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially: for some 0 < a < 1, ‖p n‖ rⁿ = o(aⁿ).

theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun (x : ℕ) => 1

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ = o(1).

theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially: for some 0 < a < 1 and C > 0, ‖p n‖ * r ^ n ≤ C * a ^ n.

theorem FormalMultilinearSeries.lt_radius_of_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h₀ : r ≠ 0) {a : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hp : (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun (x : ℕ) => a ^ x) : ↑r < p.radius

If r ≠ 0 and ‖pₙ‖ rⁿ = O(aⁿ) for some -1 < a < 1, then r < p.radius.

theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h0 : 0 < r) (h : ↑r < p.radius) : ∃ C > 0, ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

theorem FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : ∃ C > 0, ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C

For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

theorem FormalMultilinearSeries.le_radius_of_tendsto {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {r : NNReal} (p : FormalMultilinearSeries 𝕜 E F) {l : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => ‖p n‖ * ↑r ^ n) Filter.atTop (nhds l)) : ↑r ≤ p.radius

theorem FormalMultilinearSeries.le_radius_of_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {r : NNReal} (p : FormalMultilinearSeries 𝕜 E F) (hs : Summable fun (n : ℕ) => ‖p n‖ * ↑r ^ n) : ↑r ≤ p.radius

theorem FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (h : p.radius < ↑‖x‖₊) : ¬Summable fun (n : ℕ) => ‖p n‖ * ‖x‖ ^ n

theorem FormalMultilinearSeries.summable_norm_mul_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : Summable fun (n : ℕ) => ‖p n‖ * ↑r ^ n

theorem FormalMultilinearSeries.summable_norm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : Summable fun (n : ℕ) => ‖(p n) fun (x_1 : Fin n) => x‖

theorem FormalMultilinearSeries.summable_nnnorm_mul_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : ↑r < p.radius) : Summable fun (n : ℕ) => ‖p n‖₊ * r ^ n

theorem FormalMultilinearSeries.summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : Summable fun (n : ℕ) => (p n) fun (x_1 : Fin n) => x

theorem FormalMultilinearSeries.radius_eq_top_of_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (hs : ∀ (r : NNReal), Summable fun (n : ℕ) => ‖p n‖ * ↑r ^ n) : p.radius = ⊤

theorem FormalMultilinearSeries.radius_eq_top_iff_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : p.radius = ⊤ ↔ ∀ (r : NNReal), Summable fun (n : ℕ) => ‖p n‖ * ↑r ^ n

theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) : ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

If the radius of p is positive, then ‖pₙ‖ grows at most geometrically.

theorem FormalMultilinearSeries.radius_le_of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {𝕜' : Type u_5} {E' : Type u_6} {F' : Type u_7} [NontriviallyNormedField 𝕜'] [NormedAddCommGroup E'] [NormedSpace 𝕜' E'] [NormedAddCommGroup F'] [NormedSpace 𝕜' F'] {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜' E' F'} (h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖) : q.radius ≤ p.radius

theorem FormalMultilinearSeries.min_radius_le_radius_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p q : FormalMultilinearSeries 𝕜 E F) : min p.radius q.radius ≤ (p + q).radius

The radius of the sum of two formal series is at least the minimum of their two radii.

@[simp]

theorem FormalMultilinearSeries.radius_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : (-p).radius = p.radius

theorem FormalMultilinearSeries.radius_le_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {𝕜' : Type u_5} {c : 𝕜'} [NormedRing 𝕜'] [Module 𝕜' F] [SMulCommClass 𝕜 𝕜' F] [IsBoundedSMul 𝕜' F] : p.radius ≤ (c • p).radius

theorem FormalMultilinearSeries.radius_smul_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {𝕜' : Type u_5} {c : 𝕜'} [NormedDivisionRing 𝕜'] [Module 𝕜' F] [NormSMulClass 𝕜' F] [SMulCommClass 𝕜 𝕜' F] (hc : c ≠ 0) : (c • p).radius = p.radius

theorem FormalMultilinearSeries.norm_compContinuousLinearMap_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) : ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n

theorem FormalMultilinearSeries.enorm_compContinuousLinearMap_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) : ‖p.compContinuousLinearMap u n‖ₑ ≤ ‖p n‖ₑ * ‖u‖ₑ ^ n

theorem FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) : ‖p.compContinuousLinearMap u n‖₊ ≤ ‖p n‖₊ * ‖u‖₊ ^ n

theorem FormalMultilinearSeries.div_le_radius_compContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) : p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius

theorem FormalMultilinearSeries.le_radius_compContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →ₗᵢ[𝕜] F) : p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius

theorem FormalMultilinearSeries.radius_compContinuousLinearMap_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Nontrivial F] (p : FormalMultilinearSeries 𝕜 F G) (u : E ≃L[𝕜] F) : (p.compContinuousLinearMap ↑u).radius ≤ ‖↑u.symm‖ₑ * p.radius

@[simp]

theorem FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Nontrivial E] (p : FormalMultilinearSeries 𝕜 F G) (u : E ≃ₗᵢ[𝕜] F) : (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap).radius = p.radius

theorem FormalMultilinearSeries.radius_compContinuousLinearMap_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Nontrivial E] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (hu_iso : Isometry ⇑u) (hu_surj : Function.Surjective ⇑u) : (p.compContinuousLinearMap u).radius = p.radius

This is a version of radius_compContinuousLinearMap_linearIsometryEquiv_eq with better opportunity for unification, at the cost of manually supplying some hypotheses.

@[simp]

theorem FormalMultilinearSeries.radius_compNeg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial E] (p : FormalMultilinearSeries 𝕜 E F) : (p.compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E)).radius = p.radius

@[simp]

theorem FormalMultilinearSeries.radius_shift {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : p.shift.radius = p.radius

@[simp]

theorem FormalMultilinearSeries.radius_unshift {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : (p.unshift z).radius = p.radius

theorem FormalMultilinearSeries.hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : HasSum (fun (n : ℕ) => (p n) fun (x_1 : Fin n) => x) (p.sum x)

theorem FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F) (f : F →L[𝕜] G) : p.radius ≤ (f.compFormalMultilinearSeries p).radius