English
If there is a geometric bound r providing summability of q.compAlongComposition p i for all i, then the radius of the composition satisfies (r) ≤ (q.comp p).radius.
Русский
Если существует геометрическое ограничение r, обеспечивающее суммируемость q.compAlongComposition p i для всех i, тогда радиус композиции удовлетворяет r ≤ (q.comp p).radius.
LaTeX
$$$ r \\le (q \\circ p).radius $ (in ℝ_{≥0}∞).$$
Lean4
/-- Bounding below the radius of the composition of two formal multilinear series assuming
summability over all compositions. -/
theorem le_comp_radius_of_summable (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0)
(hr : Summable fun i : Σ n, Composition n => ‖q.compAlongComposition p i.2‖₊ * r ^ i.1) :
(r : ℝ≥0∞) ≤ (q.comp p).radius :=
by
refine
le_radius_of_bound_nnreal _ (∑' i : Σ n, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst) fun n => ?_
calc
‖FormalMultilinearSeries.comp q p n‖₊ * r ^ n ≤ ∑' c : Composition n, ‖compAlongComposition q p c‖₊ * r ^ n :=
by
rw [tsum_fintype, ← Finset.sum_mul]
exact mul_le_mul' (nnnorm_sum_le _ _) le_rfl
_ ≤ ∑' i : Σ n : ℕ, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst :=
NNReal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective
