fderiv_of_bilinear — Mathlib

English

If f,g are differentiable at x with derivatives f', g', then the derivative at x of y ↦ B(f(y),g(y)) is the sum B.precompR(f x) g' + B.precompL f' (g x).

Русский

Если f,g дифференцируемы в x с производными f', g', то производная функции y ↦ B(f(y), g(y)) в x равна сумме, достигаемой через B.precompR и B.precompL.

LaTeX

$$$\text{fderiv}_{𝕜} (y \mapsto B(f(y),g(y))) (x) = B.precompR(G')(f x) \; g' + B.precompL G' f' (g x)$$$

Lean4

theorem fderiv_of_bilinear {f : G' → E} {g : G' → F} {x : G'} (hf : DifferentiableAt 𝕜 f x)
    (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => B (f y) (g y)) x = B.precompR G' (f x) (fderiv 𝕜 g x) + B.precompL G' (fderiv 𝕜 f x) (g x) :=
  (B.hasFDerivAt_of_bilinear hf.hasFDerivAt hg.hasFDerivAt).fderiv

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