deriv_of_bilinear — Mathlib

English

Compute the derivative of a bilinear composition with respect to a point, obtaining a linear combination of bilinear terms involving u, v, and their derivatives.

Русский

Вычисляем производную билинейной композиции относительно точки, получая линейную комбинацию билинейных членов, задействующих u, v и их производные.

LaTeX

$$$\text{For } f(y)=B(u(y),v(y)),\; \ deriv f x = B(u(x), deriv v x) + B(deriv u x, v(x)).$$$

Lean4

theorem deriv_of_bilinear (hu : DifferentiableAt 𝕜 u x) (hv : DifferentiableAt 𝕜 v x) :
    deriv (fun y => B (u y) (v y)) x = B (u x) (deriv v x) + B (deriv u x) (v x) :=
  (B.hasDerivAt_of_bilinear hu.hasDerivAt hv.hasDerivAt).deriv

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