English
Specializing to real-valued domain, if f,g: ℝ→E with derivatives f',g' at x, then ⟪f,g⟫ has derivative ⟪f x,g'⟫ + ⟪f',g x⟫.
Русский
Упрощено до вещественной линии: если f,g: ℝ→E с производными f',g' в x, то ⟪f,g⟫ имеет производную ⟪f x,g'⟫ + ⟪f',g x⟫.
LaTeX
$$$\\text{HasDerivWithinAt}_{\\mathbb{R}}\\ (f,g) \\Rightarrow \\text{HasDerivWithinAt}_{\\mathbb{R}}\\ (t \\mapsto \\langle f t, g t\\rangle)\\ (\\langle f x, g'\\rangle + \\langle f', g x\\rangle).$$$
Lean4
theorem inner {f g : ℝ → E} {f' g' : E} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x)
(hg : HasDerivWithinAt g g' s x) : HasDerivWithinAt (fun t => ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) s x := by
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt
