English
If f,g have strict Fréchet derivatives f',g' at x, then t ↦ ⟪f t, g t⟫ has derivative given by the same composition with f x, g x as above.
Русский
Если функции f,g имеют строгий производный Фрета в точке x, то t ↦ ⟪f t, g t⟫ имеет производную, заданную той же композицией с f x, g x.
LaTeX
$$$\\text{HasStrictFDerivAt}_{\\mathbb{R}}\\ (t \\mapsto \\langle f t, g t\\rangle) = \\bigl(fderivInnerCLM 𝕜 (f x, g x)\\bigr) \\circ \\bigl(f'\\times g'\\bigr).$$$
Lean4
theorem inner (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
HasStrictFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') x :=
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E) |>.hasStrictFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)
