Mathlib.Analysis.Calculus.FDeriv.Equiv

ContinuousLinearEquiv.hasStrictFDerivAt theorem

: HasStrictFDerivAt iso (iso : E →L[𝕜] F) x

Full source

@[fun_prop]
protected theorem hasStrictFDerivAt : HasStrictFDerivAt iso (iso : E →L[𝕜] F) x :=
  iso.toContinuousLinearMap.hasStrictFDerivAt

Strict Differentiability of Continuous Linear Equivalences

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. Then, at any point $x \in E$, the map $\text{iso}$ is strictly differentiable, with its strict Fréchet derivative at $x$ being $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

ContinuousLinearEquiv.hasFDerivWithinAt theorem

: HasFDerivWithinAt iso (iso : E →L[𝕜] F) s x

Full source

@[fun_prop]
protected theorem hasFDerivWithinAt : HasFDerivWithinAt iso (iso : E →L[𝕜] F) s x :=
  iso.toContinuousLinearMap.hasFDerivWithinAt

Fréchet derivative of a continuous linear equivalence within a set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any point $x \in E$ and any set $s \subseteq E$ containing $x$, the map $\text{iso}$ has a Fréchet derivative within $s$ at $x$, and this derivative is equal to $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

ContinuousLinearEquiv.hasFDerivAt theorem

: HasFDerivAt iso (iso : E →L[𝕜] F) x

Full source

@[fun_prop]
protected theorem hasFDerivAt : HasFDerivAt iso (iso : E →L[𝕜] F) x :=
  iso.toContinuousLinearMap.hasFDerivAtFilter

Fréchet Derivative of a Continuous Linear Equivalence is Itself

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $x \in E$. For any continuous linear equivalence $\text{iso} : E \simeq_{\mathbb{K}} F$, the Fréchet derivative of $\text{iso}$ at $x$ exists and is equal to $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

ContinuousLinearEquiv.differentiableAt theorem

: DifferentiableAt 𝕜 iso x

Full source

@[fun_prop]
protected theorem differentiableAt : DifferentiableAt 𝕜 iso x :=
  iso.hasFDerivAt.differentiableAt

Differentiability of Continuous Linear Equivalences

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any point $x \in E$, the map $\text{iso}$ is differentiable at $x$.

ContinuousLinearEquiv.differentiableWithinAt theorem

: DifferentiableWithinAt 𝕜 iso s x

Full source

@[fun_prop]
protected theorem differentiableWithinAt : DifferentiableWithinAt 𝕜 iso s x :=
  iso.differentiableAt.differentiableWithinAt

Differentiability of Continuous Linear Equivalences within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any point $x \in E$ and any set $s \subseteq E$, the map $\text{iso}$ is differentiable within $s$ at $x$.

ContinuousLinearEquiv.fderiv theorem

: fderiv 𝕜 iso x = iso

Full source

protected theorem fderiv : fderiv 𝕜 iso x = iso :=
  iso.hasFDerivAt.fderiv

Fréchet Derivative of a Continuous Linear Equivalence is Itself

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For any continuous linear equivalence $\text{iso} : E \simeq F$ and any point $x \in E$, the Fréchet derivative of $\text{iso}$ at $x$ is equal to $\text{iso}$ itself, viewed as a continuous linear map from $E$ to $F$.

ContinuousLinearEquiv.fderivWithin theorem

(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 iso s x = iso

Full source

protected theorem fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 iso s x = iso :=
  iso.toContinuousLinearMap.fderivWithin hxs

Fréchet Derivative of a Continuous Linear Equivalence within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For a continuous linear equivalence $\text{iso} : E \simeq F$ and a point $x$ in $E$, if $x$ is uniquely differentiable within a set $s \subseteq E$, then the Fréchet derivative of $\text{iso}$ within $s$ at $x$ is equal to $\text{iso}$ itself, i.e., $D(\text{iso}|_s)(x) = \text{iso}$.

ContinuousLinearEquiv.differentiable theorem

: Differentiable 𝕜 iso

Full source

@[fun_prop]
protected theorem differentiable : Differentiable 𝕜 iso := fun _ => iso.differentiableAt

Differentiability of Continuous Linear Equivalences

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For any continuous linear equivalence $\text{iso} : E \simeq F$, the map $\text{iso}$ is differentiable everywhere on $E$.

ContinuousLinearEquiv.differentiableOn theorem

: DifferentiableOn 𝕜 iso s

Full source

@[fun_prop]
protected theorem differentiableOn : DifferentiableOn 𝕜 iso s :=
  iso.differentiable.differentiableOn

Differentiability of Continuous Linear Equivalences on Subsets

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For any continuous linear equivalence $\text{iso} : E \simeq F$ and any subset $s \subseteq E$, the map $\text{iso}$ is differentiable on $s$.

ContinuousLinearEquiv.comp_differentiableWithinAt_iff theorem

{f : G → E} {s : Set G} {x : G} : DifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x := by
  refine
    ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
  have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
  rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

Differentiability of Composition with Continuous Linear Equivalence iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$, a function $f \colon G \to E$, a subset $s \subseteq G$, and a point $x \in G$, the composition $\text{iso} \circ f$ is differentiable within $s$ at $x$ if and only if $f$ is differentiable within $s$ at $x$.

ContinuousLinearEquiv.comp_differentiableAt_iff theorem

{f : G → E} {x : G} : DifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

Full source

theorem comp_differentiableAt_iff {f : G → E} {x : G} :
    DifferentiableAtDifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x := by
  rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
    iso.comp_differentiableWithinAt_iff]

Differentiability of Composition with Continuous Linear Equivalence at a Point iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$, a function $f \colon G \to E$, and a point $x \in G$, the composition $\text{iso} \circ f$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

ContinuousLinearEquiv.comp_differentiableOn_iff theorem

{f : G → E} {s : Set G} : DifferentiableOn 𝕜 (iso ∘ f) s ↔ DifferentiableOn 𝕜 f s

Full source

theorem comp_differentiableOn_iff {f : G → E} {s : Set G} :
    DifferentiableOnDifferentiableOn 𝕜 (iso ∘ f) s ↔ DifferentiableOn 𝕜 f s := by
  rw [DifferentiableOn, DifferentiableOn]
  simp only [iso.comp_differentiableWithinAt_iff]

Differentiability of Composition with Continuous Linear Equivalence on a Subset iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$ and a function $f \colon G \to E$, the composition $\text{iso} \circ f$ is differentiable on a subset $s \subseteq G$ if and only if $f$ is differentiable on $s$.

ContinuousLinearEquiv.comp_differentiable_iff theorem

{f : G → E} : Differentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f

Full source

theorem comp_differentiable_iff {f : G → E} : DifferentiableDifferentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f := by
  rw [← differentiableOn_univ, ← differentiableOn_univ]
  exact iso.comp_differentiableOn_iff

