Theorems · Definition · functional analysis

ContinuousAlternatingMap.fderivCompContinuousLinearMap

{𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {G : Type wG} →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] → [DecidableEq ι] → F [⋀^ι]→L[𝕜] G → (E →L[𝕜] F) → (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G

Fréchet derivative of compContinuousLinearMap f g with respect to g. Recall that compContinuousLinearMap f g is the pullback of f : F [⋀^ι]→L[𝕜] G along g : E →L[𝕜] F. This function is linear in f, so its derivative with respect to f is given by compContinuousLinearMapCLM f g. The derivative with respect to g is given by f.fderivCompContinuousLinearMap g dg v = ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j), see fderivCompContinuousLinearMap_apply below.

Defined in

Mathlib.Analysis.Normed.Module.Alternating.Basic

Cited by

13 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceFintypeDecidableEq