deriv_inner_apply — Mathlib

English

Let f,g be differentiable with derivatives f', g'. Then the derivative of the map x ↦ ⟪f(x), g(x)⟫ at x in direction h is D⟨f,g⟩(x)[h] = ⟪f(x), f'(x)[h]⟫ + ⟪f'(x)[h], g(x)⟫.

Русский

Пусть f, g дифференцируемы с производными f', g'. Тогда производная по направлению h от отображения x ↦ ⟪f(x), g(x)⟫ равна ⟪f(x), f'(x)[h]⟫ + ⟪f'(x)[h], g(x)⟫.

LaTeX

$$$$D\langle f,g\rangle(x)[h] = \langle f(x), f'(x)[h]\rangle + \langle f'(x)[h], g(x)\rangle.$$$$

Lean4

theorem deriv_inner_apply {f g : ℝ → E} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun t => ⟪f t, g t⟫) x = ⟪f x, deriv g x⟫ + ⟪deriv f x, g x⟫ :=
  (hf.hasDerivAt.inner 𝕜 hg.hasDerivAt).deriv

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