English
Radius(p) = ∞ iff for all r≥0, the series ∑ ‖p_n‖ r^n is summable.
Русский
Radius(p) = ∞ тогда и только тогда, когда для всех r≥0 сумма ∑ ‖p_n‖ r^n суммируема.
LaTeX
$$$p.radius = \\infty \\iff \\forall r≥0,\\; Summable( n \\mapsto \\|p_n\\| r^n ).$$$
Lean4
theorem comp_rightInv_aux2 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (v : Fin (n + 2) → F) :
∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset,
p c.length (applyComposition (fun k : ℕ => ite (k < n + 2) (p.rightInv i x k) 0) c v) =
∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset, p c.length ((p.rightInv i x).applyComposition c v) :=
by
have N : 0 < n + 2 := by simp
refine sum_congr rfl fun c hc => p.congr rfl fun j hj1 hj2 => ?_
have : ∀ k, c.blocksFun k < n + 2 :=
by
simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}), Set.mem_setOf_eq] at hc
simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt hc]
simp [applyComposition, this]
