doc-next-gen

Mathlib.Analysis.Calculus.FDeriv.Linear

Module docstring

{"# The derivative of bounded linear maps

For detailed documentation of the Fréchet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of bounded linear maps. ","### Continuous linear maps

There are currently two variants of these in mathlib, the bundled version (named ContinuousLinearMap, and denoted E →L[𝕜] F), and the unbundled version (with a predicate IsBoundedLinearMap). We give statements for both versions. "}

ContinuousLinearMap.hasStrictFDerivAt theorem
{x : E} : HasStrictFDerivAt e e x
Full source 
@[fun_prop]
protected theorem ContinuousLinearMap.hasStrictFDerivAt {x : E} : HasStrictFDerivAt e e x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by
    simp only [e.map_sub, sub_self, Pi.zero_apply]
Continuous linear maps are their own strict Fréchet derivatives
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then for any point $x \in E$, the map $e$ has itself as its strict Fréchet derivative at $x$. That is, the difference $e(y) - e(z) - e(y - z)$ is $o(\|y - z\|)$ as $y, z \to x$.
ContinuousLinearMap.hasFDerivAtFilter theorem
: HasFDerivAtFilter e e x L
Full source 
protected theorem ContinuousLinearMap.hasFDerivAtFilter : HasFDerivAtFilter e e x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by
    simp only [e.map_sub, sub_self, Pi.zero_apply]
Continuous linear maps are their own Fréchet derivatives
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then for any point $x \in E$ and any filter $L$ on $E$, the map $e$ has itself as its Fréchet derivative at $x$ along the filter $L$. That is, $e$ satisfies \[ e(x') = e(x) + e(x' - x) + o(\|x' - x\|) \] as $x'$ tends to $x$ along $L$.
ContinuousLinearMap.hasFDerivWithinAt theorem
: HasFDerivWithinAt e e s x
Full source 
@[fun_prop]
protected theorem ContinuousLinearMap.hasFDerivWithinAt : HasFDerivWithinAt e e s x :=
  e.hasFDerivAtFilter
Continuous linear maps are their own Fréchet derivatives within a set
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then for any point $x \in E$ and any subset $s \subseteq E$, the map $e$ has itself as its Fréchet derivative at $x$ within $s$. That is, $e$ satisfies \[ e(x') = e(x) + e(x' - x) + o(\|x' - x\|) \] as $x'$ tends to $x$ within $s$.
ContinuousLinearMap.hasFDerivAt theorem
: HasFDerivAt e e x
Full source 
@[fun_prop]
protected theorem ContinuousLinearMap.hasFDerivAt : HasFDerivAt e e x :=
  e.hasFDerivAtFilter
Continuous linear maps are their own Fréchet derivatives
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then for any point $x \in E$, the map $e$ has itself as its Fréchet derivative at $x$. That is, $e$ satisfies \[ e(x') = e(x) + e(x' - x) + o(\|x' - x\|) \] as $x'$ tends to $x$.
ContinuousLinearMap.differentiableAt theorem
: DifferentiableAt 𝕜 e x
Full source 
@[simp, fun_prop]
protected theorem ContinuousLinearMap.differentiableAt : DifferentiableAt 𝕜 e x :=
  e.hasFDerivAt.differentiableAt
Differentiability of Continuous Linear Maps
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then $e$ is differentiable at every point $x \in E$.
ContinuousLinearMap.differentiableWithinAt theorem
: DifferentiableWithinAt 𝕜 e s x
Full source 
@[fun_prop]
protected theorem ContinuousLinearMap.differentiableWithinAt : DifferentiableWithinAt 𝕜 e s x :=
  e.differentiableAt.differentiableWithinAt
Differentiability of Continuous Linear Maps Within Subsets
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then for any subset $s \subseteq E$ and any point $x \in E$, the map $e$ is differentiable at $x$ within $s$.
ContinuousLinearMap.fderiv theorem
: fderiv 𝕜 e x = e
Full source 
@[simp]
protected theorem ContinuousLinearMap.fderiv : fderiv 𝕜 e x = e :=
  e.hasFDerivAt.fderiv
Fréchet Derivative of a Continuous Linear Map is Itself
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then the Fréchet derivative of $e$ at any point $x \in E$ is equal to $e$ itself, i.e., $\text{fderiv}_{\mathbb{K}} e x = e$.
ContinuousLinearMap.fderivWithin theorem
(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 e s x = e
Full source 
protected theorem ContinuousLinearMap.fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 e s x = e := by
  rw [DifferentiableAt.fderivWithin e.differentiableAt hxs]
  exact e.fderiv
Fréchet Derivative Within a Set for Continuous Linear Maps is Itself
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. For any subset $s \subseteq E$ and any point $x \in E$ where $s$ is uniquely differentiable at $x$, the Fréchet derivative of $e$ at $x$ within $s$ equals $e$ itself, i.e., \[ \text{fderivWithin}_{\mathbb{K}} e s x = e. \]
ContinuousLinearMap.differentiable theorem
: Differentiable 𝕜 e
Full source 
@[simp, fun_prop]
protected theorem ContinuousLinearMap.differentiable : Differentiable 𝕜 e := fun _ =>
  e.differentiableAt
Differentiability of Continuous Linear Maps
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then $e$ is differentiable everywhere on $E$.
ContinuousLinearMap.differentiableOn theorem
: DifferentiableOn 𝕜 e s
Full source 
@[fun_prop]
protected theorem ContinuousLinearMap.differentiableOn : DifferentiableOn 𝕜 e s :=
  e.differentiable.differentiableOn
Differentiability of Continuous Linear Maps on Subsets
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \to F$ be a continuous linear map. Then $e$ is differentiable on any subset $s \subseteq E$.
IsBoundedLinearMap.hasFDerivAtFilter theorem
(h : IsBoundedLinearMap 𝕜 f) : HasFDerivAtFilter f h.toContinuousLinearMap x L
Full source 
theorem IsBoundedLinearMap.hasFDerivAtFilter (h : IsBoundedLinearMap 𝕜 f) :
    HasFDerivAtFilter f h.toContinuousLinearMap x L :=
  h.toContinuousLinearMap.hasFDerivAtFilter
Bounded linear maps are their own Fréchet derivatives along any filter
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then for any point $x \in E$ and any filter $L$ on $E$, the map $f$ has its associated continuous linear map as its Fréchet derivative at $x$ along the filter $L$. That is, $f$ satisfies \[ f(x') = f(x) + h.toContinuousLinearMap(x' - x) + o(\|x' - x\|) \] as $x'$ tends to $x$ along $L$, where $h$ is the proof that $f$ is a bounded linear map.
IsBoundedLinearMap.hasFDerivWithinAt theorem
(h : IsBoundedLinearMap 𝕜 f) : HasFDerivWithinAt f h.toContinuousLinearMap s x
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.hasFDerivWithinAt (h : IsBoundedLinearMap 𝕜 f) :
    HasFDerivWithinAt f h.toContinuousLinearMap s x :=
  h.hasFDerivAtFilter
Bounded linear maps are their own Fréchet derivatives within a set
Informal description
Let \( E \) and \( F \) be seminormed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a bounded linear map. Then for any point \( x \in E \) and any set \( s \subseteq E \), the map \( f \) has its associated continuous linear map as its Fréchet derivative at \( x \) within \( s \). That is, \( f \) satisfies \[ f(x') = f(x) + h.toContinuousLinearMap(x' - x) + o(\|x' - x\|) \] as \( x' \) tends to \( x \) within \( s \), where \( h \) is the proof that \( f \) is a bounded linear map.
IsBoundedLinearMap.hasFDerivAt theorem
(h : IsBoundedLinearMap 𝕜 f) : HasFDerivAt f h.toContinuousLinearMap x
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.hasFDerivAt (h : IsBoundedLinearMap 𝕜 f) :
    HasFDerivAt f h.toContinuousLinearMap x :=
  h.hasFDerivAtFilter
Bounded linear maps are their own Fréchet derivatives at a point
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then for any point $x \in E$, the map $f$ has its associated continuous linear map as its Fréchet derivative at $x$. That is, $f$ satisfies \[ f(x') = f(x) + h.toContinuousLinearMap(x' - x) + o(\|x' - x\|) \] as $x'$ tends to $x$, where $h$ is the proof that $f$ is a bounded linear map.
IsBoundedLinearMap.differentiableAt theorem
(h : IsBoundedLinearMap 𝕜 f) : DifferentiableAt 𝕜 f x
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.differentiableAt (h : IsBoundedLinearMap 𝕜 f) : DifferentiableAt 𝕜 f x :=
  h.hasFDerivAt.differentiableAt
Differentiability of Bounded Linear Maps at Every Point
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ is differentiable at every point $x \in E$.
IsBoundedLinearMap.differentiableWithinAt theorem
(h : IsBoundedLinearMap 𝕜 f) : DifferentiableWithinAt 𝕜 f s x
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.differentiableWithinAt (h : IsBoundedLinearMap 𝕜 f) :
    DifferentiableWithinAt 𝕜 f s x :=
  h.differentiableAt.differentiableWithinAt
Differentiability of Bounded Linear Maps Within Any Subset
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ is differentiable at every point $x \in E$ within any subset $s \subseteq E$.
IsBoundedLinearMap.fderiv theorem
(h : IsBoundedLinearMap 𝕜 f) : fderiv 𝕜 f x = h.toContinuousLinearMap
Full source 
theorem IsBoundedLinearMap.fderiv (h : IsBoundedLinearMap 𝕜 f) :
    fderiv 𝕜 f x = h.toContinuousLinearMap :=
  HasFDerivAt.fderiv h.hasFDerivAt
Fréchet Derivative of a Bounded Linear Map Equals Its Continuous Linear Map Representation
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then the Fréchet derivative of $f$ at any point $x \in E$ is equal to the continuous linear map associated to $f$.
IsBoundedLinearMap.fderivWithin theorem
(h : IsBoundedLinearMap 𝕜 f) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 f s x = h.toContinuousLinearMap
Full source 
theorem IsBoundedLinearMap.fderivWithin (h : IsBoundedLinearMap 𝕜 f)
    (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 f s x = h.toContinuousLinearMap := by
  rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]
  exact h.fderiv
Fréchet Derivative Within a Set for Bounded Linear Maps Equals Their Continuous Linear Map Representation
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. If the set $s \subseteq E$ is uniquely differentiable at $x \in E$ (i.e., the tangent cone at $x$ spans a dense subspace of $E$), then the Fréchet derivative of $f$ at $x$ within $s$ equals the continuous linear map associated to $f$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} f s x = h.toContinuousLinearMap. \]
IsBoundedLinearMap.differentiable theorem
(h : IsBoundedLinearMap 𝕜 f) : Differentiable 𝕜 f
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.differentiable (h : IsBoundedLinearMap 𝕜 f) : Differentiable 𝕜 f :=
  fun _ => h.differentiableAt
Differentiability of Bounded Linear Maps
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ is differentiable on $E$.
IsBoundedLinearMap.differentiableOn theorem
(h : IsBoundedLinearMap 𝕜 f) : DifferentiableOn 𝕜 f s
Full source 
@[fun_prop]
theorem IsBoundedLinearMap.differentiableOn (h : IsBoundedLinearMap 𝕜 f) : DifferentiableOn 𝕜 f s :=
  h.differentiable.differentiableOn
Differentiability of Bounded Linear Maps on Subsets
Informal description
Let $E$ and $F$ be seminormed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ is differentiable on any subset $s \subseteq E$.