fderiv_inner_apply — Mathlib

English

If f and g are differentiable at a point x, then the derivative at x of the map t ↦ ⟪f(t), g(t)⟫ in any direction h is D⟨f,g⟩(x)[h] = ⟪f(x), Dg(x)[h]⟫ + ⟪Df(x)[h], g(x)⟫.

Русский

Если f и g дифференцируемы в точке x, то производная по направлению h от отображения t ↦ ⟪f(t), g(t)⟫ равна ⟪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 fderiv_inner_apply (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : G) :
    fderiv ℝ (fun t => ⟪f t, g t⟫) x y = ⟪f x, fderiv ℝ g x y⟫ + ⟪fderiv ℝ f x y, g x⟫ := by
  rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]; rfl

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