Mathlib.Analysis.Calculus.Deriv.Inverse

HasStrictDerivAt.hasStrictFDerivAt_equiv theorem

 {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasStrictDerivAt f f' x) (hf' : f' ≠ 0) :
  HasStrictFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x

Full source

theorem HasStrictDerivAt.hasStrictFDerivAt_equiv {f : 𝕜 → 𝕜} {f' x : 𝕜}
    (hf : HasStrictDerivAt f f' x) (hf' : f' ≠ 0) :
    HasStrictFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x :=
  hf

Strict Differentiability Implies Strict Fréchet Differentiability via Unit Equivalence

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function that is strictly differentiable at $x \in \mathbb{K}$ with derivative $f' \neq 0$. Then $f$ has a strict Fréchet derivative at $x$ given by the continuous linear equivalence $\mathbb{K} \to \mathbb{K}$ corresponding to the unit $f'$ in $\mathbb{K}^\times$.

HasDerivAt.hasFDerivAt_equiv theorem

 {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasDerivAt f f' x) (hf' : f' ≠ 0) :
  HasFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x

Full source

theorem HasDerivAt.hasFDerivAt_equiv {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasDerivAt f f' x)
    (hf' : f' ≠ 0) :
    HasFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x :=
  hf

Fréchet Derivative of Differentiable Function via Unit Equivalence

Informal description

Let $f : \mathbb{K} \to \mathbb{K}$ be a function that is differentiable at $x \in \mathbb{K}$ with derivative $f' \neq 0$. Then $f$ has a Fréchet derivative at $x$ given by the continuous linear equivalence $\mathbb{K} \to \mathbb{K}$ associated to the unit $f'$ in $\mathbb{K}^\times$.

HasStrictDerivAt.of_local_left_inverse theorem

 {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasStrictDerivAt f f' (g a)) (hf' : f' ≠ 0)
  (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasStrictDerivAt g f'⁻¹ 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 HasStrictDerivAt.of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a)
    (hf : HasStrictDerivAt f f' (g a)) (hf' : f' ≠ 0) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) :
    HasStrictDerivAt g f'⁻¹ a :=
  (hf.hasStrictFDerivAt_equiv hf').of_local_left_inverse hg hfg

Strict derivative of a local left inverse: $g'(a) = (f'(g(a)))^{-1}$

Informal description

Let $f, g \colon \mathbb{K} \to \mathbb{K}$ be functions, and let $a, f' \in \mathbb{K}$. Suppose that: 1. $g$ is continuous at $a$, 2. $f$ is strictly differentiable at $g(a)$ with derivative $f' \neq 0$, 3. There exists a neighborhood of $a$ such that $f(g(y)) = y$ for all $y$ in this neighborhood. Then $g$ is strictly differentiable at $a$ with derivative $f'^{-1}$.

PartialHomeomorph.hasStrictDerivAt_symm theorem

 (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasStrictDerivAt f f' (f.symm a)) :
  HasStrictDerivAt f.symm f'⁻¹ a

Full source

/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
nonzero derivative `f'` at `f.symm a` in the strict sense, then `f.symm` 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 PartialHomeomorph.hasStrictDerivAt_symm (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜}
    (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasStrictDerivAt f f' (f.symm a)) :
    HasStrictDerivAt f.symm f'⁻¹ a :=
  htff'.of_local_left_inverse (f.symm.continuousAt ha) hf' (f.eventually_right_inverse ha)

Strict derivative of inverse function: $(f^{-1})'(a) = (f'(f^{-1}(a)))^{-1}$

Informal description

Let $f$ be a partial homeomorphism between two topological spaces over a field $\mathbb{K}$, and let $a \in f.\text{target}$ and $f' \in \mathbb{K}$ with $f' \neq 0$. If $f$ is strictly differentiable at $f^{-1}(a)$ with derivative $f'$, then the inverse function $f^{-1}$ is strictly differentiable at $a$ with derivative $f'^{-1}$. In other words, under the given conditions, the derivative of the inverse function at $a$ is the multiplicative inverse of the derivative of $f$ at $f^{-1}(a)$.

HasDerivAt.of_local_left_inverse theorem

 {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasDerivAt f f' (g a)) (hf' : f' ≠ 0)
  (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasDerivAt g f'⁻¹ 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 HasDerivAt.of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a)
    (hf : HasDerivAt f f' (g a)) (hf' : f' ≠ 0) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) :
    HasDerivAt g f'⁻¹ a :=
  (hf.hasFDerivAt_equiv hf').of_local_left_inverse hg hfg

Derivative of Local Left Inverse: $g'(a) = (f'(g(a)))^{-1}$

Informal description

Let $f, g \colon \mathbb{K} \to \mathbb{K}$ be functions, and let $a, f' \in \mathbb{K}$. Suppose that: 1. $g$ is continuous at $a$, 2. $f$ is differentiable at $g(a)$ with derivative $f' \neq 0$, 3. There exists a neighborhood of $a$ where $f(g(y)) = y$ for all $y$ in this neighborhood. Then $g$ is differentiable at $a$ with derivative $f'^{-1}$.

PartialHomeomorph.hasDerivAt_symm theorem

 (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasDerivAt f f' (f.symm a)) :
  HasDerivAt f.symm f'⁻¹ a

Full source

/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
nonzero 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.hasDerivAt_symm (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target)
    (hf' : f' ≠ 0) (htff' : HasDerivAt f f' (f.symm a)) : HasDerivAt f.symm f'⁻¹ a :=
  htff'.of_local_left_inverse (f.symm.continuousAt ha) hf' (f.eventually_right_inverse ha)

Derivative of Inverse Function: $(f^{-1})'(a) = (f'(f^{-1}(a)))^{-1}$

Informal description

Let $f$ be a partial homeomorphism between two topological spaces over a field $\mathbb{K}$, and let $a \in \mathbb{K}$ be a point in the target of $f$. Suppose that: 1. $f$ is differentiable at its inverse image $f^{-1}(a)$ with derivative $f' \neq 0$, 2. $a$ belongs to the target of $f$. Then the inverse function $f^{-1}$ is differentiable at $a$ with derivative $(f')^{-1}$.

HasDerivWithinAt.eventually_ne theorem

(h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) : ∀ᶠ z in 𝓝[s \ { x }] x, f z ≠ c

Full source

theorem HasDerivWithinAt.eventually_ne (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) :
    ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ c :=
  h.hasFDerivWithinAt.eventually_ne
    ⟨‖f'‖⁻¹, fun z => by field_simp [norm_smul, mt norm_eq_zero.1 hf']⟩

Non-constancy of Differentiable Functions with Nonzero Derivative in Punctured Neighborhoods

Informal description

Let $f$ be a function differentiable at $x$ within a set $s \subseteq \mathbb{K}$ with derivative $f' \neq 0$. Then for any constant $c$, there exists a neighborhood of $x$ in $s \setminus \{x\}$ such that $f(z) \neq c$ for all $z$ in this neighborhood.

HasDerivAt.eventually_ne theorem

(h : HasDerivAt f f' x) (hf' : f' ≠ 0) : ∀ᶠ z in 𝓝[≠] x, f z ≠ c

Full source

theorem HasDerivAt.eventually_ne (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
    ∀ᶠ z in 𝓝[≠] x, f z ≠ c := by
  simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).eventually_ne hf'

Non-constancy of Differentiable Functions with Nonzero Derivative in Punctured Neighborhoods

Informal description

Let $f$ be a function differentiable at a point $x$ with derivative $f' \neq 0$. Then, for any constant $c$, there exists a punctured neighborhood of $x$ such that $f(z) \neq c$ for all $z$ in this neighborhood.

HasDerivAt.tendsto_nhdsNE theorem

(h : HasDerivAt f f' x) (hf' : f' ≠ 0) : Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Full source

theorem HasDerivAt.tendsto_nhdsNE (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
    Tendsto f (𝓝[≠] x) (𝓝[≠] f x) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.continuousAt.continuousWithinAt
    (h.eventually_ne hf')

Punctured Neighborhood Preservation under Differentiable Maps with Nonzero Derivative

Informal description

Let $f \colon \mathbb{K} \to F$ be a function differentiable at a point $x \in \mathbb{K}$ with derivative $f' \in F$ such that $f' \neq 0$. Then $f$ maps punctured neighborhoods of $x$ to punctured neighborhoods of $f(x)$, i.e., the limit of $f(z)$ as $z$ approaches $x$ (with $z \neq x$) exists and equals $f(x)$, and for any neighborhood of $f(x)$ excluding $f(x)$ itself, there exists a punctured neighborhood of $x$ that $f$ maps entirely into it.

derivWithin_zero_of_frequently_const theorem

{c} (h : ∃ᶠ y in 𝓝[s \ { x }] x, f y = c) : derivWithin f s x = 0

Full source

/-- If a function is equal to a constant at a set of points that accumulates to `x` in `s`,
then its derivative within `s` at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point. -/
theorem derivWithin_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[s \ {x}] x, f y = c) :
    derivWithin f s x = 0 := by
  by_cases hf : DifferentiableWithinAt 𝕜 f s x
  · contrapose h
    rw [not_frequently]
    exact hf.hasDerivWithinAt.eventually_ne h
  · exact derivWithin_zero_of_not_differentiableWithinAt hf

Vanishing Derivative for Functions Constant on a Punctured Neighborhood

Informal description

Let $f : \mathbb{K} \to F$ be a function and $s \subseteq \mathbb{K}$ a set. If there exists a constant $c$ such that $f(y) = c$ frequently in a punctured neighborhood of $x$ within $s$ (i.e., for infinitely many points $y$ arbitrarily close to $x$ in $s \setminus \{x\}$), then the derivative of $f$ at $x$ within $s$ is zero, i.e., $\text{derivWithin}\, f\, s\, x = 0$.

deriv_zero_of_frequently_const theorem

{c} (h : ∃ᶠ y in 𝓝[≠] x, f y = c) : deriv f x = 0

Full source

/-- If a function is equal to a constant at a set of points that accumulates to `x`,
then its derivative at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point. -/
theorem deriv_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[≠] x, f y = c) : deriv f x = 0 := by
  rw [← derivWithin_univ, derivWithin_zero_of_frequently_const]
  rwa [← compl_eq_univ_diff]

Vanishing Derivative for Functions Constant on a Punctured Neighborhood

Informal description

Let $f : \mathbb{K} \to F$ be a function. If there exists a constant $c$ such that $f(y) = c$ frequently in a punctured neighborhood of $x$ (i.e., for infinitely many points $y$ arbitrarily close to $x$ but not equal to $x$), then the derivative of $f$ at $x$ is zero, i.e., $\text{deriv}\, f\, x = 0$.

not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero theorem

 {f g : 𝕜 → 𝕜} {a : 𝕜} {s t : Set 𝕜} (ha : a ∈ s) (hsu : UniqueDiffWithinAt 𝕜 s a) (hf : HasDerivWithinAt f 0 t (g a))
  (hst : MapsTo g s t) (hfg : f ∘ g =ᶠ[𝓝[s] a] id) : ¬DifferentiableWithinAt 𝕜 g s a

Full source

theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
    {s t : Set 𝕜} (ha : a ∈ s) (hsu : UniqueDiffWithinAt 𝕜 s a) (hf : HasDerivWithinAt f 0 t (g a))
    (hst : MapsTo g s t) (hfg : f ∘ gf ∘ g =ᶠ[𝓝[s] a] id) : ¬DifferentiableWithinAt 𝕜 g s a := by
  intro hg
  have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha
  simpa using hsu.eq_deriv _ this (hasDerivWithinAt_id _ _)

Non-differentiability of a Local Left Inverse with Zero Derivative Within a Set

Informal description

Let $f, g : \mathbb{K} \to \mathbb{K}$ be functions, and let $a \in \mathbb{K}$ be a point in a set $s \subseteq \mathbb{K}$. Suppose that: 1. $s$ is uniquely differentiable at $a$, 2. $f$ has derivative $0$ at $g(a)$ within a set $t \subseteq \mathbb{K}$, 3. $g$ maps $s$ into $t$, 4. $f \circ g$ is eventually equal to the identity function in a neighborhood of $a$ within $s$. Then $g$ is not differentiable within $s$ at $a$.

not_differentiableAt_of_local_left_inverse_hasDerivAt_zero theorem

 {f g : 𝕜 → 𝕜} {a : 𝕜} (hf : HasDerivAt f 0 (g a)) (hfg : f ∘ g =ᶠ[𝓝 a] id) : ¬DifferentiableAt 𝕜 g a

Full source

theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
    (hf : HasDerivAt f 0 (g a)) (hfg : f ∘ gf ∘ g =ᶠ[𝓝 a] id) : ¬DifferentiableAt 𝕜 g a := by
  intro hg
  have := (hf.comp a hg.hasDerivAt).congr_of_eventuallyEq hfg.symm
  simpa using this.unique (hasDerivAt_id a)

Non-differentiability of a Local Left Inverse with Zero Derivative

Informal description

Let $f, g : \mathbb{K} \to \mathbb{K}$ be functions and $a \in \mathbb{K}$. If: 1. $f$ has derivative $0$ at $g(a)$, and 2. $f \circ g$ is eventually equal to the identity function in a neighborhood of $a$, then $g$ is not differentiable at $a$.

Keywords