Differentiability of Composition with Continuous Linear Equivalence iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$ and a function $f \colon G \to E$, the composition $\text{iso} \circ f$ is differentiable on $G$ if and only if $f$ is differentiable on $G$.

ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff theorem

 {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
  HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x

Full source

theorem comp_hasFDerivWithinAt_iff {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivWithinAtHasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x := by
  refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩
  have A : f = iso.symm ∘ iso ∘ f := by
    rw [← Function.comp_assoc, iso.symm_comp_self]
    rfl
  have B : f' = (iso.symm : F →L[𝕜] E).comp ((iso : E →L[𝕜] F).comp f') := by
    rw [← ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe, ContinuousLinearMap.id_comp]
  rw [A, B]
  exact iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H

Fréchet Differentiability of Composition with Continuous Linear Equivalence within a Subset

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a subset $s \subseteq G$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a Fréchet derivative within $s$ at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a Fréchet derivative within $s$ at $x$ equal to $f'$.

ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] E} :
  HasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x

Full source

theorem comp_hasStrictFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasStrictFDerivAtHasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x := by
  refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x H⟩
  convert iso.symm.hasStrictFDerivAt.comp x H using 1 <;>
    ext z <;> apply (iso.symm_apply_apply _).symm

Strict Differentiability of Composition with Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a strict Fréchet derivative at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a strict Fréchet derivative at $x$ equal to $f'$.

ContinuousLinearEquiv.comp_hasFDerivAt_iff theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] E} : HasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x

Full source

theorem comp_hasFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivAtHasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x := by
  simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff]

Fréchet Differentiability of Composition with Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a Fréchet derivative at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a Fréchet derivative at $x$ equal to $f'$.

ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff' theorem

 {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
  HasFDerivWithinAt (iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x

Full source

theorem comp_hasFDerivWithinAt_iff' {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivWithinAtHasFDerivWithinAt (iso ∘ f) f' s x ↔
      HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x := by
  rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_comp]

Fréchet Differentiability of Composition with Continuous Linear Equivalence within a Subset: $(\text{iso} \circ f)' = f' \leftrightarrow f' = \text{iso}^{-1} \circ (\text{iso} \circ f)'$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a subset $s \subseteq G$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} F$, the composition $\text{iso} \circ f$ has a Fréchet derivative within $s$ at $x$ equal to $f'$ if and only if $f$ has a Fréchet derivative within $s$ at $x$ equal to $\text{iso}^{-1} \circ f'$.

ContinuousLinearEquiv.comp_hasFDerivAt_iff' theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] F} : HasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x

Full source

theorem comp_hasFDerivAt_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivAtHasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x := by
  simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']

Fréchet Differentiability of Composition with Continuous Linear Equivalence: $(\text{iso} \circ f)' = f' \leftrightarrow f' = \text{iso}^{-1} \circ (\text{iso} \circ f)'$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} F$, the composition $\text{iso} \circ f$ has a Fréchet derivative at $x$ equal to $f'$ if and only if $f$ has a Fréchet derivative at $x$ equal to $\text{iso}^{-1} \circ f'$.

ContinuousLinearEquiv.comp_fderivWithin theorem

 {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x)

Full source

theorem comp_fderivWithin {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x) := by
  by_cases h : DifferentiableWithinAt 𝕜 f s x
  · rw [fderiv_comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]
  · have : ¬DifferentiableWithinAt 𝕜 (iso ∘ f) s x := mt iso.comp_differentiableWithinAt_iff.1 h
    rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.comp_zero]

Chain Rule for Fréchet Derivative of Composition with Continuous Linear Equivalence

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$, a function $f \colon G \to E$, a subset $s \subseteq G$, and a point $x \in G$ where $s$ is uniquely differentiable at $x$, the Fréchet derivative of the composition $\text{iso} \circ f$ within $s$ at $x$ is equal to the composition of $\text{iso}$ with the Fréchet derivative of $f$ within $s$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\text{iso} \circ f) s x = \text{iso} \circ (\text{fderiv}_{\mathbb{K}} f s x). \]

ContinuousLinearEquiv.comp_fderiv theorem

{f : G → E} {x : G} : fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x)

Full source

theorem comp_fderiv {f : G → E} {x : G} :
    fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) := by
  rw [← fderivWithin_univ, ← fderivWithin_univ]
  exact iso.comp_fderivWithin uniqueDiffWithinAt_univ

Chain Rule for Fréchet Derivative of Composition with Continuous Linear Equivalence

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a continuous linear equivalence $\text{iso} \colon E \simeq F$ and a function $f \colon G \to E$ that is differentiable at $x \in G$, the Fréchet derivative of the composition $\text{iso} \circ f$ at $x$ is equal to the composition of $\text{iso}$ with the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\text{iso} \circ f) x = \text{iso} \circ (\text{fderiv}_{\mathbb{K}} f x). \]

fderivWithin_continuousLinearEquiv_comp theorem

 (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) (hs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) s x =
    (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x)

Full source

lemma _root_.fderivWithin_continuousLinearEquiv_comp (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G))
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) s x =
      (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x) := by
  change fderivWithin 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x = _
  rw [ContinuousLinearEquiv.comp_fderivWithin _ hs]

Chain Rule for Fréchet Derivative of Composition with Continuous Linear Equivalence on a Subset

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$, $F$, $G$, and $G'$ be normed spaces over $\mathbb{K}$. Given a continuous linear equivalence $L \colon G \simeq G'$, a function $f \colon E \to (F \to G)$ (where $F \to G$ denotes continuous linear maps), and a point $x \in E$ where $f$ is differentiable within a set $s \subseteq E$ at $x$, the Fréchet derivative within $s$ of the function $x \mapsto L \circ f(x)$ at $x$ is equal to the composition of the continuous linear equivalence $(F \simeq F) \cong (G \simeq G')$ (induced by $L$) with the Fréchet derivative of $f$ within $s$ at $x$. In symbols: \[ \text{fderiv}_{\mathbb{K}} (x \mapsto L \circ f(x)) s x = ((\text{id}_F \cong L)) \circ \text{fderiv}_{\mathbb{K}} f s x. \]

fderiv_continuousLinearEquiv_comp theorem

 (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) (x : E) :
  fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) x = (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x)

Full source

lemma _root_.fderiv_continuousLinearEquiv_comp (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) (x : E) :
    fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) x =
      (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x) := by
  change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = _
  rw [ContinuousLinearEquiv.comp_fderiv]

Fréchet Derivative of Composition with Continuous Linear Equivalence

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$, $F$, $G$, and $G'$ be normed spaces over $\mathbb{K}$. Given a continuous linear equivalence $L \colon G \simeq_{\mathbb{K}} G'$ and a function $f \colon E \to (F \to_{\mathbb{K}} G)$ that is differentiable at $x \in E$, the Fréchet derivative of the function $x \mapsto L \circ f(x)$ at $x$ is equal to the composition of the continuous linear equivalence $(F \to_{\mathbb{K}} G) \simeq_{\mathbb{K}} (F \to_{\mathbb{K}} G')$ induced by $L$ with the Fréchet derivative of $f$ at $x$. In mathematical notation: \[ \text{fderiv}_{\mathbb{K}} (x \mapsto L \circ f(x)) \, x = ((\text{id}_{F \to_{\mathbb{K}} G}) \simeq_{\mathbb{K}} L) \circ \text{fderiv}_{\mathbb{K}} f \, x. \]

fderiv_continuousLinearEquiv_comp' theorem

 (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) :
  fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) = fun x ↦
    (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x)

Full source

