hasFDerivAt_uncurry_of_multilinear

English

If two derivatives of a function in a multilinear context coincide on the tangent cone, then the derivatives are equal as linear maps.

Русский

Если две производные функции в мультилинейном контексте совпадают на касательной, то они равны как линейные отображения.

LaTeX

$$$\text{eq}(H_f, H_g)\;\text{on tangent cone} \Rightarrow H_f = H_g$$$

Lean4

theorem hasFDerivAt_uncurry_of_multilinear [DecidableEq ι] (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F)
    (v : E × Π i, G i) :
    HasFDerivAt (fun (p : E × Π i, G i) ↦ f p.1 p.2)
      ((f.flipMultilinear v.2) ∘L (.fst _ _ _) +
        ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i) ∘L (.proj _) ∘L (.snd _ _ _))
      v :=
  (f ∘L .fst 𝕜 E (∀ i, G i)).hasFDerivAt.continuousMultilinearMap_apply
    (hasFDerivAt_pi'.mp (hasFDerivAt_snd (E := E) (F := ∀ i, G i)))

Похожие утверждения