English
The radius of the sum is at least the minimum of radii: min(radius p, radius q) ≤ radius(p+q).
Русский
Радиус суммы не меньше минимума радиусов: min(radius p, radius q) ≤ radius(p+q).
LaTeX
$$$\\min(p.radius, q.radius) \\le (p+q).radius.$$$
Lean4
/-- The right inverse to a formal multilinear series is indeed a right inverse, provided its linear
term is invertible and its constant term vanishes. -/
theorem comp_rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
(h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) : p.comp (rightInv p i x) = id 𝕜 F (p 0 0) :=
by
ext (n v)
match n with
| 0 =>
simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]
congr
ext i
exact i.elim0
| 1 =>
simp only [comp_coeff_one, h, rightInv_coeff_one, ContinuousLinearEquiv.apply_symm_apply, id_apply_one,
ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply]
| n + 2 =>
have N : 0 < n + 2 := by simp
simp [comp_rightInv_aux1 N, h, rightInv, comp_rightInv_aux2, -Set.toFinset_setOf]