lemma _root_.fderiv_continuousLinearEquiv_comp' (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) :
    fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) =
      fun x ↦ (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x) := by
  ext x : 1
  exact fderiv_continuousLinearEquiv_comp L f x

Fréchet Derivative of Composition with Continuous Linear Equivalence (Pointwise Form)

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$, $F$, $G$, and $G'$ be normed spaces over $\mathbb{K}$. Given a continuous linear equivalence $L \colon G \simeq_{\mathbb{K}} G'$ and a differentiable function $f \colon E \to (F \to_{\mathbb{K}} G)$, the Fréchet derivative of the function $x \mapsto L \circ f(x)$ is given by \[ \text{fderiv}_{\mathbb{K}} (x \mapsto L \circ f(x)) = \left( (\text{id}_{F \to_{\mathbb{K}} G}) \simeq_{\mathbb{K}} L \right) \circ \text{fderiv}_{\mathbb{K}} f, \] where the right-hand side is evaluated pointwise at each $x \in E$.

ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff theorem

 {f : F → G} {s : Set F} {x : E} :
  DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)

Full source

theorem comp_right_differentiableWithinAt_iff {f : F → G} {s : Set F} {x : E} :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x) := by
  refine ⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
  have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) := by
    rw [← iso.symm_apply_apply x] at H
    apply H.comp (iso x) iso.symm.differentiableWithinAt
    intro y hy
    simpa only [mem_preimage, apply_symm_apply] using hy
  rwa [Function.comp_assoc, iso.self_comp_symm] at this

Differentiability of Composition with Continuous Linear Equivalence: $f \circ \text{iso}$ Differentiable iff $f$ Differentiable

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : F \to G$ where $G$ is another normed space over $\mathbb{K}$, a point $x \in E$, and a subset $s \subseteq F$, the composition $f \circ \text{iso}$ is differentiable within the preimage $\text{iso}^{-1}(s)$ at $x$ if and only if $f$ is differentiable within $s$ at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_differentiableAt_iff theorem

{f : F → G} {x : E} : DifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x)

Full source

theorem comp_right_differentiableAt_iff {f : F → G} {x : E} :
    DifferentiableAtDifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x) := by
  simp only [← differentiableWithinAt_univ, ← iso.comp_right_differentiableWithinAt_iff,
    preimage_univ]

Differentiability of Composition with Continuous Linear Equivalence: $f \circ \text{iso}$ Differentiable iff $f$ Differentiable

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : F \to G$ where $G$ is another normed space over $\mathbb{K}$ and a point $x \in E$, the composition $f \circ \text{iso}$ is differentiable at $x$ if and only if $f$ is differentiable at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_differentiableOn_iff theorem

