Mathlib.Analysis.Calculus.FDeriv.RestrictScalars

Module docstring

{"# The derivative of the scalar restriction of a linear map

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 the scalar restriction of a linear map. ","### Restricting from ℂ to ℝ, or generally from 𝕜' to 𝕜

If a function is differentiable over ℂ, then it is differentiable over ℝ. In this paragraph, we give variants of this statement, in the general situation where ℂ and ℝ are replaced respectively by 𝕜' and 𝕜 where 𝕜' is a normed algebra over 𝕜. "}

HasStrictFDerivAt.restrictScalars theorem

(h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt f (f'.restrictScalars 𝕜) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.restrictScalars (h : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt f (f'.restrictScalars 𝕜) x :=
  .of_isLittleO h.isLittleO

Strict Fréchet Differentiability is Preserved Under Restriction of Scalars

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ has a strict Fréchet derivative $f' : E \toL[\mathbb{K}'] F$ at a point $x \in E$, then $f$ also has a strict Fréchet derivative at $x$ when considered as a map between normed spaces over $\mathbb{K}$, given by the restriction of scalars of $f'$ to $\mathbb{K}$.

HasFDerivAtFilter.restrictScalars theorem

{L} (h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter f (f'.restrictScalars 𝕜) x L

Full source

theorem HasFDerivAtFilter.restrictScalars {L} (h : HasFDerivAtFilter f f' x L) :
    HasFDerivAtFilter f (f'.restrictScalars 𝕜) x L :=
  .of_isLittleO h.isLittleO

Fréchet Derivative Preservation under Scalar Restriction

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}'$, and let $\mathbb{K}$ be a subfield of $\mathbb{K}'$ such that $\mathbb{K}'$ is a normed algebra over $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $f' : E \toL[\mathbb{K}'] F$ at $x \in E$ along the filter $L$. Then the scalar-restricted map $f$ also has a Fréchet derivative at $x$ along $L$ when viewed as a $\mathbb{K}$-linear map, given by the scalar restriction of $f'$ to $\mathbb{K}$.

HasFDerivAt.restrictScalars theorem

(h : HasFDerivAt f f' x) : HasFDerivAt f (f'.restrictScalars 𝕜) x

Full source

@[fun_prop]
theorem HasFDerivAt.restrictScalars (h : HasFDerivAt f f' x) :
    HasFDerivAt f (f'.restrictScalars 𝕜) x :=
  .of_isLittleO h.isLittleO

Fréchet Differentiability is Preserved Under Scalar Restriction

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ being a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ has a Fréchet derivative $f' : E \toL[\mathbb{K}'] F$ at a point $x \in E$, then $f$ also has a Fréchet derivative at $x$ when considered as a map between normed spaces over $\mathbb{K}$, given by the scalar restriction $f'.\text{restrictScalars}(\mathbb{K}) : E \toL[\mathbb{K}] F$.

HasFDerivWithinAt.restrictScalars theorem

(h : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt f (f'.restrictScalars 𝕜) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.restrictScalars (h : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt f (f'.restrictScalars 𝕜) s x :=
  .of_isLittleO h.isLittleO

Scalar restriction preserves Fréchet differentiability within a set

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ has Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$ as a $\mathbb{K}'$-linear map, then $f$ also has Fréchet derivative given by the scalar restriction of $f'$ to $\mathbb{K}$ at $x$ within $s$.

DifferentiableAt.restrictScalars theorem

(h : DifferentiableAt 𝕜' f x) : DifferentiableAt 𝕜 f x

Full source

@[fun_prop]
theorem DifferentiableAt.restrictScalars (h : DifferentiableAt 𝕜' f x) : DifferentiableAt 𝕜 f x :=
  (h.hasFDerivAt.restrictScalars 𝕜).differentiableAt

Differentiability is preserved under scalar restriction

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ is differentiable at a point $x \in E$ as a $\mathbb{K}'$-linear map, then $f$ is also differentiable at $x$ when considered as a $\mathbb{K}$-linear map.

DifferentiableWithinAt.restrictScalars theorem

(h : DifferentiableWithinAt 𝕜' f s x) : DifferentiableWithinAt 𝕜 f s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.restrictScalars (h : DifferentiableWithinAt 𝕜' f s x) :
    DifferentiableWithinAt 𝕜 f s x :=
  (h.hasFDerivWithinAt.restrictScalars 𝕜).differentiableWithinAt

Differentiability is preserved under scalar restriction within a set

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ is differentiable at a point $x \in E$ within a set $s \subseteq E$ as a $\mathbb{K}'$-linear map, then $f$ is also differentiable at $x$ within $s$ when considered as a $\mathbb{K}$-linear map.

DifferentiableOn.restrictScalars theorem

(h : DifferentiableOn 𝕜' f s) : DifferentiableOn 𝕜 f s

Full source

@[fun_prop]
theorem DifferentiableOn.restrictScalars (h : DifferentiableOn 𝕜' f s) : DifferentiableOn 𝕜 f s :=
  fun x hx => (h x hx).restrictScalars 𝕜

Differentiability on a set is preserved under scalar restriction

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ is differentiable on a set $s \subseteq E$ as a $\mathbb{K}'$-linear map, then $f$ is also differentiable on $s$ when considered as a $\mathbb{K}$-linear map.

Differentiable.restrictScalars theorem

(h : Differentiable 𝕜' f) : Differentiable 𝕜 f

Full source

@[fun_prop]
theorem Differentiable.restrictScalars (h : Differentiable 𝕜' f) : Differentiable 𝕜 f := fun x =>
  (h x).restrictScalars 𝕜

Differentiability is preserved under scalar restriction

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function. If $f$ is differentiable on $E$ as a $\mathbb{K}'$-linear map, then $f$ is also differentiable on $E$ when considered as a $\mathbb{K}$-linear map.

HasFDerivWithinAt.of_restrictScalars theorem

{g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x) (H : f'.restrictScalars 𝕜 = g') : HasFDerivWithinAt f f' s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x)
    (H : f'.restrictScalars 𝕜 = g') : HasFDerivWithinAt f f' s x := by
  rw [← H] at h
  exact .of_isLittleO h.isLittleO

Fréchet Derivative via Restriction of Scalars within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Suppose $f : E \to F$ has a Fréchet derivative $g' : E \toL[\mathbb{K}] F$ at $x \in E$ within a set $s \subseteq E$. If the restriction of scalars of $f' : E \toL[\mathbb{K}'] F$ to $\mathbb{K}$ equals $g'$, then $f$ has Fréchet derivative $f'$ at $x$ within $s$.

hasFDerivAt_of_restrictScalars theorem

{g' : E →L[𝕜] F} (h : HasFDerivAt f g' x) (H : f'.restrictScalars 𝕜 = g') : HasFDerivAt f f' x

Full source

@[fun_prop]
theorem hasFDerivAt_of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivAt f g' x)
    (H : f'.restrictScalars 𝕜 = g') : HasFDerivAt f f' x := by
  rw [← H] at h
  exact .of_isLittleO h.isLittleO

Fréchet Differentiability via Scalar Restriction

Informal description

Let $E$ and $F$ be normed spaces over a normed field $\mathbb{K}'$, where $\mathbb{K}'$ is a normed algebra over a subfield $\mathbb{K}$. Let $f : E \to F$ be a function and $x \in E$. Suppose $f$ has a Fréchet derivative $g' : E \toL[\mathbb{K}] F$ at $x$ (with respect to $\mathbb{K}$). If the restriction of scalars of $f' : E \toL[\mathbb{K}'] F$ to $\mathbb{K}$ equals $g'$, then $f$ has Fréchet derivative $f'$ at $x$ (with respect to $\mathbb{K}'$).

DifferentiableAt.fderiv_restrictScalars theorem

(h : DifferentiableAt 𝕜' f x) : fderiv 𝕜 f x = (fderiv 𝕜' f x).restrictScalars 𝕜

Full source

theorem DifferentiableAt.fderiv_restrictScalars (h : DifferentiableAt 𝕜' f x) :
    fderiv 𝕜 f x = (fderiv 𝕜' f x).restrictScalars 𝕜 :=
  (h.hasFDerivAt.restrictScalars 𝕜).fderiv

Fréchet Derivative Under Scalar Restriction: $\text{fderiv}_{\mathbb{K}} f x = (\text{fderiv}_{\mathbb{K}'} f x).\text{restrictScalars}(\mathbb{K})$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be nontrivially normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}'$, and let $f : E \to F$ be a function differentiable at a point $x \in E$ over $\mathbb{K}'$. Then the Fréchet derivative of $f$ at $x$ over $\mathbb{K}$ is equal to the restriction of scalars of the Fréchet derivative of $f$ at $x$ over $\mathbb{K}'$, i.e., \[ \text{fderiv}_{\mathbb{K}} f x = (\text{fderiv}_{\mathbb{K}'} f x).\text{restrictScalars}(\mathbb{K}). \]

differentiableWithinAt_iff_restrictScalars theorem

 (hf : DifferentiableWithinAt 𝕜 f s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
  DifferentiableWithinAt 𝕜' f s x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x

Full source

theorem differentiableWithinAt_iff_restrictScalars (hf : DifferentiableWithinAt 𝕜 f s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) : DifferentiableWithinAtDifferentiableWithinAt 𝕜' f s x ↔
      ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x := by
  constructor
  · rintro ⟨g', hg'⟩
    exact ⟨g', hs.eq (hg'.restrictScalars 𝕜) hf.hasFDerivWithinAt⟩
  · rintro ⟨f', hf'⟩
    exact ⟨f', hf.hasFDerivWithinAt.of_restrictScalars 𝕜 hf'⟩

Differentiability over $\mathbb{K}'$ via scalar restriction of the derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Let $f : E \to F$ be a function differentiable at a point $x \in E$ within a subset $s \subseteq E$, and assume $s$ is uniquely differentiable at $x$. Then $f$ is differentiable at $x$ within $s$ over $\mathbb{K}'$ if and only if there exists a continuous $\mathbb{K}'$-linear map $g' : E \to F$ whose restriction of scalars to $\mathbb{K}$ equals the Fréchet derivative of $f$ at $x$ within $s$ over $\mathbb{K}$.

differentiableAt_iff_restrictScalars theorem

 (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜' f x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderiv 𝕜 f x

Full source

theorem differentiableAt_iff_restrictScalars (hf : DifferentiableAt 𝕜 f x) :
    DifferentiableAtDifferentiableAt 𝕜' f x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderiv 𝕜 f x := by
  rw [← differentiableWithinAt_univ, ← fderivWithin_univ]
  exact
    differentiableWithinAt_iff_restrictScalars 𝕜 hf.differentiableWithinAt uniqueDiffWithinAt_univ

Differentiability over $\mathbb{K}'$ via scalar restriction of the derivative at a point

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be nontrivially normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ and $F$ be normed spaces over $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at $x \in E$ over $\mathbb{K}$. Then $f$ is differentiable at $x$ over $\mathbb{K}'$ if and only if there exists a continuous $\mathbb{K}'$-linear map $g' : E \to F$ whose restriction of scalars to $\mathbb{K}$ equals the Fréchet derivative of $f$ at $x$ over $\mathbb{K}$.