feat: port Analysis.Calculus.Deriv.Inverse (#4438)

Mathlib.lean

@@ -418,6 +418,7 @@ import Mathlib.Analysis.Calculus.Conformal.NormedSpace
 import Mathlib.Analysis.Calculus.Deriv.Add
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.Deriv.Inverse
 import Mathlib.Analysis.Calculus.Deriv.Linear
 import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Prod

Mathlib/Analysis/Calculus/Deriv/Inverse.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+! This file was ported from Lean 3 source module analysis.calculus.deriv.inverse
+! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.FDeriv.Equiv
+
+/-!
+# Inverse function theorem - the easy half
+
+In this file we prove that `g' (f x) = (f' x)⁻¹` provided that `f` is strictly differentiable at
+`x`, `f' x ≠ 0`, and `g` is a local left inverse of `f` that is continuous at `f x`. This is the
+easy half of the inverse function theorem: the harder half states that `g` exists.
+
+For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
+`Analysis/Calculus/Deriv/Basic`.
+
+## Keywords
+
+derivative, inverse function
+-/
+
+
+universe u v w
+
+open Classical Topology BigOperators Filter ENNReal
+
+open Filter Asymptotics Set
+
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+
+variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+variable {f f₀ f₁ g : 𝕜 → F}
+
+variable {f' f₀' f₁' g' : F}
+
+variable {x : 𝕜}
+
+variable {s t : Set 𝕜}
+
+variable {L L₁ L₂ : Filter 𝕜}
+
+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
+#align has_strict_deriv_at.has_strict_fderiv_at_equiv HasStrictDerivAt.hasStrictFDerivAt_equiv
+
+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
+#align has_deriv_at.has_fderiv_at_equiv HasDerivAt.hasFDerivAt_equiv
+
+/-- 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
+#align has_strict_deriv_at.of_local_left_inverse HasStrictDerivAt.of_local_left_inverse
+
+/-- If `f` is a local 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 LocalHomeomorph.hasStrictDerivAt_symm (f : LocalHomeomorph 𝕜 𝕜) {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)
+#align local_homeomorph.has_strict_deriv_at_symm LocalHomeomorph.hasStrictDerivAt_symm
+
+/-- 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
+#align has_deriv_at.of_local_left_inverse HasDerivAt.of_local_left_inverse
+
+/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
+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 LocalHomeomorph.hasDerivAt_symm (f : LocalHomeomorph 𝕜 𝕜) {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)
+#align local_homeomorph.has_deriv_at_symm LocalHomeomorph.hasDerivAt_symm
+
+theorem HasDerivAt.eventually_ne (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
+    ∀ᶠ z in 𝓝[≠] x, f z ≠ f x :=
+  (hasDerivAt_iff_hasFDerivAt.1 h).eventually_ne
+    ⟨‖f'‖⁻¹, fun z => by field_simp [norm_smul, mt norm_eq_zero.1 hf'] ⟩
+#align has_deriv_at.eventually_ne HasDerivAt.eventually_ne
+
+theorem HasDerivAt.tendsto_punctured_nhds (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')
+#align has_deriv_at.tendsto_punctured_nhds HasDerivAt.tendsto_punctured_nhds
+
+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 ∘ 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 _ _)
+#align not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero
+
+theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
+    (hf : HasDerivAt f 0 (g a)) (hfg : f ∘ 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)
+#align not_differentiable_at_of_local_left_inverse_has_deriv_at_zero not_differentiableAt_of_local_left_inverse_hasDerivAt_zero
+