English
Let E and F be normed spaces over a field 𝕜. For any scalar c and any subset s of E, the Fréchet derivative within s of the map x ↦ f(c x) at x is the same as the derivative within c s of the map y ↦ c f(y) at y = c x. In particular, scaling the input scales the derivative accordingly.
Русский
Пусть E и F – нормированные пространства над полем 𝕜. Для любого скаляра c и подмножества s ⊆ E производная Фреше внутри s от отображения x ↦ f(c x) в точке x равна производной внутри c s от отображения y ↦ c f(y) в точке y = c x. В частности, масштабирование аргумента масштабирует производную соответствующим образом.
LaTeX
$$$$ \\mathrm{D}_s\\,(f \\circ (c \\cdot))(x) \\,=\\, c \\, \\mathrm{D}_{c s}\\,f\\,(c x). $$$$
Lean4
theorem fderivWithin_comp_smul_eq_fderivWithin_smul (c : 𝕜) :
fderivWithin 𝕜 (f <| c • ·) s x = fderivWithin 𝕜 (c • f) (c • s) (c • x) :=
by
rcases eq_or_ne c 0 with rfl | hc
· simp
· classical simp only [fderivWithin, DifferentiableWithinAt, hasFDerivWithinAt_comp_smul_iff_smul hc]
