One-dimensional derivatives of compositions of functions

In this file we prove the chain rule for the following cases:

• HasDerivAt.comp etc: f : 𝕜' → 𝕜' composed with g : 𝕜 → 𝕜';
• HasDerivAt.scomp etc: f : 𝕜' → E composed with g : 𝕜 → 𝕜';
• HasFDerivAt.comp_hasDerivAt etc: f : E → F composed with g : 𝕜 → E;

Here 𝕜 is the base normed field, E and F are normed spaces over 𝕜 and 𝕜' is an algebra over 𝕜 (e.g., 𝕜'=𝕜 or 𝕜=ℝ, 𝕜'=ℂ).

We also give versions with the of_eq suffix, which require an equality proof instead of definitional equality of the different points used in the composition. These versions are often more flexible to use.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

Keywords

derivative, chain rule

Derivative of the composition of a vector function and a scalar function

We use scomp in lemmas on composition of vector valued and scalar valued functions, and comp in lemmas on composition of scalar valued functions, in analogy for smul and mul (and also because the comp version with the shorter name will show up much more often in applications). The formula for the derivative involves smul in scomp lemmas, which can be reduced to usual multiplication in comp lemmas.

theorem HasDerivAtFilter.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {L : Filter 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {L' : Filter 𝕜'} (hg : HasDerivAtFilter g₁ g₁' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Filter.Tendsto h L L') : HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

theorem HasDerivAtFilter.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {L : Filter 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {L' : Filter 𝕜'} {y : 𝕜'} (hg : HasDerivAtFilter g₁ g₁' y L') (hh : HasDerivAtFilter h h' x L) (hy : y = h x) (hL : Filter.Tendsto h L L') : HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

theorem HasDerivWithinAt.scomp_hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} (hg : HasDerivWithinAt g₁ g₁' s' (h x)) (hh : HasDerivAt h h' x) (hs : ∀ (x : 𝕜), h x ∈ s') : HasDerivAt (g₁ ∘ h) (h' • g₁') x

theorem HasDerivWithinAt.scomp_hasDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'} (hg : HasDerivWithinAt g₁ g₁' s' y) (hh : HasDerivAt h h' x) (hs : ∀ (x : 𝕜), h x ∈ s') (hy : y = h x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x

theorem HasDerivWithinAt.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} (hg : HasDerivWithinAt g₁ g₁' t' (h x)) (hh : HasDerivWithinAt h h' s x) (hst : Set.MapsTo h s t') : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

theorem HasDerivWithinAt.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'} (hg : HasDerivWithinAt g₁ g₁' t' y) (hh : HasDerivWithinAt h h' s x) (hst : Set.MapsTo h s t') (hy : y = h x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

theorem HasDerivAt.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} (hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x

The chain rule.

theorem HasDerivAt.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'} (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivAt h h' x) (hy : y = h x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x

The chain rule.

theorem HasStrictDerivAt.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} (hg : HasStrictDerivAt g₁ g₁' (h x)) (hh : HasStrictDerivAt h h' x) : HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

theorem HasStrictDerivAt.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'} (hg : HasStrictDerivAt g₁ g₁' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) : HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

theorem HasDerivAt.scomp_hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} (hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

theorem HasDerivAt.scomp_hasDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'} (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

theorem derivWithin.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F} (hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : Set.MapsTo h s t') (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

theorem derivWithin.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F} {y : 𝕜'} (hg : DifferentiableWithinAt 𝕜' g₁ t' y) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : Set.MapsTo h s t') (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : y = h x) : derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

theorem deriv.scomp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F} (hg : DifferentiableAt 𝕜' g₁ (h x)) (hh : DifferentiableAt 𝕜 h x) : deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

theorem deriv.scomp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F} {y : 𝕜'} (hg : DifferentiableAt 𝕜' g₁ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) : deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Derivative of the composition of a scalar and vector functions

theorem HasDerivAtFilter.comp_hasFDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {L' : Filter 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) {L'' : Filter E} (hh₂ : HasDerivAtFilter h₂ h₂' (f x) L') (hf : HasFDerivAtFilter f f' x L'') (hL : Filter.Tendsto f L'' L') : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

theorem HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {L' : Filter 𝕜'} {y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) {L'' : Filter E} (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hf : HasFDerivAtFilter f f' x L'') (hL : Filter.Tendsto f L'' L') (hy : y = f x) : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

theorem HasStrictDerivAt.comp_hasStrictFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) (hh : HasStrictDerivAt h₂ h₂' (f x)) (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

theorem HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) (hh : HasStrictDerivAt h₂ h₂' y) (hf : HasStrictFDerivAt f f' x) (hy : y = f x) : HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

theorem HasDerivAt.comp_hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivAt f f' x) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x

