hasStrictDerivAt_of_bilinear — Mathlib

English

If u and v have derivatives at x, then the derivative at x of the map y ↦ B(u(y), v(y)) equals B(u(x), v'(x)) + B(u'(x), v(x)).

Русский

Если u и v имеют производные в точке x, то производная по x для функции y ↦ B(u(y), v(y)) равна B(u(x), v'(x)) + B(u'(x), v(x)).

LaTeX

$$$\text{If } u,v:\mathbb{R}\to E,\; B: E\times F \to G\text{ is bilinear, then } \\ \\ \frac{d}{dx} B(u(x), v(x)) = B(u(x), v'(x)) + B(u'(x), v(x)).$$$

Lean4

theorem hasStrictDerivAt_of_bilinear (hu : HasStrictDerivAt u u' x) (hv : HasStrictDerivAt v v' x) :
    HasStrictDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x := by
  simpa using (B.hasStrictFDerivAt_of_bilinear hu.hasStrictFDerivAt hv.hasStrictFDerivAt).hasStrictDerivAt

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