English
For a fixed multilinear map f and input pair (f, x), the derivative of the map (f, x) ↦ f(x) is given by a sum of two linear parts: differentiating f and differentiating x inside f.
Русский
Для фиксированного мультилинейного отображения f и пары (f, x) производная от отображения (f, x) ↦ f(x) равна сумме двух линейных частей: производная по f и производная по x внутри f.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( (f, x) \mapsto f(x) \bigr) = (\text{terms from }f'\text{ and }x' ).$$$
Lean4
protected theorem hasStrictFDerivAt_uncurry [DecidableEq ι] (fa : ContinuousMultilinearMap 𝕜 E F × ∀ i, E i) :
HasStrictFDerivAt (fun fx : ContinuousMultilinearMap 𝕜 E F × ∀ i, E i ↦ fx.1 fx.2)
(apply 𝕜 E F fa.2 ∘L .fst _ _ _ + fa.1.linearDeriv fa.2 ∘L .snd _ _ _) fa :=
by
let f := ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F) |>.continuousMultilinearMapOption
have Hf :=
(f.hasStrictFDerivAt (fun _ ↦ fa)).comp (f := fun fx _ ↦ fx) fa
(hasStrictFDerivAt_pi.2 fun _ ↦ hasStrictFDerivAt_id _)
convert Hf using 1
ext g
· suffices
∑ i, fa.1 (Function.update fa.2 i 0) =
∑ i, fa.1 fun j ↦ (Function.update (fun _ ↦ fa) (some i) (g, 0) (some j)).2 j
by simpa [f, ContinuousLinearMap.continuousMultilinearMapOption]
congr with i
congr with j
rcases eq_or_ne j i with rfl | hij <;> simp [*]
· suffices
∑ i, fa.1 (Function.update fa.2 i (g i)) =
∑ x, fa.1 fun i ↦ (Function.update (fun x ↦ fa) (some x) (0, g) (some i)).2 i
by simpa [f, ContinuousLinearMap.continuousMultilinearMapOption]
congr with i
congr with j
rcases eq_or_ne j i with rfl | hij <;> simp [*]
