English
If f,g have derivatives f',g' at x, then the map t ↦ ⟪f t, g t⟫ has derivative ((fderivInnerCLM 𝕜 (f x, g x)) ∘ (f' × g')) at x.
Русский
Если f,g имеют производные f', g' в точке x, то t ↦ ⟪f t, g t⟫ имеет производную, заданную совпадающей композицией.
LaTeX
$$$\\text{HasFDerivAt}_{\\mathbb{R}}\\ (t \\mapsto \\langle f t, g t\\rangle) = ((fderivInnerCLM 𝕜 (f x, g x)) \\circ (f' \\times g')).$$$
Lean4
theorem inner (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') x := by
-- `by exact` to handle a tricky unification.
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E) |>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)
