English
Taking a scalar multiple preserves the radius; thus (c•p).radius = p.radius for c ≠ 0.
Русский
Копирование через скаляр сохраняет радиус; (c•p).radius = p.radius при c ≠ 0.
LaTeX
$$$\\text{If } c \\neq 0:\\quad (c\\cdot p).radius = p.radius.$$$
Lean4
/-- The right inverse of a formal multilinear series, where the `n`-th term is defined inductively
in terms of the previous ones to make sure that `p ∘ (rightInv p i) = id`. For this, the linear
term `p₁` in `p` should be invertible. In the definition, `i` is a linear isomorphism that should
coincide with `p₁`, so that one can use its inverse in the construction. The definition does not
use that `i = p₁`, but proofs that the definition is well-behaved do.
The `n`-th term in `p ∘ q` is `∑ pₖ (q_{j₁}, ..., q_{jₖ})` over `j₁ + ... + jₖ = n`. In this
expression, `qₙ` appears only once, in `p₁ (qₙ)`. We adjust the definition of `qₙ` so that this
term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`.
These formulas only make sense when the constant term `p₀` vanishes. The definition we give is
general, but it ignores the value of `p₀`.
-/
noncomputable def rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 F E
| 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ x
| 1 => (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm
| n + 2 =>
let q : FormalMultilinearSeries 𝕜 F E := fun k => if k < n + 2 then rightInv p i x k else 0;
-(i.symm : F →L[𝕜] E).compContinuousMultilinearMap ((p.comp q) (n + 2))
