# 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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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.

source
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.

source
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
source
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
source
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
source
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
source
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') :
derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
source
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') (hy : y = h x) :
derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
source
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)
source
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 #

source
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''
source
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''
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem HasDerivWithinAt.comp_hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {t : Set 𝕜'} (x : E) (hh : HasDerivWithinAt h₂ h₂' t (f x)) (hf : HasFDerivAt f f' x) (ht : ∀ᶠ (x' : E) in nhds x, f x' ∈ t) :
HasFDerivAt (h₂ ∘ f) (h₂' • f') x
source
theorem HasDerivWithinAt.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[𝕜] 𝕜'} {t : Set 𝕜'} (x : E) (hh : HasDerivWithinAt h₂ h₂' t y) (hf : HasFDerivAt f f' x) (ht : ∀ᶠ (x' : E) in nhds x, f x' ∈ t) (hy : y = f x) :
HasFDerivAt (h₂ ∘ f) (h₂' • f') x

### Derivative of the composition of two scalar functions #

source
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
source
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
source
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
source
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
source
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`.

source
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`.

source
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
source
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
source
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
source
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
source
theorem HasDerivWithinAt.comp_hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'} {t : Set 𝕜'} (hh₂ : HasDerivWithinAt h₂ h₂' t (h x)) (hh : HasDerivAt h h' x) (ht : ∀ᶠ (x' : 𝕜) in nhds x, h x' ∈ t) :
HasDerivAt (h₂ ∘ h) (h₂' * h') x
source
theorem HasDerivWithinAt.comp_hasDerivAt_of_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'} {t : Set 𝕜'} (hh₂ : HasDerivWithinAt h₂ h₂' t y) (hh : HasDerivAt h h' x) (ht : ∀ᶠ (x' : 𝕜) in nhds x, h x' ∈ t) (hy : y = h x) :
HasDerivAt (h₂ ∘ h) (h₂' * h') x
source
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') :
derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
source
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') (hy : h x = y) :
derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
source
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
source
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 : h x = y) :
deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
source
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
source
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
source
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
source
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 `𝕜` #

source
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`.

source
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`.

source
theorem HasFDerivWithinAt.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} {t : Set F} (hl : HasFDerivWithinAt l l' t (f x)) (hf : HasDerivAt f f' x) (ht : ∀ᶠ (x' : 𝕜) in nhds x, f x' ∈ t) :
HasDerivAt (l ∘ f) (l' f') x
source
theorem HasFDerivWithinAt.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} {t : Set F} (hl : HasFDerivWithinAt l l' t y) (hf : HasDerivAt f f' x) (ht : ∀ᶠ (x' : 𝕜) in nhds x, f x' ∈ t) (hy : y = f x) :
HasDerivAt (l ∘ f) (l' f') x
source
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
source
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
source
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`.

source
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`.

source
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
source
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
source
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) :
derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
source
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) (hy : y = f x) :
derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
source
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)
source
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)