English
Let f and g be differentiable maps from a domain G into an inner product space E. Then the function x ↦ ⟪f(x), g(x)⟫ is differentiable, and its derivative in direction h is given by D⟨f,g⟩(x)[h] = ⟪f(x), Dg(x)[h]⟫ + ⟪Df(x)[h], g(x)⟫.
Русский
Пусть f и g — дифференцируемые отображения из области G в пространство E с скалярным произведением. Тогда функция x ↦ ⟪f(x), g(x)⟫ дифференцируема, причём её дифференциал в направлении h задаётся формулой D⟨f,g⟩(x)[h] = ⟪f(x), Dg(x)[h]⟫ + ⟪Df(x)[h], g(x)⟫.
LaTeX
$$$$D\langle f,g\rangle(x)[h] = \langle f(x), Dg(x)[h]\rangle + \langle Df(x)[h], g(x)\rangle.$$$$
Lean4
theorem inner (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : Differentiable ℝ fun x => ⟪f x, g x⟫ := fun x =>
(hf x).inner 𝕜 (hg x)
