Documentation

Mathlib.Analysis.Calculus.Deriv.Shift

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.