Invariance of the derivative under translation

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

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

Translation in the domain does not change the derivative.

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

Translation in the domain does not change the derivative.

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

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

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

Translation in the domain does not change the derivative.

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

Translation in the domain does not change the derivative.