inner — Mathlib

English

Specializing to the real line, if f,g: ℝ→E have derivatives f',g' at x, then HasDerivAt (t ↦ ⟪f t, g t⟫) with derivative ⟪f x, g'⟫ + ⟪f', g x⟫.

Русский

Узкое частное на ℝ: если f,g: ℝ→E имеют производные f', g' в x, то ⟪f,g⟫ имеет производную ⟪f x, g'⟫ + ⟪f', g x⟫.

LaTeX

$$$\\text{HasDerivAt}_{\\mathbb{R}}\\ (t \\mapsto \\langle f t, g t\\rangle)\\ x = \\langle f x, g'\\rangle + \\langle f', g x\\rangle.$$$

Lean4

theorem inner {f g : ℝ → E} {f' g' : E} {x : ℝ} :
    HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun t => ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) x := by
  simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜

Похожие утверждения