English
If f,g: G→E have within-set derivatives f',g' at s and x, then the derivative of t ↦ ⟪f t, g t⟫ at x is given by the composition with the derivative map of the inner bilinear form, i.e., ((fderivInnerCLM 𝕜 (f x, g x)) ∘ (f' × g')) at s and x.
Русский
Если функции f,g: G→E имеют внутри множества производные f', g' в точке x, то производная t ↦ ⟪f t, g t⟫ равна композиции с производной билинейной формы inner: ((fderivInnerCLM 𝕜 (f x, g x)) ∘ (f' × g')).
LaTeX
$$$(f,g) \\mapsto \\langle f,g\\rangle\\text{ имеет производную } ((fderivInnerCLM 𝕜 (f x, g x)) \\circ (f' \\cdot g'))$ на s в x.$$
Lean4
theorem inner (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') s x := by
-- `by exact` to handle a tricky unification.
exact
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E) |>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prodMk hg)
