Mathlib.Analysis.Calculus.FDeriv.Comp

HasFDerivAtFilter.comp theorem

 {g : F → G} {g' : F →L[𝕜] G} {L' : Filter F} (hg : HasFDerivAtFilter g g' (f x) L') (hf : HasFDerivAtFilter f f' x L)
  (hL : Tendsto f L L') : HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Full source

theorem HasFDerivAtFilter.comp {g : F → G} {g' : F →L[𝕜] G} {L' : Filter F}
    (hg : HasFDerivAtFilter g g' (f x) L') (hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L') :
    HasFDerivAtFilter (g ∘ f) (g'.comp f') x L := by
  let eq₁ := (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO
  let eq₂ := (hg.isLittleO.comp_tendsto hL).trans_isBigO hf.isBigO_sub
  refine .of_isLittleO <| eq₂.triangle <| eq₁.congr_left fun x' => ?_
  simp

Chain Rule for Fréchet Derivatives Along Filters

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $f'$ at $x \in E$ along a filter $L$, and $g : F \to G$ has a Fréchet derivative $g'$ at $f(x)$ along a filter $L'$. If $f$ tends to $L'$ along $L$, then the composition $g \circ f$ has a Fréchet derivative at $x$ along $L$ given by the composition $g' \circ f'$.

HasFDerivWithinAt.comp theorem

 {g : F → G} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x)
  (hst : MapsTo f s t) : HasFDerivWithinAt (g ∘ f) (g'.comp f') s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.comp {g : F → G} {g' : F →L[𝕜] G} {t : Set F}
    (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t) :
    HasFDerivWithinAt (g ∘ f) (g'.comp f') s x :=
  HasFDerivAtFilter.comp x hg hf <| hf.continuousWithinAt.tendsto_nhdsWithin hst

Chain Rule for Fréchet Derivatives within Sets

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ has a Fréchet derivative $g'$ at $f(x)$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$, then the composition $g \circ f$ has a Fréchet derivative at $x$ within $s$ given by the composition $g' \circ f'$.

HasFDerivAt.comp_hasFDerivWithinAt theorem

 {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivWithinAt f f' s x) :
  HasFDerivWithinAt (g ∘ f) (g'.comp f') s x

Full source

@[fun_prop]
theorem HasFDerivAt.comp_hasFDerivWithinAt {g : F → G} {g' : F →L[𝕜] G}
    (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (g ∘ f) (g'.comp f') s x :=
  hg.comp x hf hf.continuousWithinAt

Chain Rule for Fréchet Derivatives: Global-to-Local Version

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ has a Fréchet derivative $g'$ at $f(x)$. Then the composition $g \circ f$ has a Fréchet derivative at $x$ within $s$ given by the composition $g' \circ f'$.

HasFDerivWithinAt.comp_of_tendsto theorem

 {g : F → G} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x)
  (hst : Tendsto f (𝓝[s] x) (𝓝[t] f x)) : HasFDerivWithinAt (g ∘ f) (g'.comp f') s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.comp_of_tendsto {g : F → G} {g' : F →L[𝕜] G} {t : Set F}
    (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x)
    (hst : Tendsto f (𝓝[s] x) (𝓝[t] f x)) : HasFDerivWithinAt (g ∘ f) (g'.comp f') s x :=
  HasFDerivAtFilter.comp x hg hf hst

Chain Rule for Fréchet Derivatives with Tendsto Condition

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ has a Fréchet derivative $g'$ at $f(x)$ within a set $t \subseteq F$. If $f$ tends to $t$ within $s$ as $x' \to x$, then the composition $g \circ f$ has a Fréchet derivative at $x$ within $s$ given by the composition $g' \circ f'$.

HasFDerivAt.comp theorem

 {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) :
  HasFDerivAt (g ∘ f) (g'.comp f') x

Full source

/-- The chain rule. -/
@[fun_prop]
theorem HasFDerivAt.comp {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x))
    (hf : HasFDerivAt f f' x) : HasFDerivAt (g ∘ f) (g'.comp f') x :=
  HasFDerivAtFilter.comp x hg hf hf.continuousAt

Chain Rule for Fréchet Derivatives at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is Fréchet differentiable at $x \in E$ with derivative $f'$, and $g \colon F \to G$ is Fréchet differentiable at $f(x)$ with derivative $g'$, then the composition $g \circ f$ is Fréchet differentiable at $x$ with derivative $g' \circ f'$.

DifferentiableWithinAt.comp theorem

 {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
  (h : MapsTo f s t) : DifferentiableWithinAt 𝕜 (g ∘ f) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.comp {g : F → G} {t : Set F}
    (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
    (h : MapsTo f s t) : DifferentiableWithinAt 𝕜 (g ∘ f) s x :=
  (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).differentiableWithinAt

Differentiability of Composition within Sets (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $f(x)$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$, then the composition $g \circ f$ is differentiable at $x$ within $s$.

DifferentiableWithinAt.comp' theorem

 {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) :
  DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.comp' {g : F → G} {t : Set F}
    (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x :=
  hg.comp x (hf.mono inter_subset_left) inter_subset_right

Chain Rule for Differentiability within Intersection of Sets

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $f(x)$ within a set $t \subseteq F$. Then the composition $g \circ f$ is differentiable at $x$ within the intersection $s \cap f^{-1}(t)$.

DifferentiableAt.comp theorem

{g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (g ∘ f) x

Full source

@[fun_prop]
theorem DifferentiableAt.comp {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
    (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (g ∘ f) x :=
  (hg.hasFDerivAt.comp x hf.hasFDerivAt).differentiableAt

Differentiability of Function Composition (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is differentiable at $x \in E$ and $g \colon F \to G$ is differentiable at $f(x)$, then the composition $g \circ f$ is differentiable at $x$.

DifferentiableAt.comp_differentiableWithinAt theorem

 {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) :
  DifferentiableWithinAt 𝕜 (g ∘ f) s x

Full source

@[fun_prop]
theorem DifferentiableAt.comp_differentiableWithinAt {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (g ∘ f) s x :=
  hg.differentiableWithinAt.comp x hf (mapsTo_univ _ _)

Differentiability of Composition within a Set (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$ and $g \colon F \to G$ is differentiable at $f(x)$, then the composition $g \circ f$ is differentiable at $x$ within $s$.

fderivWithin_comp theorem

 {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
  (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Full source

theorem fderivWithin_comp {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
  (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).fderivWithin hxs

Chain Rule for Fréchet Derivatives within Sets: $\text{fderivWithin}_{\mathbb{K}} (g \circ f) s x = (\text{fderivWithin}_{\mathbb{K}} g t (f x)) \circ (\text{fderivWithin}_{\mathbb{K}} f s x)$

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $f(x)$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$ and $s$ is uniquely differentiable at $x$, then the Fréchet derivative of the composition $g \circ f$ at $x$ within $s$ is given by the composition of the derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x = (\text{fderivWithin}_{\mathbb{K}} g t (f x)) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

fderivWithin_comp_of_eq theorem

 {g : F → G} {t : Set F} {y : F} (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x)
  (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
  fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Full source

theorem fderivWithin_comp_of_eq {g : F → G} {t : Set F} {y : F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
    fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by
  subst hy; exact fderivWithin_comp _ hg hf h hxs

Chain Rule for Fréchet Derivatives within Sets with Point Equality

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $y \in F$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$, $s$ is uniquely differentiable at $x$, and $f(x) = y$, then the Fréchet derivative of the composition $g \circ f$ at $x$ within $s$ is given by the composition of the derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x = (\text{fderivWithin}_{\mathbb{K}} g t (f x)) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

fderivWithin_comp' theorem

 {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
  (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (fun y ↦ g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Full source

/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderivWithin_comp' {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y ↦ g (f y)) s x
      = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
  fderivWithin_comp _ hg hf h hxs

Chain Rule for Fréchet Derivatives within Sets (Point-Free Form)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $f(x)$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$ and $s$ is uniquely differentiable at $x$, then the Fréchet derivative of the function $y \mapsto g(f(y))$ at $x$ within $s$ is given by the composition of the derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (y \mapsto g(f(y))) s x = (\text{fderivWithin}_{\mathbb{K}} g t (f x)) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

fderivWithin_comp_of_eq' theorem

 {g : F → G} {t : Set F} {y : F} (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x)
  (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
  fderivWithin 𝕜 (fun y ↦ g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Full source

/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderivWithin_comp_of_eq' {g : F → G} {t : Set F} {y : F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
    fderivWithin 𝕜 (fun y ↦ g (f y)) s x
      = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by
  subst hy; exact fderivWithin_comp _ hg hf h hxs

Chain Rule for Fréchet Derivatives within Sets with Explicit Point Equality

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $y \in F$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$, $s$ is uniquely differentiable at $x$, and $f(x) = y$, then the Fréchet derivative of the composition $g \circ f$ at $x$ within $s$ is given by the composition of the derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x = (\text{fderivWithin}_{\mathbb{K}} g t y) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

fderivWithin_fderivWithin theorem

 {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t y)
  (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) (v : E) :
  fderivWithin 𝕜 g t y (fderivWithin 𝕜 f s x v) = fderivWithin 𝕜 (g ∘ f) s x v

Full source

/-- A version of `fderivWithin_comp` that is useful to rewrite the composition of two derivatives
  into a single derivative. This version always applies, but creates a new side-goal `f x = y`. -/
theorem fderivWithin_fderivWithin {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E} {t : Set F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) (v : E) :
    fderivWithin 𝕜 g t y (fderivWithin 𝕜 f s x v) = fderivWithin 𝕜 (g ∘ f) s x v := by
  subst y
  rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]

Chain Rule for Fréchet Derivatives within Sets: $\text{fderivWithin}_{\mathbb{K}} g t (f x) \circ \text{fderivWithin}_{\mathbb{K}} f s x = \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x$

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $y = f(x) \in F$ within a set $t \subseteq F$. If $f$ maps $s$ into $t$ and $s$ is uniquely differentiable at $x$, then for any vector $v \in E$, the following equality holds: \[ \text{fderivWithin}_{\mathbb{K}} g t y (\text{fderivWithin}_{\mathbb{K}} f s x v) = \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x v. \]

fderivWithin_comp₃ theorem

 {g' : G → G'} {g : F → G} {t : Set F} {u : Set G} {y : F} {y' : G} (hg' : DifferentiableWithinAt 𝕜 g' u y')
  (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h2g : MapsTo g t u) (h2f : MapsTo f s t)
  (h3g : g y = y') (h3f : f x = y) (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (g' ∘ g ∘ f) s x = (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s x))

Full source

/-- Ternary version of `fderivWithin_comp`, with equality assumptions of basepoints added, in
  order to apply more easily as a rewrite from right-to-left. -/
theorem fderivWithin_comp₃ {g' : G → G'} {g : F → G} {t : Set F} {u : Set G} {y : F} {y' : G}
    (hg' : DifferentiableWithinAt 𝕜 g' u y') (hg : DifferentiableWithinAt 𝕜 g t y)
    (hf : DifferentiableWithinAt 𝕜 f s x) (h2g : MapsTo g t u) (h2f : MapsTo f s t) (h3g : g y = y')
    (h3f : f x = y) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
      (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s x)) := by
  substs h3g h3f
  exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
    h2g.comp h2f).fderivWithin hxs

Chain Rule for Triple Composition of Fréchet Derivatives within Sets

Informal description

Let $E$, $F$, $G$, and $G'$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, $g : F \to G$ is differentiable at $y = f(x) \in F$ within a set $t \subseteq F$, and $g' : G \to G'$ is differentiable at $y' = g(y) \in G$ within a set $u \subseteq G$. If $f$ maps $s$ into $t$, $g$ maps $t$ into $u$, and $s$ is uniquely differentiable at $x$, then the Fréchet derivative of the composition $g' \circ g \circ f$ at $x$ within $s$ is given by the composition of derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (g' \circ g \circ f) s x = (\text{fderivWithin}_{\mathbb{K}} g' u y') \circ (\text{fderivWithin}_{\mathbb{K}} g t y) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

fderiv_comp theorem

 {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
  fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x)

Full source

theorem fderiv_comp {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
  (hg.hasFDerivAt.comp x hf.hasFDerivAt).fderiv

Chain Rule for Fréchet Derivatives

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is differentiable at $x \in E$ and $g \colon F \to G$ is differentiable at $f(x)$, then the Fréchet derivative of the composition $g \circ f$ at $x$ is given by the composition of the derivatives: \[ \text{fderiv}_{\mathbb{K}} (g \circ f) x = (\text{fderiv}_{\mathbb{K}} g (f x)) \circ (\text{fderiv}_{\mathbb{K}} f x). \]

fderiv_comp' theorem

 {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
  fderiv 𝕜 (fun y ↦ g (f y)) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x)

Full source

/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderiv_comp' {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (fun y ↦ g (f y)) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
  fderiv_comp x hg hf

Chain Rule for Fréchet Derivatives (Pointwise Composition)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is differentiable at $x \in E$ and $g \colon F \to G$ is differentiable at $f(x)$, then the Fréchet derivative of the function $y \mapsto g(f(y))$ at $x$ is given by the composition of the derivatives: \[ \text{fderiv}_{\mathbb{K}} (y \mapsto g(f(y))) x = (\text{fderiv}_{\mathbb{K}} g (f x)) \circ (\text{fderiv}_{\mathbb{K}} f x). \]

fderiv_comp_fderivWithin theorem

 {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (fderivWithin 𝕜 f s x)

Full source

theorem fderiv_comp_fderivWithin {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (fderivWithin 𝕜 f s x) :=
  (hg.hasFDerivAt.comp_hasFDerivWithinAt x hf.hasFDerivWithinAt).fderivWithin hxs

Chain Rule for Fréchet Derivatives Within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable at $x \in E$ within a set $s \subseteq E$, and $g : F \to G$ is differentiable at $f(x)$. If $s$ is uniquely differentiable at $x$ (i.e., the tangent cone at $x$ spans a dense subspace of $E$), then the Fréchet derivative of the composition $g \circ f$ at $x$ within $s$ is equal to the composition of the Fréchet derivatives: \[ \text{fderivWithin}_{\mathbb{K}} (g \circ f) s x = (\text{fderiv}_{\mathbb{K}} g (f x)) \circ (\text{fderivWithin}_{\mathbb{K}} f s x). \]

DifferentiableOn.comp theorem

 {g : F → G} {t : Set F} (hg : DifferentiableOn 𝕜 g t) (hf : DifferentiableOn 𝕜 f s) (st : MapsTo f s t) :
  DifferentiableOn 𝕜 (g ∘ f) s

Full source

@[fun_prop]
theorem DifferentiableOn.comp {g : F → G} {t : Set F} (hg : DifferentiableOn 𝕜 g t)
    (hf : DifferentiableOn 𝕜 f s) (st : MapsTo f s t) : DifferentiableOn 𝕜 (g ∘ f) s :=
  fun x hx => DifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

Differentiability of Composition on Sets (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f : E \to F$ is differentiable on a set $s \subseteq E$, and $g : F \to G$ is differentiable on a set $t \subseteq F$. If $f$ maps $s$ into $t$, then the composition $g \circ f$ is differentiable on $s$.

Differentiable.comp theorem

{g : F → G} (hg : Differentiable 𝕜 g) (hf : Differentiable 𝕜 f) : Differentiable 𝕜 (g ∘ f)

Full source

@[fun_prop]
theorem Differentiable.comp {g : F → G} (hg : Differentiable 𝕜 g) (hf : Differentiable 𝕜 f) :
    Differentiable 𝕜 (g ∘ f) :=
  fun x => DifferentiableAt.comp x (hg (f x)) (hf x)

Differentiability of Function Composition (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ and $g \colon F \to G$ are differentiable functions, then their composition $g \circ f \colon E \to G$ is also differentiable.

Differentiable.comp_differentiableOn theorem

{g : F → G} (hg : Differentiable 𝕜 g) (hf : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (g ∘ f) s

Full source

@[fun_prop]
theorem Differentiable.comp_differentiableOn {g : F → G} (hg : Differentiable 𝕜 g)
    (hf : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (g ∘ f) s :=
  hg.differentiableOn.comp hf (mapsTo_univ _ _)

Differentiability of Composition with Differentiable Function on a Set (Chain Rule)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If $f \colon E \to F$ is differentiable on a set $s \subseteq E$ and $g \colon F \to G$ is differentiable, then the composition $g \circ f$ is differentiable on $s$.

HasStrictFDerivAt.comp theorem

 {g : F → G} {g' : F →L[𝕜] G} (hg : HasStrictFDerivAt g g' (f x)) (hf : HasStrictFDerivAt f f' x) :
  HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x

Full source

/-- The chain rule for derivatives in the sense of strict differentiability. -/
@[fun_prop]
protected theorem HasStrictFDerivAt.comp {g : F → G} {g' : F →L[𝕜] G}
    (hg : HasStrictFDerivAt g g' (f x)) (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x :=
  .of_isLittleO <|
    ((hg.isLittleO.comp_tendsto (hf.continuousAt.prodMap' hf.continuousAt)).trans_isBigO
        hf.isBigO_sub).triangle <| by
      simpa only [g'.map_sub, f'.coe_comp'] using (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO

Chain Rule for Strict Fréchet Derivatives

Informal description

Let $E$, $F$, and $G$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f \colon E \to F$ has a strict Fréchet derivative $f'$ at $x \in E$, and $g \colon F \to G$ has a strict Fréchet derivative $g'$ at $f(x)$. Then the composition $g \circ f$ has a strict Fréchet derivative at $x$ given by the composition $g' \circ f'$ of the derivatives. In symbols: \[ \text{HasStrictFDerivAt } f \, f' \, x \text{ and } \text{HasStrictFDerivAt } g \, g' \, (f x) \implies \text{HasStrictFDerivAt } (g \circ f) \, (g' \circ f') \, x. \]

Differentiable.iterate theorem

{f : E → E} (hf : Differentiable 𝕜 f) (n : ℕ) : Differentiable 𝕜 f^[n]

Full source

@[fun_prop]
protected theorem Differentiable.iterate {f : E → E} (hf : Differentiable 𝕜 f) (n : ℕ) :
    Differentiable 𝕜 f^[n] :=
  Nat.recOn n differentiable_id fun _ ihn => ihn.comp hf

Differentiability of Iterated Functions: $(f^n)' = (f')^n$

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$. If $f : E \to E$ is a differentiable function, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ (the function obtained by composing $f$ with itself $n$ times) is also differentiable.

DifferentiableOn.iterate theorem

{f : E → E} (hf : DifferentiableOn 𝕜 f s) (hs : MapsTo f s s) (n : ℕ) : DifferentiableOn 𝕜 f^[n] s

Full source

@[fun_prop]
protected theorem DifferentiableOn.iterate {f : E → E} (hf : DifferentiableOn 𝕜 f s)
    (hs : MapsTo f s s) (n : ℕ) : DifferentiableOn 𝕜 f^[n] s :=
  Nat.recOn n differentiableOn_id fun _ ihn => ihn.comp hf hs

Differentiability of Iterated Function on Invariant Subset

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function that is differentiable on a subset $s \subseteq E$. If $f$ maps $s$ into itself (i.e., $f(s) \subseteq s$), then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is differentiable on $s$.

HasFDerivAtFilter.iterate theorem

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

Full source

protected theorem HasFDerivAtFilter.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L) (hx : f x = x) (n : ℕ) :
    HasFDerivAtFilter f^[n] (f' ^ n) x L := by
  induction n with
  | zero => exact hasFDerivAtFilter_id x L
  | succ n ihn =>
    rw [Function.iterate_succ, pow_succ]
    rw [← hx] at ihn
    exact ihn.comp x hf hL

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

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function with Fréchet derivative $f'$ at $x \in E$ along a filter $L$. If $f$ maps $L$ to itself (i.e., $\text{tendsto}\, f\, L\, L$) and $f(x) = x$, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ has Fréchet derivative $(f')^n$ at $x$ along $L$.

HasFDerivAt.iterate theorem

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

Full source

@[fun_prop]
protected theorem HasFDerivAt.iterate {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivAt f f' x)
    (hx : f x = x) (n : ℕ) : HasFDerivAt f^[n] (f' ^ n) x := by
  refine HasFDerivAtFilter.iterate hf ?_ hx n
  convert hf.continuousAt.tendsto
  exact hx.symm

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

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function that is Fréchet differentiable at $x \in E$ with derivative $f'$. If $f(x) = x$, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is Fréchet differentiable at $x$ with derivative $(f')^n$.

HasFDerivWithinAt.iterate theorem

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

Full source

@[fun_prop]
protected theorem HasFDerivWithinAt.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasFDerivWithinAt f f' s x) (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) :
    HasFDerivWithinAt f^[n] (f' ^ n) s x := by
  refine HasFDerivAtFilter.iterate hf ?_ hx n
  rw [nhdsWithin]
  convert tendsto_inf.2 ⟨hf.continuousWithinAt, _⟩
  exacts [hx.symm, (tendsto_principal_principal.2 hs).mono_left inf_le_right]

Fréchet Derivative of Iterated Function within a Set: $(f^{[n]})' = (f')^n$ at Fixed Point

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function with Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$. If $f(x) = x$ and $f$ maps $s$ into itself, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ has Fréchet derivative $(f')^n$ at $x$ within $s$.

HasStrictFDerivAt.iterate theorem

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

Full source

@[fun_prop]
protected theorem HasStrictFDerivAt.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasStrictFDerivAt f f' x) (hx : f x = x) (n : ℕ) :
    HasStrictFDerivAt f^[n] (f' ^ n) x := by
  induction n with
  | zero => exact hasStrictFDerivAt_id x
  | succ n ihn =>
    rw [Function.iterate_succ, pow_succ]
    rw [← hx] at ihn
    exact ihn.comp x hf

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

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function that has a strict Fréchet derivative $f'$ at $x \in E$. If $f(x) = x$, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ has a strict Fréchet derivative at $x$ given by the $n$-th power of $f'$, i.e., $(f')^n$.

DifferentiableAt.iterate theorem

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

Full source

@[fun_prop]
protected theorem DifferentiableAt.iterate {f : E → E} (hf : DifferentiableAt 𝕜 f x) (hx : f x = x)
    (n : ℕ) : DifferentiableAt 𝕜 f^[n] x :=
  (hf.hasFDerivAt.iterate hx n).differentiableAt

Differentiability of Iterated Function at Fixed Point

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function differentiable at $x \in E$. If $f(x) = x$, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is differentiable at $x$.

DifferentiableWithinAt.iterate theorem

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

Full source

@[fun_prop]
protected theorem DifferentiableWithinAt.iterate {f : E → E} (hf : DifferentiableWithinAt 𝕜 f s x)
    (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) : DifferentiableWithinAt 𝕜 f^[n] s x :=
  (hf.hasFDerivWithinAt.iterate hx hs n).differentiableWithinAt

Differentiability of Iterated Function at Fixed Point within a Set

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $f : E \to E$ be a function differentiable at $x \in E$ within a set $s \subseteq E$. If $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$.