English
Summability of the normed coefficients applied to x yields a convergent scalar series.
Русский
Суммируемость норм коэффициентов при применении к x дает сходящийся скалярный ряд.
LaTeX
$$$\\text{Summable } \\sum_n \\|p_n\\| (\\|x\\|)^n \\quad\\text{for } x\\text{ with } \\|x\\| < p.radius.$$$
Lean4
theorem leftInv_eq_rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
(h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) : leftInv p i x = rightInv p i x :=
calc
leftInv p i x = (leftInv p i x).comp (id 𝕜 F (p 0 0)) := by simp
_ = (leftInv p i x).comp (p.comp (rightInv p i x)) := by rw [comp_rightInv p i _ h]
_ = ((leftInv p i x).comp p).comp (rightInv p i x) := by rw [comp_assoc]
_ = (id 𝕜 E x).comp (rightInv p i x) := by rw [leftInv_comp p i _ h]
_ = rightInv p i x := by simp [id_comp' _ _ 0]
