Documentation

Mathlib.Analysis.Calculus.FDeriv.Comp

The derivative of a composition (chain rule) #

For detailed documentation of the FrΓ©chet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of composition of functions (the chain rule).

Derivative of the composition of two functions #

For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to get confused since there are too many possibilities for composition.

source
theorem HasFDerivAtFilter.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {L : Filter E} {g : F β†’ G} {g' : F β†’L[π•œ] G} {L' : Filter F} (hg : HasFDerivAtFilter g g' (f x) L') (hf : HasFDerivAtFilter f f' x L) (hL : Filter.Tendsto f L L') :
HasFDerivAtFilter (g ∘ f) (g'.comp f') x L
source
theorem HasFDerivWithinAt.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {s : Set E} {g : F β†’ G} {g' : F β†’L[π•œ] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) :
HasFDerivWithinAt (g ∘ f) (g'.comp f') s x
source
theorem HasFDerivAt.comp_hasFDerivWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {s : Set E} {g : F β†’ G} {g' : F β†’L[π•œ] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (g ∘ f) (g'.comp f') s x
source
theorem HasFDerivWithinAt.comp_of_mem {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {s : Set E} {g : F β†’ G} {g' : F β†’L[π•œ] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)) :
HasFDerivWithinAt (g ∘ f) (g'.comp f') s x
source
theorem HasFDerivAt.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {g : F β†’ G} {g' : F β†’L[π•œ] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) :
HasFDerivAt (g ∘ f) (g'.comp f') x

The chain rule.

source
theorem DifferentiableWithinAt.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} {t : Set F} (hg : DifferentiableWithinAt π•œ g t (f x)) (hf : DifferentiableWithinAt π•œ f s x) (h : Set.MapsTo f s t) :
DifferentiableWithinAt π•œ (g ∘ f) s x
source
theorem DifferentiableWithinAt.comp' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} {t : Set F} (hg : DifferentiableWithinAt π•œ g t (f x)) (hf : DifferentiableWithinAt π•œ f s x) :
DifferentiableWithinAt π•œ (g ∘ f) (s ∩ f ⁻¹' t) x
source
theorem DifferentiableAt.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {g : F β†’ G} (hg : DifferentiableAt π•œ g (f x)) (hf : DifferentiableAt π•œ f x) :
DifferentiableAt π•œ (g ∘ f) x
source
theorem DifferentiableAt.comp_differentiableWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} (hg : DifferentiableAt π•œ g (f x)) (hf : DifferentiableWithinAt π•œ f s x) :
DifferentiableWithinAt π•œ (g ∘ f) s x
source
theorem fderivWithin.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} {t : Set F} (hg : DifferentiableWithinAt π•œ g t (f x)) (hf : DifferentiableWithinAt π•œ f s x) (h : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (g ∘ f) s x = (fderivWithin π•œ g t (f x)).comp (fderivWithin π•œ f s x)
source
theorem fderivWithin_fderivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {g : F β†’ G} {f : E β†’ F} {x : E} {y : F} {s : Set E} {t : Set F} (hg : DifferentiableWithinAt π•œ g t y) (hf : DifferentiableWithinAt π•œ f s x) (h : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt π•œ s x) (hy : f x = y) (v : E) :
(fderivWithin π•œ g t y) ((fderivWithin π•œ f s x) v) = (fderivWithin π•œ (g ∘ f) s x) v

A version of fderivWithin.comp that is useful to rewrite the composition of two derivatives into a single derivative. This version always applies, but creates a new side-goal f x = y.

source
theorem fderivWithin.comp₃ {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace π•œ G'] {f : E β†’ F} (x : E) {s : Set E} {g' : G β†’ G'} {g : F β†’ G} {t : Set F} {u : Set G} {y : F} {y' : G} (hg' : DifferentiableWithinAt π•œ g' u y') (hg : DifferentiableWithinAt π•œ g t y) (hf : DifferentiableWithinAt π•œ f s x) (h2g : Set.MapsTo g t u) (h2f : Set.MapsTo f s t) (h3g : g y = y') (h3f : f x = y) (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (g' ∘ g ∘ f) s x = (fderivWithin π•œ g' u y').comp ((fderivWithin π•œ g t y).comp (fderivWithin π•œ f s x))

Ternary version of fderivWithin.comp, with equality assumptions of basepoints added, in order to apply more easily as a rewrite from right-to-left.

source
theorem fderiv.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {g : F β†’ G} (hg : DifferentiableAt π•œ g (f x)) (hf : DifferentiableAt π•œ f x) :
fderiv π•œ (g ∘ f) x = (fderiv π•œ g (f x)).comp (fderiv π•œ f x)
source
theorem fderiv.comp_fderivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} (hg : DifferentiableAt π•œ g (f x)) (hf : DifferentiableWithinAt π•œ f s x) (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (g ∘ f) s x = (fderiv π•œ g (f x)).comp (fderivWithin π•œ f s x)
source
theorem DifferentiableOn.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {s : Set E} {g : F β†’ G} {t : Set F} (hg : DifferentiableOn π•œ g t) (hf : DifferentiableOn π•œ f s) (st : Set.MapsTo f s t) :
DifferentiableOn π•œ (g ∘ f) s
source
theorem Differentiable.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {g : F β†’ G} (hg : Differentiable π•œ g) (hf : Differentiable π•œ f) :
Differentiable π•œ (g ∘ f)
source
theorem Differentiable.comp_differentiableOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {s : Set E} {g : F β†’ G} (hg : Differentiable π•œ g) (hf : DifferentiableOn π•œ f s) :
DifferentiableOn π•œ (g ∘ f) s
source
theorem HasStrictFDerivAt.comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {g : F β†’ G} {g' : F β†’L[π•œ] G} (hg : HasStrictFDerivAt g g' (f x)) (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => g (f x)) (g'.comp f') x

The chain rule for derivatives in the sense of strict differentiability.

source
theorem Differentiable.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {f : E β†’ E} (hf : Differentiable π•œ f) (n : β„•) :
Differentiable π•œ f^[n]
source
theorem DifferentiableOn.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {f : E β†’ E} (hf : DifferentiableOn π•œ f s) (hs : Set.MapsTo f s s) (n : β„•) :
DifferentiableOn π•œ f^[n] s
source
theorem HasFDerivAtFilter.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {L : Filter E} {f : E β†’ E} {f' : E β†’L[π•œ] E} (hf : HasFDerivAtFilter f f' x L) (hL : Filter.Tendsto f L L) (hx : f x = x) (n : β„•) :
HasFDerivAtFilter f^[n] (f' ^ n) x L
source
theorem HasFDerivAt.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {f : E β†’ E} {f' : E β†’L[π•œ] E} (hf : HasFDerivAt f f' x) (hx : f x = x) (n : β„•) :
HasFDerivAt f^[n] (f' ^ n) x
source
theorem HasFDerivWithinAt.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {f : E β†’ E} {f' : E β†’L[π•œ] E} (hf : HasFDerivWithinAt f f' s x) (hx : f x = x) (hs : Set.MapsTo f s s) (n : β„•) :
HasFDerivWithinAt f^[n] (f' ^ n) s x
source
theorem HasStrictFDerivAt.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {f : E β†’ E} {f' : E β†’L[π•œ] E} (hf : HasStrictFDerivAt f f' x) (hx : f x = x) (n : β„•) :
HasStrictFDerivAt f^[n] (f' ^ n) x
source
theorem DifferentiableAt.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {f : E β†’ E} (hf : DifferentiableAt π•œ f x) (hx : f x = x) (n : β„•) :
DifferentiableAt π•œ f^[n] x
source
theorem DifferentiableWithinAt.iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {f : E β†’ E} (hf : DifferentiableWithinAt π•œ f s x) (hx : f x = x) (hs : Set.MapsTo f s s) (n : β„•) :
DifferentiableWithinAt π•œ f^[n] s x