fderivWithin_continuousMultilinear_apply_const_apply

English

If c is differentiable at x with derivative c', then the map y ↦ c(y) ⋅ u is strictly differentiable for a fixed u, with derivative given by the action of c' on u.

Русский

Если c дифференцируема в x с производной c', тогда y ↦ c(y) ⋅ u строго дифференцируема по отношению к u.

LaTeX

$$$ HasStrictFDerivAt\left( y \mapsto (c(y)\cdot u) \right) x = c'.flip(u)$$$

Lean4

/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderivWithin`. -/
theorem fderivWithin_continuousMultilinear_apply_const_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) (m : E) :
    (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u := by
  simp [fderivWithin_continuousMultilinear_apply_const hxs hc]

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