{f : F → G} {s : Set F} : DifferentiableOn 𝕜 (f ∘ iso) (iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s

Full source

theorem comp_right_differentiableOn_iff {f : F → G} {s : Set F} :
    DifferentiableOnDifferentiableOn 𝕜 (f ∘ iso) (iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s := by
  refine ⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
  rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]
  apply H
  simpa only [mem_preimage, apply_symm_apply] using hy

Differentiability of Composition with Continuous Linear Equivalence on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : F \to G$ where $G$ is another normed space over $\mathbb{K}$ and a subset $s \subseteq F$, the composition $f \circ \text{iso}$ is differentiable on the preimage $\text{iso}^{-1}(s)$ if and only if $f$ is differentiable on $s$.

ContinuousLinearEquiv.comp_right_differentiable_iff theorem

{f : F → G} : Differentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f

Full source

theorem comp_right_differentiable_iff {f : F → G} :
    DifferentiableDifferentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f := by
  simp only [← differentiableOn_univ, ← iso.comp_right_differentiableOn_iff, preimage_univ]

Differentiability of Composition with Continuous Linear Equivalence: $f \circ \text{iso}$ Differentiable iff $f$ Differentiable

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For any function $f : F \to G$ where $G$ is another normed space over $\mathbb{K}$, the composition $f \circ \text{iso}$ is differentiable on $E$ if and only if $f$ is differentiable on $F$.

ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff theorem

 {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :
  HasFDerivWithinAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) (iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)

Full source

theorem comp_right_hasFDerivWithinAt_iff {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :
    HasFDerivWithinAtHasFDerivWithinAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) (iso ⁻¹' s) x ↔
      HasFDerivWithinAt f f' s (iso x) := by
  refine ⟨fun H => ?_, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩
  rw [← iso.symm_apply_apply x] at H
  have A : f = (f ∘ iso) ∘ iso.symm := by
    rw [Function.comp_assoc, iso.self_comp_symm]
    rfl
  have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
  rw [A, B]
  apply H.comp (iso x) iso.symm.hasFDerivWithinAt
  intro y hy
  simpa only [mem_preimage, apply_symm_apply] using hy

Fréchet Derivative of Composition with Continuous Linear Equivalence within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For a function $f : F \to G$, a subset $s \subseteq F$, a point $x \in E$, and a continuous linear map $f' : F \to_{\mathbb{K}} G$, the following are equivalent: 1. The composition $f \circ \text{iso}$ has Fréchet derivative $f' \circ \text{iso}$ within the preimage $\text{iso}^{-1}(s)$ at $x$. 2. The function $f$ has Fréchet derivative $f'$ within $s$ at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_hasFDerivAt_iff theorem

 {f : F → G} {x : E} {f' : F →L[𝕜] G} : HasFDerivAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) x ↔ HasFDerivAt f f' (iso x)

Full source

theorem comp_right_hasFDerivAt_iff {f : F → G} {x : E} {f' : F →L[𝕜] G} :
    HasFDerivAtHasFDerivAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) x ↔ HasFDerivAt f f' (iso x) := by
  simp only [← hasFDerivWithinAt_univ, ← comp_right_hasFDerivWithinAt_iff, preimage_univ]

Fréchet Derivative of Composition with Continuous Linear Equivalence

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{SL} F$ be a continuous linear equivalence between $E$ and $F$. For a function $f : F \to G$, a point $x \in E$, and a continuous linear map $f' : F \to_{SL} G$, the composition $f \circ \text{iso}$ has Fréchet derivative $f' \circ \text{iso}$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff' theorem

 {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :
  HasFDerivWithinAt (f ∘ iso) f' (iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp (iso.symm : F →L[𝕜] E)) s (iso x)

Full source

theorem comp_right_hasFDerivWithinAt_iff' {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivWithinAtHasFDerivWithinAt (f ∘ iso) f' (iso ⁻¹' s) x ↔
      HasFDerivWithinAt f (f'.comp (iso.symm : F →L[𝕜] E)) s (iso x) := by
  rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]

Fréchet Derivative of Composition with Continuous Linear Equivalence (Variant)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For a function $f : F \to G$, a subset $s \subseteq F$, a point $x \in E$, and a continuous linear map $f' : E \to_{\mathbb{K}} G$, the following are equivalent: 1. The composition $f \circ \text{iso}$ has Fréchet derivative $f'$ within the preimage $\text{iso}^{-1}(s)$ at $x$. 2. The function $f$ has Fréchet derivative $f' \circ \text{iso}^{-1}$ within $s$ at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_hasFDerivAt_iff' theorem

 {f : F → G} {x : E} {f' : E →L[𝕜] G} :
  HasFDerivAt (f ∘ iso) f' x ↔ HasFDerivAt f (f'.comp (iso.symm : F →L[𝕜] E)) (iso x)

Full source

theorem comp_right_hasFDerivAt_iff' {f : F → G} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivAtHasFDerivAt (f ∘ iso) f' x ↔ HasFDerivAt f (f'.comp (iso.symm : F →L[𝕜] E)) (iso x) := by
  simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]

Fréchet Derivative of Composition with Continuous Linear Equivalence (Pointwise Variant)

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence. For a function $f : F \to G$, a point $x \in E$, and a continuous linear map $f' : E \to_{\mathbb{K}} G$, the following are equivalent: 1. The composition $f \circ \text{iso}$ has Fréchet derivative $f'$ at $x$. 2. The function $f$ has Fréchet derivative $f' \circ \text{iso}^{-1}$ at $\text{iso}(x)$.

ContinuousLinearEquiv.comp_right_fderivWithin theorem

 {f : F → G} {s : Set F} {x : E} (hxs : UniqueDiffWithinAt 𝕜 (iso ⁻¹' s) x) :
  fderivWithin 𝕜 (f ∘ iso) (iso ⁻¹' s) x = (fderivWithin 𝕜 f s (iso x)).comp (iso : E →L[𝕜] F)

Full source

theorem comp_right_fderivWithin {f : F → G} {s : Set F} {x : E}
    (hxs : UniqueDiffWithinAt 𝕜 (iso ⁻¹' s) x) :
    fderivWithin 𝕜 (f ∘ iso) (iso ⁻¹' s) x =
      (fderivWithin 𝕜 f s (iso x)).comp (iso : E →L[𝕜] F) := by
  by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
  · exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs
  · have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x := by
      intro h'
      exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
    rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]

Chain Rule for Fréchet Derivative of Composition with Continuous Linear Equivalence within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence between $E$ and $F$. For a function $f : F \to G$, a subset $s \subseteq F$, and a point $x \in E$ such that $\text{iso}^{-1}(s)$ is uniquely differentiable at $x$, the Fréchet derivative of the composition $f \circ \text{iso}$ within $\text{iso}^{-1}(s)$ at $x$ is equal to the composition of the Fréchet derivative of $f$ within $s$ at $\text{iso}(x)$ with $\text{iso}$ as a continuous linear map. That is: $$ D(f \circ \text{iso})_{\text{iso}^{-1}(s)}(x) = Df_s(\text{iso}(x)) \circ \text{iso} $$

ContinuousLinearEquiv.comp_right_fderiv theorem

{f : F → G} {x : E} : fderiv 𝕜 (f ∘ iso) x = (fderiv 𝕜 f (iso x)).comp (iso : E →L[𝕜] F)

Full source

theorem comp_right_fderiv {f : F → G} {x : E} :
    fderiv 𝕜 (f ∘ iso) x = (fderiv 𝕜 f (iso x)).comp (iso : E →L[𝕜] F) := by
  rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]
  exact uniqueDiffWithinAt_univ

Chain Rule for Fréchet Derivative of Composition with Continuous Linear Equivalence

Informal description

Let $E$, $F$, and $G$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a continuous linear equivalence. For any function $f : F \to G$ and any point $x \in E$, the Fréchet derivative of the composition $f \circ \text{iso}$ at $x$ is equal to the composition of the Fréchet derivative of $f$ at $\text{iso}(x)$ with $\text{iso}$ as a continuous linear map. That is: $$ D(f \circ \text{iso})(x) = Df(\text{iso}(x)) \circ \text{iso} $$

LinearIsometryEquiv.hasStrictFDerivAt theorem

: HasStrictFDerivAt iso (iso : E →L[𝕜] F) x

Full source

@[fun_prop]
protected theorem hasStrictFDerivAt : HasStrictFDerivAt iso (iso : E →L[𝕜] F) x :=
  (iso : E ≃L[𝕜] F).hasStrictFDerivAt

Strict Fréchet Differentiability of Linear Isometric Equivalences

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a linear isometric equivalence between $E$ and $F$. Then, at any point $x \in E$, the map $\text{iso}$ is strictly Fréchet differentiable, with its strict Fréchet derivative at $x$ being $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

LinearIsometryEquiv.hasFDerivWithinAt theorem

: HasFDerivWithinAt iso (iso : E →L[𝕜] F) s x

Full source

@[fun_prop]
protected theorem hasFDerivWithinAt : HasFDerivWithinAt iso (iso : E →L[𝕜] F) s x :=
  (iso : E ≃L[𝕜] F).hasFDerivWithinAt

Fréchet Derivative of a Linear Isometric Equivalence Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a linear isometric equivalence between $E$ and $F$. For any point $x \in E$ and any set $s \subseteq E$ containing $x$, the map $\text{iso}$ has a Fréchet derivative within $s$ at $x$, and this derivative is equal to $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

LinearIsometryEquiv.hasFDerivAt theorem

: HasFDerivAt iso (iso : E →L[𝕜] F) x

Full source

@[fun_prop]
protected theorem hasFDerivAt : HasFDerivAt iso (iso : E →L[𝕜] F) x :=
  (iso : E ≃L[𝕜] F).hasFDerivAt

Fréchet Derivative of a Linear Isometric Equivalence is Itself

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a linear isometric equivalence between $E$ and $F$. Then, at any point $x \in E$, the map $\text{iso}$ is Fréchet differentiable, with its Fréchet derivative at $x$ being $\text{iso}$ itself (viewed as a continuous linear map from $E$ to $F$).

LinearIsometryEquiv.differentiableAt theorem

: DifferentiableAt 𝕜 iso x

Full source

@[fun_prop]
protected theorem differentiableAt : DifferentiableAt 𝕜 iso x :=
  iso.hasFDerivAt.differentiableAt

Differentiability of Linear Isometric Equivalences

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a linear isometric equivalence between $E$ and $F$. Then, for any point $x \in E$, the map $\text{iso}$ is differentiable at $x$.

LinearIsometryEquiv.differentiableWithinAt theorem

: DifferentiableWithinAt 𝕜 iso s x

Full source

@[fun_prop]
protected theorem differentiableWithinAt : DifferentiableWithinAt 𝕜 iso s x :=
  iso.differentiableAt.differentiableWithinAt

Differentiability of Linear Isometric Equivalence within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $\text{iso} : E \simeq F$ be a linear isometric equivalence. For any point $x \in E$ and any subset $s \subseteq E$, the map $\text{iso}$ is differentiable within $s$ at $x$.

LinearIsometryEquiv.fderiv theorem

: fderiv 𝕜 iso x = iso

Full source

protected theorem fderiv : fderiv 𝕜 iso x = iso :=
  iso.hasFDerivAt.fderiv

Fréchet Derivative of a Linear Isometric Equivalence is Itself

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $\text{iso} : E \simeq F$ be a linear isometric equivalence. For any point $x \in E$, the Fréchet derivative of $\text{iso}$ at $x$ is equal to $\text{iso}$ itself, i.e., $D\text{iso}(x) = \text{iso}$.

LinearIsometryEquiv.fderivWithin theorem

(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 iso s x = iso

Full source

protected theorem fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 iso s x = iso :=
  (iso : E ≃L[𝕜] F).fderivWithin hxs

Fréchet Derivative of Linear Isometric Equivalence within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $\text{iso} : E \simeq F$ be a linear isometric equivalence. For a point $x \in E$ and a set $s \subseteq E$, if $x$ is uniquely differentiable within $s$, then the Fréchet derivative of $\text{iso}$ within $s$ at $x$ equals $\text{iso}$ itself, i.e., $D(\text{iso}|_s)(x) = \text{iso}$.

LinearIsometryEquiv.differentiable theorem

: Differentiable 𝕜 iso

Full source

@[fun_prop]
protected theorem differentiable : Differentiable 𝕜 iso := fun _ => iso.differentiableAt

Every Linear Isometric Equivalence is Differentiable

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For any linear isometric equivalence $\text{iso} \colon E \simeq F$, the map $\text{iso}$ is differentiable everywhere on $E$.

LinearIsometryEquiv.differentiableOn theorem

: DifferentiableOn 𝕜 iso s

Full source

@[fun_prop]
protected theorem differentiableOn : DifferentiableOn 𝕜 iso s :=
  iso.differentiable.differentiableOn

Differentiability of Linear Isometric Equivalence on a Subset

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For any linear isometric equivalence $\text{iso} \colon E \simeq F$ and any subset $s \subseteq E$, the map $\text{iso}$ is differentiable on $s$.

LinearIsometryEquiv.comp_differentiableWithinAt_iff theorem

{f : G → E} {s : Set G} {x : G} : DifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  (iso : E ≃L[𝕜] F).comp_differentiableWithinAt_iff

Differentiability of Composition with Semilinear Isometric Equivalence iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a semilinear isometric equivalence $\text{iso} \colon E \simeq F$, a function $f \colon G \to E$, a subset $s \subseteq G$, and a point $x \in G$, the composition $\text{iso} \circ f$ is differentiable within $s$ at $x$ if and only if $f$ is differentiable within $s$ at $x$.

LinearIsometryEquiv.comp_differentiableAt_iff theorem

{f : G → E} {x : G} : DifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

Full source

theorem comp_differentiableAt_iff {f : G → E} {x : G} :
    DifferentiableAtDifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x :=
  (iso : E ≃L[𝕜] F).comp_differentiableAt_iff

Differentiability of Composition with Semilinear Isometric Equivalence at a Point iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a semilinear isometric equivalence $\text{iso} \colon E \simeq F$, a function $f \colon G \to E$, and a point $x \in G$, the composition $\text{iso} \circ f$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

LinearIsometryEquiv.comp_differentiableOn_iff theorem

{f : G → E} {s : Set G} : DifferentiableOn 𝕜 (iso ∘ f) s ↔ DifferentiableOn 𝕜 f s

Full source

theorem comp_differentiableOn_iff {f : G → E} {s : Set G} :
    DifferentiableOnDifferentiableOn 𝕜 (iso ∘ f) s ↔ DifferentiableOn 𝕜 f s :=
  (iso : E ≃L[𝕜] F).comp_differentiableOn_iff

Differentiability of Composition with Semilinear Isometric Equivalence on a Subset iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a semilinear isometric equivalence $\text{iso} \colon E \simeq F$ and a function $f \colon G \to E$, the composition $\text{iso} \circ f$ is differentiable on a subset $s \subseteq G$ if and only if $f$ is differentiable on $s$.

LinearIsometryEquiv.comp_differentiable_iff theorem

{f : G → E} : Differentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f

Full source

theorem comp_differentiable_iff {f : G → E} : DifferentiableDifferentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f :=
  (iso : E ≃L[𝕜] F).comp_differentiable_iff

Differentiability of Composition with Linear Isometric Equivalence iff Differentiability of Original Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a semilinear isometric equivalence $\text{iso} \colon E \simeq F$ and a function $f \colon G \to E$, the composition $\text{iso} \circ f$ is differentiable on $G$ if and only if $f$ is differentiable on $G$.

LinearIsometryEquiv.comp_hasFDerivWithinAt_iff theorem

 {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
  HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x

Full source

theorem comp_hasFDerivWithinAt_iff {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivWithinAtHasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivWithinAt_iff

Fréchet Differentiability of Composition with Linear Isometric Equivalence within a Subset

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \simeq_{\mathbb{K}} F$ be a linear isometric equivalence between $E$ and $F$. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a subset $s \subseteq G$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a Fréchet derivative within $s$ at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a Fréchet derivative within $s$ at $x$ equal to $f'$.

LinearIsometryEquiv.comp_hasStrictFDerivAt_iff theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] E} :
  HasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x

Full source

theorem comp_hasStrictFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasStrictFDerivAtHasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x :=
  (iso : E ≃L[𝕜] F).comp_hasStrictFDerivAt_iff

Strict Differentiability of Composition with Linear Isometric Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \to F$ be a linear isometric equivalence. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a strict Fréchet derivative at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a strict Fréchet derivative at $x$ equal to $f'$.

LinearIsometryEquiv.comp_hasFDerivAt_iff theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] E} : HasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x

Full source

theorem comp_hasFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivAtHasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff

Fréchet Differentiability of Composition with Linear Isometric Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \to F$ be a linear isometric equivalence. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} E$, the composition $\text{iso} \circ f$ has a Fréchet derivative at $x$ equal to $\text{iso} \circ f'$ if and only if $f$ has a Fréchet derivative at $x$ equal to $f'$.

LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' theorem

 {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
  HasFDerivWithinAt (iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x

Full source

theorem comp_hasFDerivWithinAt_iff' {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivWithinAtHasFDerivWithinAt (iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivWithinAt_iff'

Fréchet Differentiability of Composition with Linear Isometric Equivalence within a Subset: $(\text{iso} \circ f)' = f' \leftrightarrow f' = \text{iso}^{-1} \circ (\text{iso} \circ f)'$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \to F$ be a linear isometric equivalence. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a subset $s \subseteq G$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} F$, the composition $\text{iso} \circ f$ has a Fréchet derivative within $s$ at $x$ equal to $f'$ if and only if $f$ has a Fréchet derivative within $s$ at $x$ equal to $\text{iso}^{-1} \circ f'$.

LinearIsometryEquiv.comp_hasFDerivAt_iff' theorem

 {f : G → E} {x : G} {f' : G →L[𝕜] F} : HasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x

Full source

theorem comp_hasFDerivAt_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivAtHasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff'

Fréchet Differentiability of Composition with Linear Isometric Equivalence: $(\text{iso} \circ f)' = f' \leftrightarrow f' = \text{iso}^{-1} \circ (\text{iso} \circ f)'$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\text{iso} : E \to F$ be a linear isometric equivalence. For any function $f : G \to E$ defined on a normed space $G$ over $\mathbb{K}$, a point $x \in G$, and a continuous linear map $f' : G \to_{\mathbb{K}} F$, the composition $\text{iso} \circ f$ has a Fréchet derivative at $x$ equal to $f'$ if and only if $f$ has a Fréchet derivative at $x$ equal to $\text{iso}^{-1} \circ f'$.

LinearIsometryEquiv.comp_fderivWithin theorem

 {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x)

Full source

theorem comp_fderivWithin {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x) :=
  (iso : E ≃L[𝕜] F).comp_fderivWithin hxs

Chain Rule for Fréchet Derivative of Composition with Linear Isometric Equivalence within a Subset

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a linear isometric equivalence $\text{iso} \colon E \to F$, a function $f \colon G \to E$, a subset $s \subseteq G$, and a point $x \in G$ where $s$ is uniquely differentiable at $x$, the Fréchet derivative of the composition $\text{iso} \circ f$ within $s$ at $x$ is equal to the composition of $\text{iso}$ with the Fréchet derivative of $f$ within $s$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\text{iso} \circ f) s x = \text{iso} \circ (\text{fderiv}_{\mathbb{K}} f s x). \]

LinearIsometryEquiv.comp_fderiv theorem

{f : G → E} {x : G} : fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x)

Full source

theorem comp_fderiv {f : G → E} {x : G} :
    fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) :=
  (iso : E ≃L[𝕜] F).comp_fderiv

Chain Rule for Fréchet Derivative of Composition with Linear Isometric Equivalence

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a linear isometric equivalence $\text{iso} \colon E \to F$ and a function $f \colon G \to E$ that is differentiable at $x \in G$, the Fréchet derivative of the composition $\text{iso} \circ f$ at $x$ is equal to the composition of $\text{iso}$ with the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\text{iso} \circ f) x = \text{iso} \circ (\text{fderiv}_{\mathbb{K}} f x). \]

LinearIsometryEquiv.comp_fderiv' theorem

{f : G → E} : fderiv 𝕜 (iso ∘ f) = fun x ↦ (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x)

Full source

theorem comp_fderiv' {f : G → E} :
    fderiv 𝕜 (iso ∘ f) = fun x ↦ (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) := by
  ext x : 1
  exact LinearIsometryEquiv.comp_fderiv iso

Chain Rule for Fréchet Derivative of Composition with Linear Isometric Equivalence (Pointwise Version)

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $G$ be a normed additive commutative group. Given a linear isometric equivalence $\text{iso} \colon E \to F$ and a differentiable function $f \colon G \to E$, the Fréchet derivative of the composition $\text{iso} \circ f$ at any point $x \in G$ is equal to the composition of $\text{iso}$ with the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\text{iso} \circ f) = \lambda x, \text{iso} \circ (\text{fderiv}_{\mathbb{K}} f x). \]

HasFDerivWithinAt.of_local_left_inverse theorem

 {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F} (hg : Tendsto g (𝓝[t] a) (𝓝[s] (g a)))
  (hf : HasFDerivWithinAt f (f' : E →L[𝕜] F) s (g a)) (ha : a ∈ t) (hfg : ∀ᶠ y in 𝓝[t] a, f (g y) = y) :
  HasFDerivWithinAt g (f'.symm : F →L[𝕜] E) t a

Full source

/-- If `f (g y) = y` for `y` in a neighborhood of `a` within `t`,
`g` maps a neighborhood of `a` within `t` to a neighborhood of `g a` within `s`,
and `f` has an invertible derivative `f'` at `g a` within `s`,
then `g` has the derivative `f'⁻¹` at `a` within `t`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function. -/
theorem HasFDerivWithinAt.of_local_left_inverse {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F}
    (hg : Tendsto g (𝓝[t] a) (𝓝[s] (g a))) (hf : HasFDerivWithinAt f (f' : E →L[𝕜] F) s (g a))
    (ha : a ∈ t) (hfg : ∀ᶠ y in 𝓝[t] a, f (g y) = y) :
    HasFDerivWithinAt g (f'.symm : F →L[𝕜] E) t a := by
  have : (fun x : F => g x - g a - f'.symm (x - a)) =O[𝓝[t] a]
      fun x : F => f' (g x - g a) - (x - a) :=
    ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x ↦ by simp) fun _ ↦ rfl
  refine .of_isLittleO <| this.trans_isLittleO ?_
  clear this
  refine ((hf.isLittleO.comp_tendsto hg).symm.congr' (hfg.mono ?_) .rfl).trans_isBigO ?_
  · intro p hp
    simp [hp, hfg.self_of_nhdsWithin ha]
  · refine ((hf.isBigO_sub_rev f'.antilipschitz).comp_tendsto hg).congr'
      (Eventually.of_forall fun _ => rfl) (hfg.mono ?_)
    rintro p hp
    simp only [(· ∘ ·), hp, hfg.self_of_nhdsWithin ha]

Inverse Function Theorem for Local Left Inverse with Fréchet Derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ and $t \subseteq F$ be subsets. Suppose $g \colon F \to E$ is a function such that: 1. $g$ maps a neighborhood of $a$ within $t$ to a neighborhood of $g(a)$ within $s$, 2. $f \colon E \to F$ has a Fréchet derivative $f' \colon E \simeq_{\text{SL}[\mathbb{K}]} F$ at $g(a)$ within $s$, 3. $a \in t$, 4. $f(g(y)) = y$ for all $y$ in some neighborhood of $a$ within $t$. Then $g$ has the Fréchet derivative $f'^{-1}$ at $a$ within $t$.

HasStrictFDerivAt.of_local_left_inverse theorem

 {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a)
  (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) (g a)) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) :
  HasStrictFDerivAt g (f'.symm : F →L[𝕜] E) a

Full source

/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a`
in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function. -/
theorem HasStrictFDerivAt.of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F}
    (hg : ContinuousAt g a) (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) (g a))
    (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasStrictFDerivAt g (f'.symm : F →L[𝕜] E) a := by
  replace hg := hg.prodMap' hg
  replace hfg := hfg.prodMk_nhds hfg
  have :
    (fun p : F × F => g p.1 - g p.2 - f'.symm (p.1 - p.2)) =O[𝓝 (a, a)] fun p : F × F =>
      f' (g p.1 - g p.2) - (p.1 - p.2) := by
    refine ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => ?_) fun _ => rfl
    simp
  refine .of_isLittleO <| this.trans_isLittleO ?_
  clear this
  refine ((hf.isLittleO.comp_tendsto hg).symm.congr'
    (hfg.mono ?_) (Eventually.of_forall fun _ => rfl)).trans_isBigO ?_
  · rintro p ⟨hp1, hp2⟩
    simp [hp1, hp2]
  · refine (hf.isBigO_sub_rev.comp_tendsto hg).congr' (Eventually.of_forall fun _ => rfl)
      (hfg.mono ?_)
    rintro p ⟨hp1, hp2⟩
    simp only [(· ∘ ·), hp1, hp2, Prod.map]

Strict Differentiability of Local Inverse via Invertible Derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f \colon E \to F$ and $g \colon F \to E$ be functions. Suppose that: 1. $g$ is continuous at a point $a \in F$, 2. $f$ has a strict Fréchet derivative at $g(a)$, given by an invertible continuous linear equivalence $f' \colon E \simeq_{\mathbb{K}} F$, 3. There exists a neighborhood of $a$ such that for all $y$ in this neighborhood, $f(g(y)) = y$. Then $g$ has a strict Fréchet derivative at $a$, and it is equal to the inverse of $f'$, i.e., $g'(a) = (f')^{-1} \colon F \to_{\mathbb{K}} E$.

HasFDerivAt.of_local_left_inverse theorem

 {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasFDerivAt f (f' : E →L[𝕜] F) (g a))
  (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasFDerivAt g (f'.symm : F →L[𝕜] E) a

Full source

/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem HasFDerivAt.of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F}
    (hg : ContinuousAt g a) (hf : HasFDerivAt f (f' : E →L[𝕜] F) (g a))
    (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasFDerivAt g (f'.symm : F →L[𝕜] E) a := by
  simp only [← hasFDerivWithinAt_univ, ← nhdsWithin_univ] at hf hfg ⊢
  exact hf.of_local_left_inverse (.inf hg (by simp)) (mem_univ _) hfg

Fréchet Derivative of Local Left Inverse via Invertible Derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Let $f \colon E \to F$ and $g \colon F \to E$ be functions, and let $a \in F$. Suppose that: 1. $g$ is continuous at $a$, 2. $f$ has a Fréchet derivative at $g(a)$, given by an invertible continuous linear equivalence $f' \colon E \simeq_{\mathbb{K}} F$, 3. There exists a neighborhood of $a$ such that for all $y$ in this neighborhood, $f(g(y)) = y$. Then $g$ has a Fréchet derivative at $a$, and it is equal to the inverse of $f'$, i.e., $g'(a) = (f')^{-1} \colon F \to_{\mathbb{K}} E$.

PartialHomeomorph.hasStrictFDerivAt_symm theorem

 (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
  (htff' : HasStrictFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) : HasStrictFDerivAt f.symm (f'.symm : F →L[𝕜] E) a

Full source

/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` in the sense of strict differentiability at `f.symm a`, then `f.symm` has
the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem PartialHomeomorph.hasStrictFDerivAt_symm (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F}
    {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) :
    HasStrictFDerivAt f.symm (f'.symm : F →L[𝕜] E) a :=
  htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)

Strict Differentiability of Inverse Partial Homeomorphism via Invertible Derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f$ be a partial homeomorphism between $E$ and $F$. Suppose that: 1. $a$ is a point in the target of $f$ (i.e., $a \in f.\text{target}$), 2. $f$ has a strict Fréchet derivative at $f^{-1}(a)$, given by an invertible continuous linear equivalence $f' : E \simeq_{\mathbb{K}} F$. Then the inverse function $f^{-1}$ has a strict Fréchet derivative at $a$, and it is equal to the inverse of $f'$, i.e., $(f^{-1})'(a) = (f')^{-1} : F \to_{\mathbb{K}} E$.

PartialHomeomorph.hasFDerivAt_symm theorem

 (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
  (htff' : HasFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) : HasFDerivAt f.symm (f'.symm : F →L[𝕜] E) a

Full source

/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem PartialHomeomorph.hasFDerivAt_symm (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F}
    (ha : a ∈ f.target) (htff' : HasFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) :
    HasFDerivAt f.symm (f'.symm : F →L[𝕜] E) a :=
  htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)

Fréchet derivative of the inverse of a partial homeomorphism via invertible derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f$ be a partial homeomorphism between $E$ and $F$. Suppose that: 1. $a$ is a point in the target of $f$ (i.e., $a \in f.\text{target}$), 2. $f$ has a Fréchet derivative at $f^{-1}(a)$, given by an invertible continuous linear equivalence $f' : E \simeq_{\mathbb{K}} F$. Then the inverse function $f^{-1}$ has a Fréchet derivative at $a$, and it is equal to the inverse of $f'$, i.e., $(f^{-1})'(a) = (f')^{-1} : F \to_{\mathbb{K}} E$.

HasFDerivWithinAt.eventually_ne theorem

 (h : HasFDerivWithinAt f f' s x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) : ∀ᶠ z in 𝓝[s \ { x }] x, f z ≠ c

Full source

theorem HasFDerivWithinAt.eventually_ne (h : HasFDerivWithinAt f f' s x)
    (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) : ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ c := by
  rcases eq_or_ne (f x) c with rfl | hc
  · rw [nhdsWithin, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal]
    have A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x) :=
      isBigO_iff.2 <| hf'.imp fun C hC => Eventually.of_forall fun z => hC _
    have : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x) := h.isLittleO.trans_isBigO A
    simpa [not_imp_not, sub_eq_zero] using (A.trans this.isBigO_symm).eq_zero_imp
  · exact (h.continuousWithinAt.eventually_ne hc).filter_mono <| by gcongr; apply diff_subset

Eventual distinctness of function values near a point with Fréchet derivative

Informal description

Let $E$ and $F$ be normed spaces, $f : E \to F$ a function, $s \subseteq E$ a subset, and $x \in E$. If $f$ has a Fréchet derivative $f'$ within $s$ at $x$, and there exists a constant $C > 0$ such that $\|z\| \leq C \|f'(z)\|$ for all $z \in E$, then for all $z$ in a punctured neighborhood of $x$ within $s$, $f(z) \neq c$.

HasFDerivAt.eventually_ne theorem

(h : HasFDerivAt f f' x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) : ∀ᶠ z in 𝓝[≠] x, f z ≠ c

Full source

theorem HasFDerivAt.eventually_ne (h : HasFDerivAt f f' x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) :
    ∀ᶠ z in 𝓝[≠] x, f z ≠ c := by
  simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_ne hf'

Eventual Distinctness of Function Values Near a Differentiable Point

Informal description

Let $E$ and $F$ be normed spaces, $f : E \to F$ a function, and $x \in E$. If $f$ has a Fréchet derivative $f'$ at $x$, and there exists a constant $C > 0$ such that $\|z\| \leq C \|f'(z)\|$ for all $z \in E$, then for all $z$ in a punctured neighborhood of $x$, $f(z) \neq c$.

has_fderiv_at_filter_real_equiv theorem

 {L : Filter E} :
  Tendsto (fun x' : E => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
    Tendsto (fun x' : E => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)

Full source

theorem has_fderiv_at_filter_real_equiv {L : Filter E} :
    TendstoTendsto (fun x' : E => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
      Tendsto (fun x' : E => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) := by
  symm
  rw [tendsto_iff_norm_sub_tendsto_zero]
  refine tendsto_congr fun x' => ?_
  simp [norm_smul]

Equivalence of Fréchet Derivative Conditions in Normed Spaces

Informal description

Let $E$ be a normed space, $f : E \to F$ a function between normed spaces, $x \in E$, and $f' : E \to F$ a continuous linear map. For any filter $L$ on $E$, the following are equivalent: 1. The limit $\lim_{x' \to_L x} \frac{\|f(x') - f(x) - f'(x' - x)\|}{\|x' - x\|} = 0$; 2. The limit $\lim_{x' \to_L x} \frac{f(x') - f(x) - f'(x' - x)}{\|x' - x\|} = 0$ in the norm topology of $F$.

HasFDerivAt.lim_real theorem

(hf : HasFDerivAt f f' x) (v : E) : Tendsto (fun c : ℝ => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v))

Full source

theorem HasFDerivAt.lim_real (hf : HasFDerivAt f f' x) (v : E) :
    Tendsto (fun c : ℝ => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v)) := by
  apply hf.lim v
  rw [tendsto_atTop_atTop]
  exact fun b => ⟨b, fun a ha => le_trans ha (le_abs_self _)⟩

Limit characterization of Fréchet derivative via directional difference quotients

Informal description

Let $E$ and $F$ be normed spaces over $\mathbb{R}$, $f : E \to F$ a function, and $x \in E$. If $f$ is Fréchet differentiable at $x$ with derivative $f'$, then for any vector $v \in E$, the limit of $c \cdot (f(x + c^{-1}v) - f(x))$ as $c \to +\infty$ exists and equals $f'(v)$.

HasFDerivWithinAt.mapsTo_tangent_cone theorem

{x : E} (h : HasFDerivWithinAt f f' s x) : MapsTo f' (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))

Full source

/-- The image of a tangent cone under the differential of a map is included in the tangent cone to
the image. -/
theorem HasFDerivWithinAt.mapsTo_tangent_cone {x : E} (h : HasFDerivWithinAt f f' s x) :
    MapsTo f' (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x)) := by
  rintro v ⟨c, d, dtop, clim, cdlim⟩
  refine
    ⟨c, fun n => f (x + d n) - f x, mem_of_superset dtop ?_, clim, h.lim atTop dtop clim cdlim⟩
  simp +contextual [-mem_image, mem_image_of_mem]

Image of Tangent Cone under Derivative is Contained in Tangent Cone of Image

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable within a set $s \subseteq E$ at a point $x \in s$ with derivative $f'$. Then the derivative $f'$ maps the tangent cone of $s$ at $x$ into the tangent cone of the image $f(s)$ at $f(x)$. In other words, if $v$ belongs to the tangent cone of $s$ at $x$, then $f'(v)$ belongs to the tangent cone of $f(s)$ at $f(x)$.

HasFDerivWithinAt.uniqueDiffWithinAt theorem

 {x : E} (h : HasFDerivWithinAt f f' s x) (hs : UniqueDiffWithinAt 𝕜 s x) (h' : DenseRange f') :
  UniqueDiffWithinAt 𝕜 (f '' s) (f x)

Full source

/-- If a set has the unique differentiability property at a point x, then the image of this set
under a map with onto derivative has also the unique differentiability property at the image point.
-/
theorem HasFDerivWithinAt.uniqueDiffWithinAt {x : E} (h : HasFDerivWithinAt f f' s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) (h' : DenseRange f') : UniqueDiffWithinAt 𝕜 (f '' s) (f x) := by
  refine ⟨h'.dense_of_mapsTo f'.continuous hs.1 ?_, h.continuousWithinAt.mem_closure_image hs.2⟩
  show
    Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))).comap f'
  rw [Submodule.span_le]
  exact h.mapsTo_tangent_cone.mono Subset.rfl Submodule.subset_span

Preservation of Unique Differentiability under Densely Ranged Derivatives

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable within a set $s \subseteq E$ at a point $x \in s$ with derivative $f'$. If $s$ has the unique differentiability property at $x$ and the range of $f'$ is dense in $F$, then the image $f(s)$ has the unique differentiability property at $f(x)$.

UniqueDiffOn.image theorem

 {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
  (hd : ∀ x ∈ s, DenseRange (f' x)) : UniqueDiffOn 𝕜 (f '' s)

Full source

theorem UniqueDiffOn.image {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hd : ∀ x ∈ s, DenseRange (f' x)) :
    UniqueDiffOn 𝕜 (f '' s) :=
  forall_mem_image.2 fun x hx => (hf' x hx).uniqueDiffWithinAt (hs x hx) (hd x hx)

Preservation of Unique Differentiability under Densely Ranged Derivatives on Images

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with the unique differentiability property on $\mathbb{K}$. Suppose $f : E \to F$ is a function such that for every $x \in s$, $f$ has a Fréchet derivative $f'(x)$ within $s$ at $x$, and the range of $f'(x)$ is dense in $F$. Then the image $f(s)$ has the unique differentiability property on $\mathbb{K}$.

HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv theorem

 {x : E} (e' : E ≃L[𝕜] F) (h : HasFDerivWithinAt f (e' : E →L[𝕜] F) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
  UniqueDiffWithinAt 𝕜 (f '' s) (f x)

Full source

theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv {x : E} (e' : E ≃L[𝕜] F)
    (h : HasFDerivWithinAt f (e' : E →L[𝕜] F) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
    UniqueDiffWithinAt 𝕜 (f '' s) (f x) :=
  h.uniqueDiffWithinAt hs e'.surjective.denseRange

Preservation of Unique Differentiability under Continuous Linear Equivalence Derivatives

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable within a set $s \subseteq E$ at a point $x \in s$ with derivative given by a continuous linear equivalence $e' : E \simeqL[\mathbb{K}] F$. If $s$ has the unique differentiability property at $x$, then the image $f(s)$ has the unique differentiability property at $f(x)$.

ContinuousLinearEquiv.uniqueDiffOn_image theorem

(e : E ≃L[𝕜] F) (h : UniqueDiffOn 𝕜 s) : UniqueDiffOn 𝕜 (e '' s)

Full source

theorem ContinuousLinearEquiv.uniqueDiffOn_image (e : E ≃L[𝕜] F) (h : UniqueDiffOn 𝕜 s) :
    UniqueDiffOn 𝕜 (e '' s) :=
  h.image (fun _ _ => e.hasFDerivWithinAt) fun _ _ => e.surjective.denseRange

Preservation of Unique Differentiability under Continuous Linear Equivalence Images

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \simeqL[\mathbb{K}] F$ be a continuous linear equivalence. If a set $s \subseteq E$ has the unique differentiability property on $\mathbb{K}$, then the image $e(s) \subseteq F$ also has the unique differentiability property on $\mathbb{K}$.

ContinuousLinearEquiv.uniqueDiffOn_image_iff theorem

(e : E ≃L[𝕜] F) : UniqueDiffOn 𝕜 (e '' s) ↔ UniqueDiffOn 𝕜 s

Full source

@[simp]
theorem ContinuousLinearEquiv.uniqueDiffOn_image_iff (e : E ≃L[𝕜] F) :
    UniqueDiffOnUniqueDiffOn 𝕜 (e '' s) ↔ UniqueDiffOn 𝕜 s :=
  ⟨fun h => e.symm_image_image s ▸ e.symm.uniqueDiffOn_image h, e.uniqueDiffOn_image⟩

Unique Differentiability of Set Image under Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : E \simeqL[\mathbb{K}] F$ be a continuous linear equivalence. A subset $s \subseteq E$ has the unique differentiability property on $\mathbb{K}$ if and only if its image $e(s) \subseteq F$ has the unique differentiability property on $\mathbb{K}$.

ContinuousLinearEquiv.uniqueDiffOn_preimage_iff theorem

(e : F ≃L[𝕜] E) : UniqueDiffOn 𝕜 (e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Full source

@[simp]
theorem ContinuousLinearEquiv.uniqueDiffOn_preimage_iff (e : F ≃L[𝕜] E) :
    UniqueDiffOnUniqueDiffOn 𝕜 (e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s := by
  rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]

Unique Differentiability of Preimage under Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $e : F \simeqL[\mathbb{K}] E$ be a continuous linear equivalence. A subset $s \subseteq E$ has the unique differentiability property on $\mathbb{K}$ if and only if its preimage $e^{-1}(s) \subseteq F$ has the unique differentiability property on $\mathbb{K}$.