Derivative of x ↦ f (cx)

In this file we prove that the derivative of fun x ↦ f (c * x) equals c times the derivative of f evaluated at c * x.

Since Mathlib uses 0 as the fallback value for the derivatives whenever they are undefined, the theorems in this file require neither differentiability of f, nor assumptions like UniqueDiffWithinAt 𝕜 s x.

theorem hasDerivWithinAt_comp_mul_left_smul_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} {f : 𝕜 → E} {f' : E} {s : Set 𝕜} {x : 𝕜} : HasDerivWithinAt (fun (x : 𝕜) => f (c * x)) (c • f') s x ↔ HasDerivWithinAt f f' (c • s) (c * x)

theorem derivWithin_comp_mul_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (f : 𝕜 → E) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (c * x)) s x = c • derivWithin f (c • s) (c * x)

theorem deriv_comp_mul_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (f : 𝕜 → E) (x : 𝕜) : deriv (fun (x : 𝕜) => f (c * x)) x = c • deriv f (c * x)