The derivative of a composition (chain rule)

For detailed documentation of the Fréchet derivative, see the module docstring of Mathlib/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.

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} {L : Filter (E × E)} {g : F → G} {g' : F →L[𝕜] G} {L' : Filter (F × F)} (hg : HasFDerivAtFilter g g' L') (hf : HasFDerivAtFilter f f' L) (hL : Filter.Tendsto (Prod.map f f) L L') : HasFDerivAtFilter (g ∘ f) (g'.comp f') L

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.

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

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

theorem HasFDerivWithinAt.comp_of_tendsto {𝕜 : 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

theorem HasFDerivWithinAt.comp_hasFDerivAt {𝕜 : 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} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivAt f f' x) (ht : ∀ᶠ (x' : E) in nhds x, f x' ∈ t) : HasFDerivAt (g ∘ f) (g'.comp f') x

theorem HasFDerivWithinAt.comp_hasFDerivAt_of_eq {𝕜 : 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} {t : Set F} {y : F} (hg : HasFDerivWithinAt g g' t y) (hf : HasFDerivAt f f' x) (ht : ∀ᶠ (x' : E) in nhds x, f x' ∈ t) (hy : y = f x) : HasFDerivAt (g ∘ f) (g'.comp f') x

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.

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

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

theorem DifferentiableAt.fun_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] (x : E) {f : E → F} {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun (x : E) => g (f x)) x

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

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

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)

theorem fderivWithin_comp_of_eq {𝕜 : 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} {y : 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) : fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

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 𝕜 (fun (y : E) => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

A variant for the derivative of a composition, written without ∘.

theorem fderivWithin_comp_of_eq' {𝕜 : 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} {y : 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) : fderivWithin 𝕜 (fun (y : E) => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

A variant for the derivative of a composition, written without ∘.

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.

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.

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)

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 𝕜 (fun (y : E) => g (f y)) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x)

A variant for the derivative of a composition, written without ∘.

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)

theorem DifferentiableOn.fun_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 𝕜 (fun (x : E) => g (f x)) s

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

theorem Differentiable.fun_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 𝕜 fun (x : E) => g (f x)

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)

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

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]

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

theorem HasFDerivAtFilter.iterate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {L : Filter (E × E)} {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivAtFilter f f' L) (hL : Filter.Tendsto (Prod.map f f) L L) (n : ℕ) : HasFDerivAtFilter f^[n] (f' ^ n) L

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

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

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

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

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