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

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

Equations

- p.sum x = ∑' (n : ℕ), (p n) fun (x_1 : Fin n) => x

Instances For

source
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}`.

Equations

- p.partialSum n x = ∑ k ∈ Finset.range n, (p k) fun (x_1 : Fin k) => x

Instances For

source
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 #

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

Equations

- p.radius = ⨆ (r : NNReal), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

Instances For

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

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

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

source
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
source
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
source
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
source
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 = ⊤
source
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 = ⊤
source
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 = ⊤
source
@[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 = ⊤
source
@[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

source
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ⁿ)`.

source
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)`.

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

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

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

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

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

source
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
source
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
source
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
source
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
source
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 ∈ EMetric.ball 0 p.radius) :
Summable fun (n : ℕ) => ‖(p n) fun (x_1 : Fin n) => x‖
source
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
source
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 ∈ EMetric.ball 0 p.radius) :
Summable fun (n : ℕ) => (p n) fun (x_1 : Fin n) => x
source
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 = ⊤
source
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
source
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.

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

source
@[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
source
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} {c : 𝕜} :
p.radius ≤ (c • p).radius
source
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) {c : 𝕜} (hc : c ≠ 0) :
(c • p).radius = p.radius
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
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.

source
@[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
source
@[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
source
@[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
source
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 ∈ EMetric.ball 0 p.radius) :
HasSum (fun (n : ℕ) => (p n) fun (x_1 : Fin n) => x) (p.sum x)
source
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