Theorems · Definition · several complex variables

FormalMultilinearSeries.leftInv

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F → (E ≃L[𝕜] F) → E → FormalMultilinearSeries 𝕜 F E

The left inverse of a formal multilinear series, where the n-th term is defined inductively in terms of the previous ones to make sure that (leftInv p i) ∘ p = 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 q ∘ p is ∑ qₖ (p_{j₁}, ..., p_{jₖ}) over j₁ + ... + jₖ = n. In this expression, qₙ appears only once, in qₙ (p₁, ..., p₁). We adjust the definition 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₀.

Defined in

Mathlib.Analysis.Analytic.Inverse

Cited by

8 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace