English
Under standard assumptions, a derivative of multilinear map is unique across equivalent derivative representations.
Русский
При стандартных условиях производная мультилинейного отображения уникальна между эквивалентными представлениями производной.
LaTeX
$$$f' = f_1'\;\text{ if } f'\text{ and } f_1'\text{ differentiate f on the same set.}$$$
Lean4
/-- Given `f` a linear map into multilinear maps, then the derivative
of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. Version inside a set. -/
theorem _root_.HasFDerivWithinAt.linear_multilinear_comp [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : ∀ i, H → G i}
{b' : ∀ i, H →L[𝕜] G i} {s : Set H} {x : H} (ha : HasFDerivWithinAt a a' s x)
(hb : ∀ i, HasFDerivWithinAt (b i) (b' i) s x) (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
HasFDerivWithinAt (fun y ↦ f (a y) (fun i ↦ b i y))
((f.flipMultilinear (fun i ↦ b i x)) ∘L a' + ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i)) s
x :=
(f.hasFDerivAt.comp_hasFDerivWithinAt x ha).continuousMultilinearMap_apply hb
