hasDerivWithinAt_comp_mul_left_smul_iff

English

Equivalence between having a derivative within s for x ↦ f(c x) with derivative c·f' and having a derivative within c·s for x at c x, scaled by c.

Русский

Эквивалентность: производная внутри s для x↦f(c x) равна c·f' тогда как внутри c·s для x при cx имеет производную f', масштабированная на c.

LaTeX

$$$$HasDerivWithinAt\ (f \left\lvert\; c * \cdot\right)\ (c \cdot f')\ s x \iff HasDerivWithinAt\ f f' (c \cdot s) (c \cdot x)$$$$

Lean4

theorem hasDerivWithinAt_comp_mul_left_smul_iff :
    HasDerivWithinAt (f <| c * ·) (c • f') s x ↔ HasDerivWithinAt f f' (c • s) (c * x) :=
  by
  simp only [hasDerivWithinAt_iff_hasFDerivWithinAt, ← smul_eq_mul, ← hasFDerivWithinAt_comp_smul_smul_iff]
  simp only [ContinuousLinearMap.one_smulRight_eq_toSpanSingleton, ContinuousLinearMap.toSpanSingleton_smul]

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