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 : 𝕜)
: