feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): s…

…mooth inverse function theorem (#4407)

The inverse function theorem, in the C^k and smooth categories.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/calculus/fderiv.lean

@@ -1914,6 +1914,47 @@ h.continuous.comp (continuous_const.prod_mk continuous_id)
 
 end bilinear_map
 
+namespace continuous_linear_equiv
+
+/-!
+### The set of continuous linear equivalences between two Banach spaces is open
+
+In this section we establish that the set of continuous linear equivalences between two Banach
+spaces is an open subset of the space of linear maps between them.  These facts are placed here
+because the proof uses `is_bounded_bilinear_map.continuous`, proved just above as a consequence
+of its differentiability.
+-/
+
+protected lemma is_open [complete_space E] : is_open (range (coe : (E ≃L[𝕜] F) → (E →L[𝕜] F))) :=
+begin
+  rw [is_open_iff_mem_nhds, forall_range_iff],
+  refine λ e, mem_nhds_sets _ (mem_range_self _),
+  let O : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : F →L[𝕜] E).comp f,
+  cases subsingleton_or_nontrivial E with _i _i; resetI,
+  { exact is_open_discrete _ },
+  have h_O : continuous O,
+  { have h_e_symm : continuous (λ (x : E →L[𝕜] F), (e.symm : F →L[𝕜] E)) := continuous_const,
+    exact is_bounded_bilinear_map_comp.continuous.comp (continuous_id.prod_mk h_e_symm) },
+  convert units.is_open.preimage h_O using 1,
+  ext f',
+  split,
+  { rintros ⟨e', rfl⟩,
+    let w : units (E →L[𝕜] E) := continuous_linear_equiv.to_unit (e'.trans e.symm),
+    exact ⟨w, rfl⟩ },
+  { rintros ⟨w, hw⟩,
+    let e' : E ≃L[𝕜] E := continuous_linear_equiv.of_unit w,
+    use e'.trans e,
+    ext x,
+    have he'w : e' x = w x := rfl,
+    simp [hw, he'w] }
+end
+
+protected lemma nhds [complete_space E] (e : E ≃L[𝕜] F) :
+  (range (coe : (E ≃L[𝕜] F) → (E →L[𝕜] F))) ∈ 𝓝 (e : E →L[𝕜] F) :=
+mem_nhds_sets continuous_linear_equiv.is_open (by simp)
+
+end continuous_linear_equiv
+
 section smul
 /-! ### Derivative of the product of a scalar-valued function and a vector-valued function -/
 
@@ -2351,6 +2392,17 @@ begin
     simp only [(∘), hp, hfg.self_of_nhds] }
 end
 
+
+/-- If `f` is a local 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. -/
+lemma has_fderiv_at.of_local_homeomorph {f : local_homeomorph E F} {f' : E ≃L[𝕜] F} {a : F}
+  (ha : a ∈ f.target) (htff' : has_fderiv_at f (f' : E →L[𝕜] F) (f.symm a)) :
+  has_fderiv_at f.symm (f'.symm : F →L[𝕜] E) a :=
+htff'.of_local_left_inverse (f.symm.continuous_at ha) (f.eventually_right_inverse ha)
+
 end
 
 section

src/analysis/calculus/inverse.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov.
+Authors: Yury Kudryashov, Heather Macbeth.
 -/
-import analysis.calculus.deriv
+import analysis.calculus.times_cont_diff
 import topology.local_homeomorph
 import topology.metric_space.contracting
 
@@ -31,8 +31,15 @@ and prove two versions of the inverse function theorem:
   `f'.symm` at `f a` in the strict sense.
 
 In the one-dimensional case we reformulate these theorems in terms of `has_strict_deriv_at` and
-`f'⁻¹`. Some other versions of the theorem assuming that we already know the inverse function are
-formulated in `fderiv.lean` and `deriv.lean`
+`f'⁻¹`.
+
+We also reformulate the theorems in terms of `times_cont_diff`, to give that `C^k` (respectively,
+smooth) inputs give `C^k` (smooth) inverses.  These versions require that continuous
+differentiability implies strict differentiability; this is false over a general field, true over
+`ℝ` (the setting in which it is implemented here), and true but (TODO) not yet implemented over `ℂ`.
+
+Some related theorems, providing the derivative and higher regularity assuming that we already know
+the inverse function, are formulated in `fderiv.lean`, `deriv.lean`, and `times_cont_diff.lean`.
 
 ## Notations
 
@@ -45,7 +52,7 @@ shorter:
 
 ## Tags
 
-derivative, strictly differentiable, inverse function
+derivative, strictly differentiable, continuously differentiable, smooth, inverse function
 -/
 
 open function set filter metric
@@ -496,3 +503,69 @@ theorem to_local_left_inverse {g : 𝕜 → 𝕜} (hg : ∀ᶠ x in 𝓝 a, g (f
 (hf.has_strict_fderiv_at_equiv hf').to_local_left_inverse hg
 
 end has_strict_deriv_at
+
+/-!
+### Inverse function theorem, smooth case
+
+-/
+
+namespace times_cont_diff_at
+variables {E' : Type*} [normed_group E'] [normed_space ℝ E']
+variables {F' : Type*} [normed_group F'] [normed_space ℝ F']
+variables [complete_space E'] (f : E' → F') {f' : E' ≃L[ℝ] F'} {a : E'}
+
+/-- Given a `times_cont_diff` function over `ℝ` with an invertible derivative at `a`, returns a
+`local_homeomorph` with `to_fun = f` and `a ∈ source`. -/
+def to_local_homeomorph
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  local_homeomorph E' F' :=
+(hf.has_strict_fderiv_at' hf' hn).to_local_homeomorph f
+
+variable {f}
+
+@[simp] lemma to_local_homeomorph_coe
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  (hf.to_local_homeomorph f hf' hn : E' → F') = f := rfl
+
+lemma mem_to_local_homeomorph_source
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  a ∈ (hf.to_local_homeomorph f hf' hn).source :=
+(hf.has_strict_fderiv_at' hf' hn).mem_to_local_homeomorph_source
+
+lemma image_mem_to_local_homeomorph_target
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  f a ∈ (hf.to_local_homeomorph f hf' hn).target :=
+(hf.has_strict_fderiv_at' hf' hn).image_mem_to_local_homeomorph_target
+
+/-- Given a `times_cont_diff` function over `ℝ` with an invertible derivative at `a`, returns a
+function that is locally inverse to `f`. -/
+def local_inverse
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  F' → E' :=
+(hf.has_strict_fderiv_at' hf' hn).local_inverse f f' a
+
+lemma local_inverse_apply_image
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  hf.local_inverse hf' hn (f a) = a :=
+(hf.has_strict_fderiv_at' hf' hn).local_inverse_apply_image
+
+/-- Given a `times_cont_diff` function over `ℝ` with an invertible derivative at `a`, the inverse
+function (produced by `times_cont_diff.to_local_homeomorph`) is also `times_cont_diff`. -/
+lemma to_local_inverse
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f a) (hf' : has_fderiv_at f (f' : E' →L[ℝ] F') a)
+  (hn : 1 ≤ n) :
+  times_cont_diff_at ℝ n (hf.local_inverse hf' hn) (f a) :=
+begin
+  have := hf.local_inverse_apply_image hf' hn,
+  apply times_cont_diff_at.of_local_homeomorph (image_mem_to_local_homeomorph_target hf hf' hn),
+  { convert hf' },
+  { convert hf }
+end
+
+end times_cont_diff_at

src/analysis/calculus/times_cont_diff.lean

@@ -873,6 +873,22 @@ begin
   exact ⟨by rwa insert_eq_of_mem hx, λ x hx, by simp [ftaylor_series_within]⟩
 end
 
+lemma times_cont_diff_within_at_zero (hx : x ∈ s) :
+  times_cont_diff_within_at 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, continuous_on f (s ∩ u) :=
+begin
+  split,
+  { intros h,
+    obtain ⟨u, H, p, hp⟩ := h 0 (by norm_num),
+    refine ⟨u, _, _⟩,
+    { simpa [hx] using H },
+    { simp only [with_top.coe_zero, has_ftaylor_series_up_to_on_zero_iff] at hp,
+      exact hp.1.mono (inter_subset_right s u) } },
+  { rintros ⟨u, H, hu⟩,
+    rw ← times_cont_diff_within_at_inter' H,
+    have h' : x ∈ s ∩ u := ⟨hx, mem_of_mem_nhds_within hx H⟩,
+    exact (times_cont_diff_on_zero.mpr hu).times_cont_diff_within_at h' }
+end
+
 /-- On a set with unique differentiability, any choice of iterated differential has to coincide
 with the one we have chosen in `iterated_fderiv_within 𝕜 m f s`. -/
 theorem has_ftaylor_series_up_to_on.eq_ftaylor_series_of_unique_diff_on {n : with_top ℕ}
@@ -1053,8 +1069,8 @@ begin
     exact with_top.coe_le_coe.2 (nat.le_succ n) }
 end
 
-/-- A function is `C^∞` on a domain with unique derivatives if and only if it is differentiable
-there, and its derivative (expressed with `fderiv`) is `C^∞`. -/
+/-- A function is `C^∞` on an open domain if and only if it is differentiable there, and its
+derivative (expressed with `fderiv`) is `C^∞`. -/
 theorem times_cont_diff_on_top_iff_fderiv_of_open (hs : is_open s) :
   times_cont_diff_on 𝕜 ∞ f s ↔
   differentiable_on 𝕜 f s ∧ times_cont_diff_on 𝕜 ∞ (λ y, fderiv 𝕜 f y) s :=
@@ -1315,6 +1331,10 @@ begin
   exact times_cont_diff_on_zero
 end
 
+lemma times_cont_diff_at_zero :
+  times_cont_diff_at 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, continuous_on f u :=
+by { rw ← times_cont_diff_within_at_univ, simp [times_cont_diff_within_at_zero, nhds_within_univ] }
+
 lemma times_cont_diff.of_le {m n : with_top ℕ}
   (h : times_cont_diff 𝕜 n f) (hmn : m ≤ n) :
   times_cont_diff 𝕜 m f :=
@@ -2382,6 +2402,66 @@ end
 
 end map_inverse
 
+section function_inverse
+open continuous_linear_map
+
+/-- If `f` is a local homeomorphism and the point `a` is in its target, and if `f` is `n` times
+continuously differentiable at `f.symm a`, and if the derivative at `f.symm a` is a continuous linear
+equivalence, then `f.symm` is `n` times continuously differentiable at the point `a`.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem times_cont_diff_at.of_local_homeomorph [complete_space E] {n : with_top ℕ}
+  {f : local_homeomorph E F} {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
+  (hf₀' : has_fderiv_at f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : times_cont_diff_at 𝕜 n f (f.symm a)) :
+  times_cont_diff_at 𝕜 n f.symm a :=
+begin
+  -- We prove this by induction on `n`
+  induction n using with_top.nat_induction with n IH Itop,
+  { rw times_cont_diff_at_zero,
+    exact ⟨f.target, mem_nhds_sets f.open_target ha, f.continuous_inv_fun⟩ },
+  { obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := times_cont_diff_at_succ_iff_has_fderiv_at.mp hf,
+    apply times_cont_diff_at_succ_iff_has_fderiv_at.mpr,
+    -- For showing `n.succ` times continuous differentiability (the main inductive step), it
+    -- suffices to produce the derivative and show that it is `n` times continuously differentiable
+    have eq_f₀' : f' (f.symm a) = f₀',
+    { exact has_fderiv_at_unique (hff' (f.symm a) (mem_of_nhds hu)) hf₀' },
+    -- This follows by a bootstrapping formula expressing the derivative as a function of `f` itself
+    refine ⟨inverse ∘ f' ∘ f.symm, _, _⟩,
+    { -- We first check that the derivative of `f` is that formula
+      have h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), ↑e = f' y} ∈ 𝓝 ((f.symm) a),
+      { have hf₀' := f₀'.nhds,
+        rw ← eq_f₀' at hf₀',
+        exact hf'.continuous_at.preimage_mem_nhds hf₀' },
+      obtain ⟨t, htu, ht, htf⟩ := mem_nhds_sets_iff.mp (filter.inter_mem_sets hu h_nhds),
+      use f.target ∩ (f.symm) ⁻¹' t,
+      refine ⟨mem_nhds_sets _ _, _⟩,
+      { exact f.preimage_open_of_open_symm ht },
+      { exact mem_inter ha (mem_preimage.mpr htf) },
+      intros x hx,
+      obtain ⟨hxu, e, he⟩ := htu hx.2,
+      have h_deriv : has_fderiv_at f ↑e ((f.symm) x),
+      { rw he,
+        exact hff' (f.symm x) hxu },
+      convert h_deriv.of_local_homeomorph hx.1,
+      simp [← he] },
+    { -- Then we check that the formula, being a composition of `times_cont_diff` pieces, is
+      -- itself `times_cont_diff`
+      have h_deriv₁ : times_cont_diff_at 𝕜 n inverse (f' (f.symm a)),
+      { rw eq_f₀',
+        exact times_cont_diff_at_map_inverse _ },
+      have h_deriv₂ : times_cont_diff_at 𝕜 n f.symm a,
+      { refine IH (hf.of_le _),
+        norm_cast,
+        exact nat.le_succ n },
+      exact (h_deriv₁.comp _ hf').comp _ h_deriv₂ } },
+  { refine times_cont_diff_at_top.mpr _,
+    intros n,
+    exact Itop n (times_cont_diff_at_top.mp hf n) }
+end
+
+end function_inverse
+
 section real
 /-!
 ### Results over `ℝ`
@@ -2421,6 +2501,14 @@ begin
   exact this.has_fderiv_at.fderiv
 end
 
+/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
+us as `f'`, then `f'` is also a strict derivative. -/
+lemma times_cont_diff_at.has_strict_fderiv_at'
+  {f : E' → F'} {f' : E' →L[ℝ] F'} {x : E'}
+  {n : with_top ℕ} (hf : times_cont_diff_at ℝ n f x) (hf' : has_fderiv_at f f' x) (hn : 1 ≤ n) :
+  has_strict_fderiv_at f f' x :=
+by simpa only [hf'.fderiv] using hf.has_strict_fderiv_at hn
+
 /-- If a function is `C^n` with `1 ≤ n`, then the derivative of `f` is also a strict derivative. -/
 lemma times_cont_diff.has_strict_fderiv_at
   {f : E' → F'} {x : E'} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) (hn : 1 ≤ n) :