Theorems · Definition · functional analysis

ContinuousMultilinearMap.iteratedFDerivComponent

{𝕜 : Type u} →
  {ι : Type v} →
    {E₁ : ι → Type wE₁} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [Fintype ι] →
                    {α : Type u_1} →
                      [Fintype α] →
                        ContinuousMultilinearMap 𝕜 E₁ G →
                          {s : Set ι} →
                            α ≃ ↑s →
                              [DecidablePred fun x => x ∈ s] →
                                ContinuousMultilinearMap 𝕜 (fun i => E₁ ↑i)
                                  (ContinuousMultilinearMap 𝕜 (fun x => (i : ι) → E₁ i) G)

One of the components of the iterated derivative of a continuous multilinear map. Given a bijection e between a type α (typically Fin k) and a subset s of ι, this component is a continuous multilinear map of k vectors v₁, ..., vₖ, mapping them to f (x₁, (v_{e.symm 2})₂, x₃, ...), where at indices i in s one uses the i-th coordinate of the vector v_{e.symm i} and otherwise one uses the i-th coordinate of a reference vector x. This is continuous multilinear in the components of x outside of s, and in the v_j.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceFintypeFintypeDecidablePred