Mathlib.Analysis.Calculus.Deriv.Comp

HasDerivAtFilter.scomp theorem

 (hg : HasDerivAtFilter g₁ g₁' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
  HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Full source

theorem HasDerivAtFilter.scomp (hg : HasDerivAtFilter g₁ g₁' (h x) L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
    HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L := by
  simpa using ((hg.restrictScalars 𝕜).comp x hh hL).hasDerivAtFilter

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions Along Filters

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g₁ : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g₁$ has derivative $g₁'$ at $h(x)$ along filter $L'$, 2. $h$ has derivative $h'$ at $x$ along filter $L$, 3. The function $h$ tends to $L'$ along $L$ (i.e., $\lim_{L} h \in L'$), then the composition $g₁ \circ h$ has derivative $h' \cdot g₁'$ at $x$ along $L$.

HasDerivAtFilter.scomp_of_eq theorem

 (hg : HasDerivAtFilter g₁ g₁' y L') (hh : HasDerivAtFilter h h' x L) (hy : y = h x) (hL : Tendsto h L L') :
  HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Full source

theorem HasDerivAtFilter.scomp_of_eq (hg : HasDerivAtFilter g₁ g₁' y L')
    (hh : HasDerivAtFilter h h' x L) (hy : y = h x) (hL : Tendsto h L L') :
    HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L := by
  rw [hy] at hg; exact hg.scomp x hh hL

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions Along Filters with Explicit Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g₁ : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g₁$ has derivative $g₁'$ at $y$ along filter $L'$, 2. $h$ has derivative $h'$ at $x$ along filter $L$, 3. $y = h(x)$, 4. The function $h$ tends to $L'$ along $L$ (i.e., $\lim_{L} h \in L'$), then the composition $g₁ \circ h$ has derivative $h' \cdot g₁'$ at $x$ along $L$.

HasDerivWithinAt.scomp_hasDerivAt theorem

 (hg : HasDerivWithinAt g₁ g₁' s' (h x)) (hh : HasDerivAt h h' x) (hs : ∀ x, h x ∈ s') :
  HasDerivAt (g₁ ∘ h) (h' • g₁') x

Full source

theorem HasDerivWithinAt.scomp_hasDerivAt (hg : HasDerivWithinAt g₁ g₁' s' (h x))
    (hh : HasDerivAt h h' x) (hs : ∀ x, h x ∈ s') : HasDerivAt (g₁ ∘ h) (h' • g₁') x :=
  hg.scomp x hh <| tendsto_inf.2 ⟨hh.continuousAt, tendsto_principal.2 <| Eventually.of_forall hs⟩

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions with Domain Restriction

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $h(x)$ within the set $s' \subseteq \mathbb{K}'$, 2. $h$ has derivative $h'$ at $x$, 3. For all $x$, $h(x) \in s'$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$.

HasDerivWithinAt.scomp_hasDerivAt_of_eq theorem

 (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

Full source

theorem HasDerivWithinAt.scomp_hasDerivAt_of_eq (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 := by
  rw [hy] at hg; exact hg.scomp_hasDerivAt x hh hs

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions with Explicit Equality Condition

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $y$ within the set $s' \subseteq \mathbb{K}'$, 2. $h$ has derivative $h'$ at $x$, 3. For all $x$, $h(x) \in s'$, 4. $y = h(x)$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$.

HasDerivWithinAt.scomp theorem

 (hg : HasDerivWithinAt g₁ g₁' t' (h x)) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t') :
  HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Full source

nonrec theorem HasDerivWithinAt.scomp (hg : HasDerivWithinAt g₁ g₁' t' (h x))
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t') :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x :=
  hg.scomp x hh <| hh.continuousWithinAt.tendsto_nhdsWithin hst

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions Within Sets

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $h(x)$ within the set $t' \subseteq \mathbb{K}'$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $t'$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$ within $s$.

HasDerivWithinAt.scomp_of_eq theorem

 (hg : HasDerivWithinAt g₁ g₁' t' y) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t') (hy : y = h x) :
  HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Full source

theorem HasDerivWithinAt.scomp_of_eq (hg : HasDerivWithinAt g₁ g₁' t' y)
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t') (hy : y = h x) :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x := by
  rw [hy] at hg; exact hg.scomp x hh hst

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions Within Sets with Point Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $y$ within the set $t' \subseteq \mathbb{K}'$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $t'$, 4. $y = h(x)$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$ within $s$.

HasDerivAt.scomp theorem

(hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x

Full source

/-- The chain rule. -/
nonrec theorem HasDerivAt.scomp (hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivAt h h' x) :
    HasDerivAt (g₁ ∘ h) (h' • g₁') x :=
  hg.scomp x hh hh.continuousAt

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $g_1$ has derivative $g_1'$ at $h(x)$, and 2. $h$ has derivative $h'$ at $x$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$.

HasDerivAt.scomp_of_eq theorem

(hg : HasDerivAt g₁ g₁' y) (hh : HasDerivAt h h' x) (hy : y = h x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x

Full source

/-- The chain rule. -/
theorem HasDerivAt.scomp_of_eq
    (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
    HasDerivAt (g₁ ∘ h) (h' • g₁') x := by
  rw [hy] at hg; exact hg.scomp x hh

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $g_1$ has derivative $g_1'$ at $y$, and 2. $h$ has derivative $h'$ at $x$, with $y = h(x)$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$.

HasStrictDerivAt.scomp theorem

 (hg : HasStrictDerivAt g₁ g₁' (h x)) (hh : HasStrictDerivAt h h' x) : HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Full source

theorem HasStrictDerivAt.scomp (hg : HasStrictDerivAt g₁ g₁' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x := by
  simpa using ((hg.restrictScalars 𝕜).comp x hh).hasStrictDerivAt

Chain Rule for Strict Derivatives of Vector-Scalar Function Composition

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if $g_1$ has strict derivative $g_1'$ at $h(x)$ and $h$ has strict derivative $h'$ at $x$, then the composition $g_1 \circ h$ has strict derivative $h' \cdot g_1'$ at $x$.

HasStrictDerivAt.scomp_of_eq theorem

 (hg : HasStrictDerivAt g₁ g₁' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) : HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Full source

theorem HasStrictDerivAt.scomp_of_eq
    (hg : HasStrictDerivAt g₁ g₁' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
    HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x := by
  rw [hy] at hg; exact hg.scomp x hh

Chain Rule for Strict Derivatives of Vector-Scalar Function Composition with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if $g_1$ has strict derivative $g_1'$ at $y$ and $h$ has strict derivative $h'$ at $x$, with $y = h(x)$, then the composition $g_1 \circ h$ has strict derivative $h' \cdot g_1'$ at $x$.

HasDerivAt.scomp_hasDerivWithinAt theorem

(hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Full source

theorem HasDerivAt.scomp_hasDerivWithinAt (hg : HasDerivAt g₁ g₁' (h x))
    (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x :=
  HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh (mapsTo_univ _ _)

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions with Restricted Differentiability

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $h(x)$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$ within $s$.

HasDerivAt.scomp_hasDerivWithinAt_of_eq theorem

 (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Full source

theorem HasDerivAt.scomp_hasDerivWithinAt_of_eq (hg : HasDerivAt g₁ g₁' y)
    (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x := by
  rw [hy] at hg; exact hg.scomp_hasDerivWithinAt x hh

Chain Rule for Composition with Point Equality: $\text{derivWithin}\, (g_1 \circ h)\, s\, x = h' \cdot g_1'$ when $y = h(x)$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ has derivative $g_1'$ at $y$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $y = h(x)$, then the composition $g_1 \circ h$ has derivative $h' \cdot g_1'$ at $x$ within $s$.

derivWithin.scomp theorem

 (hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t') :
  derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Full source

theorem derivWithin.scomp (hg : DifferentiableWithinAt 𝕜' g₁ t' (h x))
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t') :
    derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x) := by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh.hasDerivWithinAt hs).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Chain Rule for Differentiable Composition Within Sets: $\text{derivWithin}\, (g \circ h)\, s\, x = (\text{derivWithin}\, h\, s\, x) \cdot (\text{derivWithin}\, g\, t'\, (h x))$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Consider functions $g_1 : \mathbb{K}' \to E$ (where $E$ is a normed space over $\mathbb{K}$) and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $g_1$ is differentiable at $h(x)$ within $t' \subseteq \mathbb{K}'$, 2. $h$ is differentiable at $x$ within $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $t'$, then the derivative of the composition $g_1 \circ h$ at $x$ within $s$ is given by: \[ \text{derivWithin}\, (g_1 \circ h)\, s\, x = (\text{derivWithin}\, h\, s\, x) \cdot (\text{derivWithin}\, g_1\, t'\, (h x)) \]

derivWithin.scomp_of_eq theorem

 (hg : DifferentiableWithinAt 𝕜' g₁ t' y) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t') (hy : y = h x) :
  derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Full source

theorem derivWithin.scomp_of_eq (hg : DifferentiableWithinAt 𝕜' g₁ t' y)
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t')
    (hy : y = h x) :
    derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x) := by
  rw [hy] at hg; exact derivWithin.scomp x hg hh hs

Chain Rule for Differentiable Composition Within Sets with Equality Condition

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, suppose: 1. $g_1$ is differentiable at $y$ within $t' \subseteq \mathbb{K}'$, 2. $h$ is differentiable at $x$ within $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $t'$, 4. $y = h(x)$. Then the derivative of the composition $g_1 \circ h$ at $x$ within $s$ is given by: \[ \text{derivWithin}\, (g_1 \circ h)\, s\, x = (\text{derivWithin}\, h\, s\, x) \cdot (\text{derivWithin}\, g_1\, t'\, y). \]

deriv.scomp theorem

 (hg : DifferentiableAt 𝕜' g₁ (h x)) (hh : DifferentiableAt 𝕜 h x) : deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Full source

theorem deriv.scomp (hg : DifferentiableAt 𝕜' g₁ (h x)) (hh : DifferentiableAt 𝕜 h x) :
    deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x) :=
  (HasDerivAt.scomp x hg.hasDerivAt hh.hasDerivAt).deriv

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $g_1$ is differentiable at $h(x)$, and 2. $h$ is differentiable at $x$, then the derivative of the composition $g_1 \circ h$ at $x$ is given by: $$ \text{deriv}(g_1 \circ h)(x) = \text{deriv} h(x) \cdot \text{deriv} g_1(h(x)) $$

deriv.scomp_of_eq theorem

 (hg : DifferentiableAt 𝕜' g₁ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) :
  deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Full source

theorem deriv.scomp_of_eq
    (hg : DifferentiableAt 𝕜' g₁ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) :
    deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x) := by
  rw [hy] at hg; exact deriv.scomp x hg hh

Chain Rule for Composition of Vector-Valued and Scalar-Valued Functions with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{K}'$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$. Given functions $g_1 : \mathbb{K}' \to E$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $g_1$ is differentiable at $y \in \mathbb{K}'$, 2. $h$ is differentiable at $x \in \mathbb{K}$, and 3. $y = h(x)$, then the derivative of the composition $g_1 \circ h$ at $x$ is given by: $$ \text{deriv}(g_1 \circ h)(x) = \text{deriv} h(x) \cdot \text{deriv} g_1(h(x)) $$

HasDerivAtFilter.comp_hasFDerivAtFilter theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E} (hh₂ : HasDerivAtFilter h₂ h₂' (f x) L')
  (hf : HasFDerivAtFilter f f' x L'') (hL : Tendsto f L'' L') : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Full source

theorem HasDerivAtFilter.comp_hasFDerivAtFilter {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
    (hh₂ : HasDerivAtFilter h₂ h₂' (f x) L') (hf : HasFDerivAtFilter f f' x L'')
    (hL : Tendsto f L'' L') : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L'' := by
  convert (hh₂.restrictScalars 𝕜).comp x hf hL
  ext x
  simp [mul_comm]

Chain Rule for Composition of Scalar and Vector Functions Along Filters

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. Suppose that at a point $x \in E$, the function $f$ has a Fréchet derivative $f' : E \to \mathbb{K}'$ along a filter $L''$ on $E$, and $h_2$ has a derivative $h_2' \in \mathbb{K}'$ at $f(x)$ along a filter $L'$ on $\mathbb{K}'$. If $f$ tends to $f(x)$ along $L''$ with respect to $L'$, then the composition $h_2 \circ f$ has a Fréchet derivative at $x$ along $L''$ given by the scalar multiplication $h_2' \cdot f'$.

HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E} (hh₂ : HasDerivAtFilter h₂ h₂' y L')
  (hf : HasFDerivAtFilter f f' x L'') (hL : Tendsto f L'' L') (hy : y = f x) :
  HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Full source

theorem HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq
    {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
    (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hf : HasFDerivAtFilter f f' x L'')
    (hL : Tendsto f L'' L') (hy : y = f x) : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L'' := by
  rw [hy] at hh₂; exact hh₂.comp_hasFDerivAtFilter x hf hL

Chain Rule for Composition of Scalar and Vector Functions Along Filters with Point Equality

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. Suppose that at a point $x \in E$, the function $f$ has a Fréchet derivative $f' : E \to \mathbb{K}'$ along a filter $L''$ on $E$, and $h_2$ has a derivative $h_2' \in \mathbb{K}'$ at a point $y$ along a filter $L'$ on $\mathbb{K}'$. If $f$ tends to $y$ along $L''$ with respect to $L'$ and $y = f(x)$, then the composition $h_2 \circ f$ has a Fréchet derivative at $x$ along $L''$ given by the scalar multiplication $h_2' \cdot f'$.

HasStrictDerivAt.comp_hasStrictFDerivAt theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasStrictDerivAt h₂ h₂' (f x)) (hf : HasStrictFDerivAt f f' x) :
  HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Full source

theorem HasStrictDerivAt.comp_hasStrictFDerivAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasStrictDerivAt h₂ h₂' (f x)) (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x := by
  rw [HasStrictDerivAt] at hh
  convert (hh.restrictScalars 𝕜).comp x hf
  ext x
  simp [mul_comm]

Strict Chain Rule for Composition of Scalar and Vector Functions

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Let $f : E \to \mathbb{K}'$ be a function with strict Fréchet derivative $f' : E \to L(E, \mathbb{K}')$ at a point $x \in E$, and let $h_2 : \mathbb{K}' \to \mathbb{K}'$ be a function with strict derivative $h_2' \in \mathbb{K}'$ at $f(x)$. Then the composition $h_2 \circ f : E \to \mathbb{K}'$ has strict Fréchet derivative $h_2' \cdot f'$ at $x$.

HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasStrictDerivAt h₂ h₂' y) (hf : HasStrictFDerivAt f f' x) (hy : y = f x) :
  HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Full source

theorem HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasStrictDerivAt h₂ h₂' y) (hf : HasStrictFDerivAt f f' x) (hy : y = f x) :
    HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x := by
  rw [hy] at hh; exact hh.comp_hasStrictFDerivAt x hf

Strict Chain Rule for Composition of Scalar and Vector Functions with Point Equality

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Let $f : E \to \mathbb{K}'$ be a function with strict Fréchet derivative $f' : E \to L(E, \mathbb{K}')$ at a point $x \in E$, and let $h_2 : \mathbb{K}' \to \mathbb{K}'$ be a function with strict derivative $h_2' \in \mathbb{K}'$ at $y \in \mathbb{K}'$. If $y = f(x)$, then the composition $h_2 \circ f : E \to \mathbb{K}'$ has strict Fréchet derivative $h_2' \cdot f'$ at $x$.

HasDerivAt.comp_hasFDerivAt theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivAt f f' x) :
  HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Full source

theorem HasDerivAt.comp_hasFDerivAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivAt f f' x) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x :=
  hh.comp_hasFDerivAtFilter x hf hf.continuousAt

Chain Rule for Composition of Scalar and Vector Functions

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Suppose $f : E \to \mathbb{K}'$ has a Fréchet derivative $f' : E \to \mathbb{K}'$ at a point $x \in E$, and $h_2 : \mathbb{K}' \to \mathbb{K}'$ has a derivative $h_2' \in \mathbb{K}'$ at $f(x)$. Then the composition $h_2 \circ f : E \to \mathbb{K}'$ has a Fréchet derivative at $x$ given by $h_2' \cdot f'$.

HasDerivAt.comp_hasFDerivAt_of_eq theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivAt f f' x) (hy : y = f x) :
  HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Full source

theorem HasDerivAt.comp_hasFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivAt f f' x) (hy : y = f x) :
    HasFDerivAt (h₂ ∘ f) (h₂' • f') x := by
  rw [hy] at hh; exact hh.comp_hasFDerivAt x hf

Chain Rule for Composition of Scalar and Vector Functions with Point Equality

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. If $h_2$ has derivative $h_2' \in \mathbb{K}'$ at a point $y \in \mathbb{K}'$, and $f$ has Fréchet derivative $f' : E \to \mathbb{K}'$ at a point $x \in E$, with $y = f(x)$, then the composition $h_2 \circ f$ has Fréchet derivative $h_2' \cdot f'$ at $x$.

HasDerivAt.comp_hasFDerivWithinAt theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x) (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivWithinAt f f' s x) :
  HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Full source

theorem HasDerivAt.comp_hasFDerivWithinAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x)
    (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x :=
  hh.comp_hasFDerivAtFilter x hf hf.continuousWithinAt

Chain Rule for Composition of Scalar and Vector Functions Within a Set

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. If $h_2$ has derivative $h_2' \in \mathbb{K}'$ at $f(x)$, and $f$ has Fréchet derivative $f' : E \to \mathbb{K}'$ at $x$ within a set $s \subseteq E$, then the composition $h_2 \circ f$ has Fréchet derivative $h_2' \cdot f'$ at $x$ within $s$.

HasDerivAt.comp_hasFDerivWithinAt_of_eq theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x) (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivWithinAt f f' s x) (hy : y = f x) :
  HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Full source

theorem HasDerivAt.comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x)
    (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivWithinAt f f' s x) (hy : y = f x) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x := by
  rw [hy] at hh; exact hh.comp_hasFDerivWithinAt x hf

Chain Rule for Composition of Scalar and Vector Functions Within a Set (Equality Version)

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. If: 1. $h_2$ has derivative $h_2' \in \mathbb{K}'$ at a point $y \in \mathbb{K}'$, 2. $f$ has Fréchet derivative $f' : E \to \mathbb{K}'$ at $x \in E$ within a set $s \subseteq E$, 3. $y = f(x)$, then the composition $h_2 \circ f$ has Fréchet derivative $h_2' \cdot f'$ at $x$ within $s$.

HasDerivWithinAt.comp_hasFDerivWithinAt theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x) (hh : HasDerivWithinAt h₂ h₂' t (f x)) (hf : HasFDerivWithinAt f f' s x)
  (hst : MapsTo f s t) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Full source

theorem HasDerivWithinAt.comp_hasFDerivWithinAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x)
    (hh : HasDerivWithinAt h₂ h₂' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x :=
  hh.comp_hasFDerivAtFilter x hf <| hf.continuousWithinAt.tendsto_nhdsWithin hst

Chain Rule for Composition of Vector and Scalar Functions Within Sets

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. Suppose that at a point $x \in E$: 1. $h_2$ has derivative $h_2'$ within a set $t \subseteq \mathbb{K}'$ at $f(x)$, 2. $f$ has Fréchet derivative $f'$ within a set $s \subseteq E$ at $x$, 3. $f$ maps $s$ into $t$. Then the composition $h_2 \circ f$ has Fréchet derivative $h_2' \cdot f'$ within $s$ at $x$.

HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq theorem

 {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x) (hh : HasDerivWithinAt h₂ h₂' t y) (hf : HasFDerivWithinAt f f' s x)
  (hst : MapsTo f s t) (hy : y = f x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Full source

theorem HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x)
    (hh : HasDerivWithinAt h₂ h₂' t y) (hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t)
    (hy : y = f x) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x := by
  rw [hy] at hh; exact hh.comp_hasFDerivWithinAt x hf hst

Chain Rule for Composition of Scalar and Vector Functions Within Sets (Equality Version)

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Consider functions $f : E \to \mathbb{K}'$ and $h_2 : \mathbb{K}' \to \mathbb{K}'$. If: 1. $h_2$ has derivative $h_2'$ within a set $t \subseteq \mathbb{K}'$ at a point $y \in \mathbb{K}'$, 2. $f$ has Fréchet derivative $f'$ within a set $s \subseteq E$ at a point $x \in E$, 3. $f$ maps $s$ into $t$, 4. $y = f(x)$, then the composition $h_2 \circ f$ has Fréchet derivative $h_2' \cdot f'$ at $x$ within $s$.

HasDerivAtFilter.comp theorem

 (hh₂ : HasDerivAtFilter h₂ h₂' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
  HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Full source

theorem HasDerivAtFilter.comp (hh₂ : HasDerivAtFilter h₂ h₂' (h x) L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
    HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L := by
  rw [mul_comm]
  exact hh₂.scomp x hh hL

Chain Rule for Composition of Scalar-Valued Functions Along Filters

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Consider functions $h₂ : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $h₂$ has derivative $h₂'$ at $h(x)$ along filter $L'$, 2. $h$ has derivative $h'$ at $x$ along filter $L$, 3. The function $h$ tends to $L'$ along $L$ (i.e., $\lim_{L} h \in L'$), then the composition $h₂ \circ h$ has derivative $h₂' \cdot h'$ at $x$ along $L$.

HasDerivAtFilter.comp_of_eq theorem

 (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') (hy : y = h x) :
  HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Full source

theorem HasDerivAtFilter.comp_of_eq (hh₂ : HasDerivAtFilter h₂ h₂' y L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') (hy : y = h x) :
    HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L := by
  rw [hy] at hh₂; exact hh₂.comp x hh hL

Chain Rule for Composition of Scalar-Valued Functions Along Filters with Explicit Point Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Consider functions $h₂ : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $h₂$ has derivative $h₂'$ at $y$ along filter $L'$, 2. $h$ has derivative $h'$ at $x$ along filter $L$, 3. The function $h$ tends to $L'$ along $L$ (i.e., $\lim_{L} h \in L'$), 4. $y = h(x)$, then the composition $h₂ \circ h$ has derivative $h₂' \cdot h'$ at $x$ along $L$.

HasDerivWithinAt.comp theorem

 (hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') :
  HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Full source

theorem HasDerivWithinAt.comp (hh₂ : HasDerivWithinAt h₂ h₂' s' (h x))
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by
  rw [mul_comm]
  exact hh₂.scomp x hh hst

Chain Rule for Composition of Scalar-Valued Functions Within Sets

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Consider functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$. If: 1. $h_2$ has derivative $h_2'$ at $h(x)$ within the set $s' \subseteq \mathbb{K}'$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $s'$, then the composition $h_2 \circ h$ has derivative $h_2' \cdot h'$ at $x$ within $s$.

HasDerivWithinAt.comp_of_eq theorem

 (hh₂ : HasDerivWithinAt h₂ h₂' s' y) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') (hy : y = h x) :
  HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Full source

theorem HasDerivWithinAt.comp_of_eq (hh₂ : HasDerivWithinAt h₂ h₂' s' y)
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') (hy : y = h x) :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by
  rw [hy] at hh₂; exact hh₂.comp x hh hst

Chain Rule for Composition of Scalar-Valued Functions Within Sets with Point Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Consider functions $f : \mathbb{K}' \to \mathbb{K}'$ and $g : \mathbb{K} \to \mathbb{K}'$. If: 1. $f$ has derivative $f'$ at $y$ within the set $s' \subseteq \mathbb{K}'$, 2. $g$ has derivative $g'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $g$ maps $s$ into $s'$, 4. $y = g(x)$, then the composition $f \circ g$ has derivative $f' \cdot g'$ at $x$ within $s$.

HasDerivAt.comp theorem

(hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x

Full source

/-- 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`. -/
nonrec theorem HasDerivAt.comp (hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivAt h h' x) :
    HasDerivAt (h₂ ∘ h) (h₂' * h') x :=
  hh₂.comp x hh hh.continuousAt

Chain Rule for Derivatives of Scalar Function Compositions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $h_2$ has derivative $h_2'$ at $h(x)$, and 2. $h$ has derivative $h'$ at $x$, then the composition $h_2 \circ h$ has derivative $h_2' \cdot h'$ at $x$.

HasDerivAt.comp_of_eq theorem

(hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivAt h h' x) (hy : y = h x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x

Full source

/-- 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 HasDerivAt.comp_of_eq
    (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
    HasDerivAt (h₂ ∘ h) (h₂' * h') x := by
  rw [hy] at hh₂; exact hh₂.comp x hh

Chain Rule for Derivatives with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given functions $f : \mathbb{K}' \to \mathbb{K}'$ and $g : \mathbb{K} \to \mathbb{K}'$, suppose: 1. $f$ has derivative $f'$ at $y$, 2. $g$ has derivative $g'$ at $x$, 3. $y = g(x)$. Then the composition $f \circ g$ has derivative $f' \cdot g'$ at $x$.

HasStrictDerivAt.comp theorem

 (hh₂ : HasStrictDerivAt h₂ h₂' (h x)) (hh : HasStrictDerivAt h h' x) : HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Full source

theorem HasStrictDerivAt.comp (hh₂ : HasStrictDerivAt h₂ h₂' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x := by
  rw [mul_comm]
  exact hh₂.scomp x hh

Chain Rule for Strict Derivatives of Scalar Function Compositions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, if $h_2$ has strict derivative $h_2'$ at $h(x)$ and $h$ has strict derivative $h'$ at $x$, then the composition $h_2 \circ h$ has strict derivative $h_2' \cdot h'$ at $x$.

HasStrictDerivAt.comp_of_eq theorem

 (hh₂ : HasStrictDerivAt h₂ h₂' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
  HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Full source

theorem HasStrictDerivAt.comp_of_eq
    (hh₂ : HasStrictDerivAt h₂ h₂' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x := by
  rw [hy] at hh₂; exact hh₂.comp x hh

Chain Rule for Strict Derivatives with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, suppose: 1. $h_2$ has strict derivative $h_2'$ at $y$, 2. $h$ has strict derivative $h'$ at $x$, 3. $y = h(x)$. Then the composition $h_2 \circ h$ has strict derivative $h_2' \cdot h'$ at $x$.

HasDerivAt.comp_hasDerivWithinAt theorem

(hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Full source

theorem HasDerivAt.comp_hasDerivWithinAt (hh₂ : HasDerivAt h₂ h₂' (h x))
    (hh : HasDerivWithinAt h h' s x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x :=
  hh₂.hasDerivWithinAt.comp x hh (mapsTo_univ _ _)

Chain Rule for Composition of Scalar-Valued Functions with Differentiability Within a Set

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $h_2$ has derivative $h_2'$ at $h(x)$, and 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, then the composition $h_2 \circ h$ has derivative $h_2' \cdot h'$ at $x$ within $s$.

HasDerivAt.comp_hasDerivWithinAt_of_eq theorem

 (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Full source

theorem HasDerivAt.comp_hasDerivWithinAt_of_eq (hh₂ : HasDerivAt h₂ h₂' y)
    (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by
  rw [hy] at hh₂; exact hh₂.comp_hasDerivWithinAt x hh

Chain Rule for Composition with Point Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, suppose: 1. $h_2$ has derivative $h_2'$ at $y$, 2. $h$ has derivative $h'$ at $x$ within the set $s \subseteq \mathbb{K}$, 3. $y = h(x)$. Then the composition $h_2 \circ h$ has derivative $h_2' \cdot h'$ at $x$ within $s$.

derivWithin_comp theorem

 (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s') :
  derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Full source

theorem derivWithin_comp (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x))
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s') :
    derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x := by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hh₂.hasDerivWithinAt.comp x hh.hasDerivWithinAt hs).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Chain Rule for Differentiable Compositions Within Sets

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $h_2$ is differentiable at $h(x)$ within $s' \subseteq \mathbb{K}'$, 2. $h$ is differentiable at $x$ within $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $s'$, then the derivative of the composition $h_2 \circ h$ at $x$ within $s$ satisfies: \[ \frac{d}{dx}\Big|_{s} (h_2 \circ h)(x) = \left(\frac{d}{dy}\Big|_{s'} h_2(y)\right)\Big|_{y=h(x)} \cdot \frac{d}{dx}\Big|_{s} h(x). \]

derivWithin_comp_of_eq theorem

 (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s') (hy : h x = y) :
  derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Full source

theorem derivWithin_comp_of_eq (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y)
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s')
    (hy : h x = y) :
    derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x := by
  subst hy; exact derivWithin_comp x hh₂ hh hs

Chain Rule for Differentiable Compositions Within Sets with Point Equality

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being an algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ and $h : \mathbb{K} \to \mathbb{K}'$, if: 1. $h_2$ is differentiable at $y$ within $s' \subseteq \mathbb{K}'$, 2. $h$ is differentiable at $x$ within $s \subseteq \mathbb{K}$, 3. $h$ maps $s$ into $s'$, 4. $h(x) = y$, then the derivative of the composition $h_2 \circ h$ at $x$ within $s$ satisfies: \[ \frac{d}{dx}\Big|_{s} (h_2 \circ h)(x) = \left(\frac{d}{dy}\Big|_{s'} h_2(y)\right) \cdot \frac{d}{dx}\Big|_{s} h(x). \]

deriv_comp theorem

 (hh₂ : DifferentiableAt 𝕜' h₂ (h x)) (hh : DifferentiableAt 𝕜 h x) : deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Full source

theorem deriv_comp (hh₂ : DifferentiableAt 𝕜' h₂ (h x)) (hh : DifferentiableAt 𝕜 h x) :
    deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x :=
  (hh₂.hasDerivAt.comp x hh.hasDerivAt).deriv

Chain Rule for Differentiable Scalar Function Compositions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given differentiable functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ at $h(x)$ and $h : \mathbb{K} \to \mathbb{K}'$ at $x$, the derivative of their composition $h_2 \circ h$ at $x$ satisfies: \[ \frac{d}{dx}(h_2 \circ h)(x) = h_2'(h(x)) \cdot h'(x) \] where $h_2'$ and $h'$ are the derivatives of $h_2$ and $h$ respectively.

deriv_comp_of_eq theorem

 (hh₂ : DifferentiableAt 𝕜' h₂ y) (hh : DifferentiableAt 𝕜 h x) (hy : h x = y) :
  deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Full source

theorem deriv_comp_of_eq (hh₂ : DifferentiableAt 𝕜' h₂ y) (hh : DifferentiableAt 𝕜 h x)
    (hy : h x = y) :
    deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x := by
  subst hy; exact deriv_comp x hh₂ hh

Chain Rule for Differentiable Compositions with Point Equality

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Given functions $h_2 : \mathbb{K}' \to \mathbb{K}'$ differentiable at $y$ and $h : \mathbb{K} \to \mathbb{K}'$ differentiable at $x$, with $h(x) = y$, the derivative of their composition satisfies: \[ \frac{d}{dx}(h_2 \circ h)(x) = h_2'(y) \cdot h'(x) \] where $h_2'$ and $h'$ are the derivatives of $h_2$ and $h$ respectively.

HasDerivAtFilter.iterate theorem

 {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAtFilter f f' x L) (hL : Tendsto f L L) (hx : f x = x) (n : ℕ) :
  HasDerivAtFilter f^[n] (f' ^ n) x L

Full source

protected nonrec theorem HasDerivAtFilter.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
    (hf : HasDerivAtFilter f f' x L) (hL : Tendsto f L L) (hx : f x = x) (n : ℕ) :
    HasDerivAtFilter f^[n] (f' ^ n) x L := by
  have := hf.iterate hL hx n
  rwa [ContinuousLinearMap.smulRight_one_pow] at this

Derivative of Iterated Function Along a Filter: $(f^{[n]})' = (f')^n$ at Fixed Point

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function with derivative $f'$ at $x$ along the filter $L$, and suppose $f$ maps $L$ to itself and $f(x) = x$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ has derivative $(f')^n$ at $x$ along $L$.

HasDerivAt.iterate theorem

{f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) (hx : f x = x) (n : ℕ) : HasDerivAt f^[n] (f' ^ n) x

Full source

protected nonrec theorem HasDerivAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x)
    (hx : f x = x) (n : ℕ) : HasDerivAt f^[n] (f' ^ n) x :=
  hf.iterate _ (have := hf.tendsto_nhds le_rfl; by rwa [hx] at this) hx n

Derivative of Iterated Function at Fixed Point: $(f^{[n]})'(x) = (f'(x))^n$

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function differentiable at $x \in \mathbb{K}$ with derivative $f'$, and suppose $f(x) = x$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is differentiable at $x$ with derivative $(f')^n$.

HasDerivWithinAt.iterate theorem

 {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivWithinAt f f' s x) (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) :
  HasDerivWithinAt f^[n] (f' ^ n) s x

Full source

protected theorem HasDerivWithinAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivWithinAt f f' s x)
    (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) : HasDerivWithinAt f^[n] (f' ^ n) s x := by
  have := HasFDerivWithinAt.iterate hf hx hs n
  rwa [ContinuousLinearMap.smulRight_one_pow] at this

Derivative of the $n$-th iterate of a function at a fixed point within a set

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function differentiable at $x$ within a set $s \subseteq \mathbb{K}$ with derivative $f'$, and suppose $f(x) = x$ and $f$ maps $s$ into itself. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is differentiable at $x$ within $s$ with derivative $(f')^n$.

HasStrictDerivAt.iterate theorem

 {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasStrictDerivAt f f' x) (hx : f x = x) (n : ℕ) : HasStrictDerivAt f^[n] (f' ^ n) x

Full source

protected nonrec theorem HasStrictDerivAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
    (hf : HasStrictDerivAt f f' x) (hx : f x = x) (n : ℕ) :
    HasStrictDerivAt f^[n] (f' ^ n) x := by
  have := hf.iterate hx n
  rwa [ContinuousLinearMap.smulRight_one_pow] at this

Strict derivative of iterated function at fixed point: $(f^{[n]})'(x) = (f'(x))^n$

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function that has strict derivative $f'$ at point $x$, and suppose $f(x) = x$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ has strict derivative $(f')^n$ at $x$.

HasFDerivWithinAt.comp_hasDerivWithinAt theorem

 {t : Set F} (hl : HasFDerivWithinAt l l' t (f x)) (hf : HasDerivWithinAt f f' s x) (hst : MapsTo f s t) :
  HasDerivWithinAt (l ∘ f) (l' f') s x

Full source

/-- 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 {t : Set F} (hl : HasFDerivWithinAt l l' t (f x))
    (hf : HasDerivWithinAt f f' s x) (hst : MapsTo f s t) :
    HasDerivWithinAt (l ∘ f) (l' f') s x := by
  simpa only [one_apply, one_smul, smulRight_apply, coe_comp', (· ∘ ·)] using
    (hl.comp x hf.hasFDerivWithinAt hst).hasDerivWithinAt

Chain Rule for Composition of Fréchet Differentiable and Scalar Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $F$ and $E$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ and $t \subseteq F$ be subsets, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$ within $s$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $f(x)$ within $t$, 3. $f$ maps $s$ into $t$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$ within $s$.

HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq theorem

 {t : Set F} (hl : HasFDerivWithinAt l l' t y) (hf : HasDerivWithinAt f f' s x) (hst : MapsTo f s t) (hy : y = f x) :
  HasDerivWithinAt (l ∘ f) (l' f') s x

Full source

/-- 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 {t : Set F}
    (hl : HasFDerivWithinAt l l' t y)
    (hf : HasDerivWithinAt f f' s x) (hst : MapsTo f s t) (hy : y = f x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x := by
  rw [hy] at hl; exact hl.comp_hasDerivWithinAt x hf hst

Chain Rule for Composition with Point Equality Condition

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $F$ and $E$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ and $t \subseteq F$ be subsets, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$ within $s$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $y$ within $t$, 3. $f$ maps $s$ into $t$, 4. $y = f(x)$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$ within $s$.

HasFDerivAt.comp_hasDerivWithinAt theorem

(hl : HasFDerivAt l l' (f x)) (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (l ∘ f) (l' f') s x

Full source

theorem HasFDerivAt.comp_hasDerivWithinAt (hl : HasFDerivAt l l' (f x))
    (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (l ∘ f) (l' f') s x :=
  hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf (mapsTo_univ _ _)

Chain Rule for Composition of Fréchet Differentiable and Scalar Differentiable Functions (Within a Subset)

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ be a subset, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$ within $s$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $f(x)$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$ within $s$.

HasFDerivAt.comp_hasDerivWithinAt_of_eq theorem

(hl : HasFDerivAt l l' y) (hf : HasDerivWithinAt f f' s x) (hy : y = f x) : HasDerivWithinAt (l ∘ f) (l' f') s x

Full source

theorem HasFDerivAt.comp_hasDerivWithinAt_of_eq (hl : HasFDerivAt l l' y)
    (hf : HasDerivWithinAt f f' s x) (hy : y = f x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x := by
  rw [hy] at hl; exact hl.comp_hasDerivWithinAt x hf

Chain Rule for Composition with Point Equality Condition (Within a Subset)

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ be a subset, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$ within $s$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $y$, 3. $y = f(x)$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$ within $s$.

HasFDerivAt.comp_hasDerivAt theorem

(hl : HasFDerivAt l l' (f x)) (hf : HasDerivAt f f' x) : HasDerivAt (l ∘ f) (l' f') x

Full source

/-- 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 (hl : HasFDerivAt l l' (f x)) (hf : HasDerivAt f f' x) :
    HasDerivAt (l ∘ f) (l' f') x :=
  hasDerivWithinAt_univ.mp <| hl.comp_hasDerivWithinAt x hf.hasDerivWithinAt

Chain Rule for Composition of Fréchet Differentiable and Scalar Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $f(x)$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$.

HasFDerivAt.comp_hasDerivAt_of_eq theorem

(hl : HasFDerivAt l l' y) (hf : HasDerivAt f f' x) (hy : y = f x) : HasDerivAt (l ∘ f) (l' f') x

Full source

/-- 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
    (hl : HasFDerivAt l l' y) (hf : HasDerivAt f f' x) (hy : y = f x) :
    HasDerivAt (l ∘ f) (l' f') x := by
  rw [hy] at hl; exact hl.comp_hasDerivAt x hf

Chain Rule for Composition with Point Equality Condition: $(l \circ f)'(x) = l'(f(x)) \cdot f'(x)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ has derivative $f'$ at $x$, 2. $l : F \to E$ has Fréchet derivative $l'$ at $y$, 3. $y = f(x)$. Then the composition $l \circ f : \mathbb{K} \to E$ has derivative $l'(f')$ at $x$.

HasStrictFDerivAt.comp_hasStrictDerivAt theorem

(hl : HasStrictFDerivAt l l' (f x)) (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (l ∘ f) (l' f') x

Full source

theorem HasStrictFDerivAt.comp_hasStrictDerivAt (hl : HasStrictFDerivAt l l' (f x))
    (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (l ∘ f) (l' f') x := by
  simpa only [one_apply, one_smul, smulRight_apply, coe_comp', (· ∘ ·)] using
    (hl.comp x hf.hasStrictFDerivAt).hasStrictDerivAt

Chain Rule for Strict Derivatives: $(l \circ f)'(x) = l'(f(x)) \cdot f'(x)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$. Suppose $f : \mathbb{K} \to E$ has a strict derivative $f' \in E$ at $x \in \mathbb{K}$, and $l : E \to F$ has a strict Fréchet derivative $l' : E \to F$ at $f(x)$. Then the composition $l \circ f : \mathbb{K} \to F$ has a strict derivative at $x$ given by $l'(f') \in F$.

HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq theorem

(hl : HasStrictFDerivAt l l' y) (hf : HasStrictDerivAt f f' x) (hy : y = f x) : HasStrictDerivAt (l ∘ f) (l' f') x

Full source

theorem HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq (hl : HasStrictFDerivAt l l' y)
    (hf : HasStrictDerivAt f f' x) (hy : y = f x) :
    HasStrictDerivAt (l ∘ f) (l' f') x := by
  rw [hy] at hl; exact hl.comp_hasStrictDerivAt x hf

Chain Rule for Strict Derivatives with Equality Condition: $(l \circ f)'(x) = l'(f(x)) \cdot f'(x)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$. Suppose $f : \mathbb{K} \to E$ has a strict derivative $f' \in E$ at $x \in \mathbb{K}$, and $l : E \to F$ has a strict Fréchet derivative $l' : E \to F$ at $y \in E$. If $y = f(x)$, then the composition $l \circ f : \mathbb{K} \to F$ has a strict derivative at $x$ given by $l'(f') \in F$.

fderivWithin_comp_derivWithin theorem

 {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) :
  derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x)

Full source

theorem fderivWithin_comp_derivWithin {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) :
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x) := by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Chain Rule for Derivatives within Sets: $\text{derivWithin}\, (l \circ f)\, s\, x = \text{fderivWithin}\, l\, t\, (f x) \left(\text{derivWithin}\, f\, s\, x\right)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ and $t \subseteq F$ be subsets, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ is differentiable at $x$ within $s$, 2. $l : F \to E$ is differentiable at $f(x)$ within $t$, 3. $f$ maps $s$ into $t$. Then the derivative of the composition $l \circ f$ at $x$ within $s$ is given by: \[ \text{derivWithin}\, (l \circ f)\, s\, x = \text{fderivWithin}\, l\, t\, (f x) \left(\text{derivWithin}\, f\, s\, x\right). \]

fderivWithin_comp_derivWithin_of_eq theorem

 {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t y) (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t)
  (hy : y = f x) : derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x)

Full source

theorem fderivWithin_comp_derivWithin_of_eq {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t y)
    (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) (hy : y = f x) :
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x) := by
  rw [hy] at hl; exact fderivWithin_comp_derivWithin x hl hf hs

Chain Rule for Derivatives within Sets with Equality Condition: $\text{derivWithin}\, (l \circ f)\, s\, x = \text{fderivWithin}\, l\, t\, (f x) \left(\text{derivWithin}\, f\, s\, x\right)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $s \subseteq \mathbb{K}$ and $t \subseteq F$ be subsets, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ is differentiable at $x$ within $s$, 2. $l : F \to E$ is differentiable at $y$ within $t$, 3. $f$ maps $s$ into $t$, 4. $y = f(x)$. Then the derivative of the composition $l \circ f$ at $x$ within $s$ is given by: \[ \text{derivWithin}\, (l \circ f)\, s\, x = \text{fderivWithin}\, l\, t\, (f x) \left(\text{derivWithin}\, f\, s\, x\right). \]

fderiv_comp_deriv theorem

 (hl : DifferentiableAt 𝕜 l (f x)) (hf : DifferentiableAt 𝕜 f x) :
  deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x)

Full source

theorem fderiv_comp_deriv (hl : DifferentiableAt 𝕜 l (f x)) (hf : DifferentiableAt 𝕜 f x) :
    deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x) :=
  (hl.hasFDerivAt.comp_hasDerivAt x hf.hasDerivAt).deriv

Chain Rule for Composition of Differentiable Functions: $\text{deriv}\, (l \circ f)\, x = \text{fderiv}\, l\, (f x) \left(\text{deriv}\, f\, x\right)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ is differentiable at $x$, 2. $l : F \to E$ is differentiable at $f(x)$. Then the derivative of the composition $l \circ f$ at $x$ is given by: \[ \text{deriv}\, (l \circ f)\, x = \text{fderiv}\, l\, (f x) \left(\text{deriv}\, f\, x\right). \]

fderiv_comp_deriv_of_eq theorem

 (hl : DifferentiableAt 𝕜 l y) (hf : DifferentiableAt 𝕜 f x) (hy : y = f x) :
  deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x)

Full source

theorem fderiv_comp_deriv_of_eq (hl : DifferentiableAt 𝕜 l y) (hf : DifferentiableAt 𝕜 f x)
    (hy : y = f x) :
    deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x) := by
  rw [hy] at hl; exact fderiv_comp_deriv x hl hf

Chain Rule for Composition with Equality Condition: $\text{deriv}\, (l \circ f)\, x = \text{fderiv}\, l\, (f x) \left(\text{deriv}\, f\, x\right)$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $x \in \mathbb{K}$. Suppose: 1. $f : \mathbb{K} \to F$ is differentiable at $x$, 2. $l : F \to E$ is differentiable at $y$, 3. $y = f(x)$. Then the derivative of the composition $l \circ f$ at $x$ is given by: \[ \text{deriv}\, (l \circ f)\, x = \text{fderiv}\, l\, (f x) \left(\text{deriv}\, f\, x\right). \]

Keywords