chore(Calculus/Inverse): split (#8603)

Mathlib.lean

@@ -623,7 +623,11 @@ import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
 import Mathlib.Analysis.Calculus.Gradient.Basic
 import Mathlib.Analysis.Calculus.Implicit
-import Mathlib.Analysis.Calculus.Inverse
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.Calculus.LHopital
 import Mathlib.Analysis.Calculus.LagrangeMultipliers

Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

@@ -16,8 +16,10 @@ see the module docstring of `Analysis/Calculus/FDeriv/Basic.lean`.
 
 This file contains the usual formulas (and existence assertions) for the derivative of
 continuous linear equivalences.
--/
 
+We also prove the usual formula for the derivative of the inverse function, assuming it exists.
+The inverse function theorem is in `Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean`.
+-/
 
 open Filter Asymptotics ContinuousLinearMap Set Metric
 

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -17,8 +17,7 @@ This file contains the usual formulas (and existence assertions) for the derivat
 
 * multiplication of a function by a scalar function
 * multiplication of two scalar functions
-* inverse function (assuming that it exists; the inverse function theorem is in
-  `Mathlib/Analysis/Calculus/Inverse.lean`)
+* taking the pointwise multiplicative inverse (i.e. `Inv.inv` or `Ring.inverse`) of a function
 -/
 
 

Mathlib/Analysis/Calculus/Implicit.lean

@@ -3,7 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.Calculus.Inverse
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.NormedSpace.Complemented
 
 #align_import analysis.calculus.implicit from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2020 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import Mathlib.Analysis.Calculus.ContDiff.IsROrC
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+
+/-!
+# Inverse function theorem, smooth case
+
+In this file we specialize the inverse function theorem to `C^r`-smooth functions.
+-/
+
+noncomputable section
+
+namespace ContDiffAt
+
+variable {𝕂 : Type*} [IsROrC 𝕂]
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕂 E]
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕂 F]
+
+variable [CompleteSpace E] (f : E → F) {f' : E ≃L[𝕂] F} {a : E}
+
+/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible
+derivative at `a`, returns a `LocalHomeomorph` with `to_fun = f` and `a ∈ source`. -/
+def toLocalHomeomorph {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a)
+    (hn : 1 ≤ n) : LocalHomeomorph E F :=
+  (hf.hasStrictFDerivAt' hf' hn).toLocalHomeomorph f
+#align cont_diff_at.to_local_homeomorph ContDiffAt.toLocalHomeomorph
+
+variable {f}
+
+@[simp]
+theorem toLocalHomeomorph_coe {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
+    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
+    (hf.toLocalHomeomorph f hf' hn : E → F) = f :=
+  rfl
+#align cont_diff_at.to_local_homeomorph_coe ContDiffAt.toLocalHomeomorph_coe
+
+theorem mem_toLocalHomeomorph_source {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
+    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
+    a ∈ (hf.toLocalHomeomorph f hf' hn).source :=
+  (hf.hasStrictFDerivAt' hf' hn).mem_toLocalHomeomorph_source
+#align cont_diff_at.mem_to_local_homeomorph_source ContDiffAt.mem_toLocalHomeomorph_source
+
+theorem image_mem_toLocalHomeomorph_target {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
+    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
+    f a ∈ (hf.toLocalHomeomorph f hf' hn).target :=
+  (hf.hasStrictFDerivAt' hf' hn).image_mem_toLocalHomeomorph_target
+#align cont_diff_at.image_mem_to_local_homeomorph_target ContDiffAt.image_mem_toLocalHomeomorph_target
+
+/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
+at `a`, returns a function that is locally inverse to `f`. -/
+def localInverse {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a)
+    (hn : 1 ≤ n) : F → E :=
+  (hf.hasStrictFDerivAt' hf' hn).localInverse f f' a
+#align cont_diff_at.local_inverse ContDiffAt.localInverse
+
+theorem localInverse_apply_image {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
+    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) : hf.localInverse hf' hn (f a) = a :=
+  (hf.hasStrictFDerivAt' hf' hn).localInverse_apply_image
+#align cont_diff_at.local_inverse_apply_image ContDiffAt.localInverse_apply_image
+
+/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
+at `a`, the inverse function (produced by `ContDiff.toLocalHomeomorph`) is
+also `ContDiff`. -/
+theorem to_localInverse {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
+    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
+    ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a) := by
+  have := hf.localInverse_apply_image hf' hn
+  apply (hf.toLocalHomeomorph f hf' hn).contDiffAt_symm
+    (image_mem_toLocalHomeomorph_target hf hf' hn)
+  · convert hf'
+  · convert hf
+#align cont_diff_at.to_local_inverse ContDiffAt.to_localInverse
+
+end ContDiffAt

Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+-/
+import Mathlib.Analysis.Calculus.Deriv.Inverse
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+
+/-!
+# Inverse function theorem, 1D case
+
+In this file we prove a version of the inverse function theorem for maps `f : 𝕜 → 𝕜`.
+We use `ContinuousLinearEquiv.unitsEquivAut` to translate `HasStrictDerivAt f f' a` and
+`f' ≠ 0` into `HasStrictFDerivAt f (_ : 𝕜 ≃L[𝕜] 𝕜) a`.
+-/
+
+open Filter
+open scoped Topology
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (f : 𝕜 → 𝕜)
+
+noncomputable section
+namespace HasStrictDerivAt
+
+variable (f' a : 𝕜) (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0)
+
+/-- A function that is inverse to `f` near `a`. -/
+@[reducible]
+def localInverse : 𝕜 → 𝕜 :=
+  (hf.hasStrictFDerivAt_equiv hf').localInverse _ _ _
+#align has_strict_deriv_at.local_inverse HasStrictDerivAt.localInverse
+
+variable {f f' a}
+
+theorem map_nhds_eq : map f (𝓝 a) = 𝓝 (f a) :=
+  (hf.hasStrictFDerivAt_equiv hf').map_nhds_eq_of_equiv
+#align has_strict_deriv_at.map_nhds_eq HasStrictDerivAt.map_nhds_eq
+
+theorem to_localInverse : HasStrictDerivAt (hf.localInverse f f' a hf') f'⁻¹ (f a) :=
+  (hf.hasStrictFDerivAt_equiv hf').to_localInverse
+#align has_strict_deriv_at.to_local_inverse HasStrictDerivAt.to_localInverse
+
+theorem to_local_left_inverse {g : 𝕜 → 𝕜} (hg : ∀ᶠ x in 𝓝 a, g (f x) = x) :
+    HasStrictDerivAt g f'⁻¹ (f a) :=
+  (hf.hasStrictFDerivAt_equiv hf').to_local_left_inverse hg
+#align has_strict_deriv_at.to_local_left_inverse HasStrictDerivAt.to_local_left_inverse
+
+end HasStrictDerivAt
+
+variable {f}
+
+/-- If a function has a non-zero strict derivative at all points, then it is an open map. -/
+theorem open_map_of_strict_deriv {f' : 𝕜 → 𝕜}
+    (hf : ∀ x, HasStrictDerivAt f (f' x) x) (h0 : ∀ x, f' x ≠ 0) : IsOpenMap f :=
+  isOpenMap_iff_nhds_le.2 fun x => ((hf x).map_nhds_eq (h0 x)).ge
+#align open_map_of_strict_deriv open_map_of_strict_deriv