Invariance of the derivative under translation

We show that if a function f has derivative f' at a point a + x, then f (a + ·) has derivative f' at x. Similarly for x + a.

theorem HasDerivAt.comp_const_add {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (a x : 𝕜) (hf : HasDerivAt f f' (a + x)) : HasDerivAt (fun (x : 𝕜) => f (a + x)) f' x

Translation in the domain does not change the derivative.

theorem HasDerivAt.comp_add_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (x a : 𝕜) (hf : HasDerivAt f f' (x + a)) : HasDerivAt (fun (x : 𝕜) => f (x + a)) f' x

Translation in the domain does not change the derivative.

theorem HasDerivAt.comp_const_sub {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (a x : 𝕜) (hf : HasDerivAt f f' (a - x)) : HasDerivAt (fun (x : 𝕜) => f (a - x)) (-f') x

Translation in the domain does not change the derivative.

theorem HasDerivAt.comp_sub_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (x a : 𝕜) (hf : HasDerivAt f f' (x - a)) : HasDerivAt (fun (x : 𝕜) => f (x - a)) f' x

Translation in the domain does not change the derivative.

theorem derivWithin_comp_neg {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (-x)) s x = -derivWithin f (-s) (-x)

theorem deriv_comp_neg {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (x : 𝕜) : deriv (fun (x : 𝕜) => f (-x)) x = -deriv f (-x)

The derivative of x ↦ f (-x) at a is the negative of the derivative of f at -a.

theorem derivWithin_comp_const_add {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (a + x)) s x = derivWithin f (a +ᵥ s) (a + x)

Translation in the domain does not change the derivative.

theorem deriv_comp_const_add {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜) : deriv (fun (x : 𝕜) => f (a + x)) x = deriv f (a + x)

Translation in the domain does not change the derivative.

theorem derivWithin_comp_add_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (x + a)) s x = derivWithin f (a +ᵥ s) (x + a)

Translation in the domain does not change the derivative.

theorem deriv_comp_add_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜) : deriv (fun (x : 𝕜) => f (x + a)) x = deriv f (x + a)

Translation in the domain does not change the derivative.

theorem derivWithin_comp_const_sub {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (a - x)) s x = -derivWithin f (a +ᵥ -s) (a - x)

theorem deriv_comp_const_sub {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜) : deriv (fun (x : 𝕜) => f (a - x)) x = -deriv f (a - x)

theorem derivWithin_comp_sub_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜) : derivWithin (fun (x : 𝕜) => f (x - a)) s x = derivWithin f (-a +ᵥ s) (x - a)

theorem deriv_comp_sub_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜) : deriv (fun (x : 𝕜) => f (x - a)) x = deriv f (x - a)