Theorems · Theorem · global analysis

ContinuousMultilinearMap.hasStrictFDerivAt_uncurry

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)),
  HasStrictFDerivAt (fun fx => fx.1 fx.2)
    (ContinuousMultilinearMap.apply 𝕜 E F fa.2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa

Defined in

Mathlib.Analysis.Calculus.FDeriv.Analytic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceFintypeDecidableEq