fun_smul — Mathlib

English

If c has derivative c' at x and f has derivative f' at x, then y ↦ c(y)·f(y) has derivative c(x)·f' + c' smulRight (f x) at x.

Русский

Если c имеет производную c' в x и f имеет производную f' в x, то y ↦ c(y)·f(y) имеет производную c(x)·f' + c' smulRight (f(x)) в x.

LaTeX

$$$$ \\text{HasFDerivAt}(\\lambda y, c(y)·f(y), x) = c(x)·f' + c'.smulRight(f(x)). $$$$

Lean4

@[fun_prop]
theorem fun_smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
    HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x := by
  -- `by exact` to solve unification issues.
  exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf

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