theorem HasDerivAt.comp_hasFDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E) (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivAt f f' x) (hy : y = f x) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x

theorem HasDerivAt.comp_hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} (x : E) (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

theorem HasDerivAt.comp_hasFDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} (x : E) (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivWithinAt f f' s x) (hy : y = f x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

theorem HasDerivWithinAt.comp_hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} {t : Set 𝕜'} (x : E) (hh : HasDerivWithinAt h₂ h₂' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

theorem HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} {t : Set 𝕜'} (x : E) (hh : HasDerivWithinAt h₂ h₂' t y) (hf : HasFDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) (hy : y = f x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Derivative of the composition of two scalar functions

theorem HasDerivAtFilter.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {L : Filter 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {L' : Filter 𝕜'} (hh₂ : HasDerivAtFilter h₂ h₂' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Filter.Tendsto h L L') : HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

theorem HasDerivAtFilter.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {L : Filter 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {L' : Filter 𝕜'} {y : 𝕜'} (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hh : HasDerivAtFilter h h' x L) (hL : Filter.Tendsto h L L') (hy : y = h x) : HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

theorem HasDerivWithinAt.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} (hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)) (hh : HasDerivWithinAt h h' s x) (hst : Set.MapsTo h s s') : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

theorem HasDerivWithinAt.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} (hh₂ : HasDerivWithinAt h₂ h₂' s' y) (hh : HasDerivWithinAt h h' s x) (hst : Set.MapsTo h s s') (hy : y = h x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

theorem HasDerivAt.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} (hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x

The chain rule.

Note that the function h₂ is a function on an algebra. If you are looking for the chain rule with h₂ taking values in a vector space, use HasDerivAt.scomp.

theorem HasDerivAt.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivAt h h' x) (hy : y = h x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x

The chain rule.

Note that the function h₂ is a function on an algebra. If you are looking for the chain rule with h₂ taking values in a vector space, use HasDerivAt.scomp_of_eq.

theorem HasStrictDerivAt.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} (hh₂ : HasStrictDerivAt h₂ h₂' (h x)) (hh : HasStrictDerivAt h h' x) : HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

theorem HasStrictDerivAt.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} (hh₂ : HasStrictDerivAt h₂ h₂' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) : HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

theorem HasDerivAt.comp_hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} (hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

theorem HasDerivAt.comp_hasDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' : 𝕜'} {h₂' : 𝕜'} {y : 𝕜'} (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

theorem derivWithin.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : Set.MapsTo h s s') (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

theorem derivWithin.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {y : 𝕜'} (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : Set.MapsTo h s s') (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : y = h x) : derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

theorem deriv.comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} (hh₂ : DifferentiableAt 𝕜' h₂ (h x)) (hh : DifferentiableAt 𝕜 h x) : deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

theorem deriv.comp_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {y : 𝕜'} (hh₂ : DifferentiableAt 𝕜' h₂ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) : deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

theorem HasDerivAtFilter.iterate {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {L : Filter 𝕜} {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAtFilter f f' x L) (hL : Filter.Tendsto f L L) (hx : f x = x) (n : ℕ) : HasDerivAtFilter f^[n] (f' ^ n) x L

theorem HasDerivAt.iterate {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) (hx : f x = x) (n : ℕ) : HasDerivAt f^[n] (f' ^ n) x

theorem HasDerivWithinAt.iterate {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivWithinAt f f' s x) (hx : f x = x) (hs : Set.MapsTo f s s) (n : ℕ) : HasDerivWithinAt f^[n] (f' ^ n) s x

theorem HasStrictDerivAt.iterate {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasStrictDerivAt f f' x) (hx : f x = x) (n : ℕ) : HasStrictDerivAt f^[n] (f' ^ n) x

Derivative of the composition of a function between vector spaces and a function on 𝕜

theorem HasFDerivWithinAt.comp_hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {t : Set F} (hl : HasFDerivWithinAt l l' t (f x)) (hf : HasDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) : HasDerivWithinAt (l ∘ f) (l' f') s x

The composition l ∘ f where l : F → E and f : 𝕜 → F, has a derivative within a set equal to the Fréchet derivative of l applied to the derivative of f.

theorem HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {y : F} {t : Set F} (hl : HasFDerivWithinAt l l' t y) (hf : HasDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) (hy : y = f x) : HasDerivWithinAt (l ∘ f) (l' f') s x

The composition l ∘ f where l : F → E and f : 𝕜 → F, has a derivative within a set equal to the Fréchet derivative of l applied to the derivative of f.

theorem HasFDerivAt.comp_hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} (hl : HasFDerivAt l l' (f x)) (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (l ∘ f) (l' f') s x

theorem HasFDerivAt.comp_hasDerivWithinAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {y : F} (hl : HasFDerivAt l l' y) (hf : HasDerivWithinAt f f' s x) (hy : y = f x) : HasDerivWithinAt (l ∘ f) (l' f') s x

theorem HasFDerivAt.comp_hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} (hl : HasFDerivAt l l' (f x)) (hf : HasDerivAt f f' x) : HasDerivAt (l ∘ f) (l' f') x

The composition l ∘ f where l : F → E and f : 𝕜 → F, has a derivative equal to the Fréchet derivative of l applied to the derivative of f.

theorem HasFDerivAt.comp_hasDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {y : F} (hl : HasFDerivAt l l' y) (hf : HasDerivAt f f' x) (hy : y = f x) : HasDerivAt (l ∘ f) (l' f') x

The composition l ∘ f where l : F → E and f : 𝕜 → F, has a derivative equal to the Fréchet derivative of l applied to the derivative of f.

theorem HasStrictFDerivAt.comp_hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} (hl : HasStrictFDerivAt l l' (f x)) (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (l ∘ f) (l' f') x

theorem HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {y : F} (hl : HasStrictFDerivAt l l' y) (hf : HasStrictDerivAt f f' x) (hy : y = f x) : HasStrictDerivAt (l ∘ f) (l' f') x

theorem fderivWithin.comp_derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) (hs : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

theorem fderivWithin.comp_derivWithin_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {y : F} {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t y) (hf : DifferentiableWithinAt 𝕜 f s x) (hs : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : y = f x) : derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

theorem fderiv.comp_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜) {l : F → E} (hl : DifferentiableAt 𝕜 l (f x)) (hf : DifferentiableAt 𝕜 f x) : deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

theorem fderiv.comp_deriv_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜) {l : F → E} {y : F} (hl : DifferentiableAt 𝕜 l y) (hf : DifferentiableAt 𝕜 f x) (hy : y = f x) : deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)