feat(analysis/calculus/times_cont_diff): inversion of continuous linear maps is smooth (#4185)

- Introduce an `inverse` function on the space of continuous linear maps between two Banach spaces, which is the inverse if the map is a continuous linear equivalence and zero otherwise.

- Prove that this function is `times_cont_diff_at` each `continuous_linear_equiv`.

- Some of the constructions used had been introduced in #3282 and placed in `analysis.normed_space.operator_norm` (normed spaces); they are moved to the earlier file `topology.algebra.module` (topological vector spaces).

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: hrmacbeth

src/algebra/ring/basic.lean

@@ -775,12 +775,15 @@ noncomputable def inverse : R → R :=
 λ x, if h : is_unit x then (((classical.some h)⁻¹ : units R) : R) else 0
 
 /-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
-lemma inverse_unit (a : units R) : inverse (a : R) = (a⁻¹ : units R) :=
+@[simp] lemma inverse_unit (a : units R) : inverse (a : R) = (a⁻¹ : units R) :=
 begin
   simp [is_unit_unit, inverse],
   exact units.inv_unique (classical.some_spec (is_unit_unit a)),
 end
 
+/-- By definition, if `x` is not invertible then `inverse x = 0`. -/
+@[simp] lemma inverse_non_unit (x : R) (h : ¬(is_unit x)) : inverse x = 0 := dif_neg h
+
 end ring
 
 /-- A predicate to express that a ring is an integral domain.

src/analysis/calculus/fderiv.lean

@@ -2142,8 +2142,8 @@ open normed_ring continuous_linear_map ring
 
 /-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
 operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/
-lemma has_fderiv_at_inverse  (x : units R) :
-  has_fderiv_at inverse (- (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹)) x :=
+lemma has_fderiv_at_ring_inverse (x : units R) :
+  has_fderiv_at ring.inverse (- (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹)) x :=
 begin
   have h_is_o : is_o (λ (t : R), inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹)
     (λ (t : R), t) (𝓝 0),
@@ -2163,12 +2163,12 @@ begin
   abel
 end
 
-lemma differentiable_at_inverse (x : units R) : differentiable_at 𝕜 (@inverse R _) x :=
-(has_fderiv_at_inverse x).differentiable_at
+lemma differentiable_at_inverse (x : units R) : differentiable_at 𝕜 (@ring.inverse R _) x :=
+(has_fderiv_at_ring_inverse x).differentiable_at
 
 lemma fderiv_inverse (x : units R) :
-  fderiv 𝕜 (@inverse R _) x = - (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹) :=
-(has_fderiv_at_inverse x).fderiv
+  fderiv 𝕜 (@ring.inverse R _) x = - (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹) :=
+(has_fderiv_at_ring_inverse x).fderiv
 
 end algebra_inverse
 

src/analysis/calculus/times_cont_diff.lean

@@ -1812,6 +1812,13 @@ lemma times_cont_diff_on.prod {n : with_top ℕ} {s : set E} {f : E → F} {g :
   times_cont_diff_on 𝕜 n (λx:E, (f x, g x)) s :=
 λ x hx, (hf x hx).prod (hg x hx)
 
+/-- The cartesian product of `C^n` functions at a point is `C^n`. -/
+lemma times_cont_diff_at.prod {n : with_top ℕ} {f : E → F} {g : E → G}
+  (hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g x) :
+  times_cont_diff_at 𝕜 n (λx:E, (f x, g x)) x :=
+times_cont_diff_within_at_univ.1 $ times_cont_diff_within_at.prod (times_cont_diff_within_at_univ.2 hf)
+  (times_cont_diff_within_at_univ.2 hg)
+
 /--
 The cartesian product of `C^n` functions is `C^n`.
 -/
@@ -2273,8 +2280,8 @@ open normed_ring continuous_linear_map ring
 /-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
 invertible element.  The proof is by induction, bootstrapping using an identity expressing the
 derivative of inversion as a bilinear map of inversion itself. -/
-lemma times_cont_diff_at_inverse [complete_space R] {n : with_top ℕ} (x : units R) :
-  times_cont_diff_at 𝕜 n inverse (x : R) :=
+lemma times_cont_diff_at_ring_inverse [complete_space R] {n : with_top ℕ} (x : units R) :
+  times_cont_diff_at 𝕜 n ring.inverse (x : R) :=
 begin
   induction n using with_top.nat_induction with n IH Itop,
   { intros m hm,
@@ -2294,14 +2301,51 @@ begin
       intros y hy,
       cases mem_set_of_eq.mp hy with y' hy',
       rw [← hy', inverse_unit],
-      exact @has_fderiv_at_inverse 𝕜 _ _ _ _ _ y' },
+      exact @has_fderiv_at_ring_inverse 𝕜 _ _ _ _ _ y' },
     { exact (lmul_left_right_is_bounded_bilinear 𝕜 R).times_cont_diff.neg.comp_times_cont_diff_at
         (x : R) (IH.prod IH) } },
   { exact times_cont_diff_at_top.mpr Itop }
 end
 
 end algebra_inverse
 
+/-! ### Inversion of continuous linear maps between Banach spaces -/
+
+section map_inverse
+open continuous_linear_map
+
+/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
+inversion is `C^n`, for all `n`. -/
+lemma times_cont_diff_at_map_inverse [complete_space E] {n : with_top ℕ} (e : E ≃L[𝕜] F) :
+  times_cont_diff_at 𝕜 n inverse (e : E →L[𝕜] F) :=
+begin
+  -- first, we use the lemma `to_ring_inverse` to rewrite in terms of `ring.inverse` in the ring
+  -- `E →L[𝕜] E`
+  let O₁ : (E →L[𝕜] E) → (F →L[𝕜] E) := λ f, f.comp (e.symm : (F →L[𝕜] E)),
+  let O₂ : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : (F →L[𝕜] E)).comp f,
+  have : continuous_linear_map.inverse = O₁ ∘ ring.inverse ∘ O₂,
+  { funext f,
+    rw to_ring_inverse e},
+  rw this,
+  -- `O₁` and `O₂` are `times_cont_diff`, so we reduce to proving that `ring.inverse` is `times_cont_diff`
+  have h₁ : times_cont_diff 𝕜 n O₁,
+  { exact is_bounded_bilinear_map_comp.times_cont_diff.comp (times_cont_diff_const.prod times_cont_diff_id) },
+  have h₂ : times_cont_diff 𝕜 n O₂,
+  { exact is_bounded_bilinear_map_comp.times_cont_diff.comp (times_cont_diff_id.prod times_cont_diff_const) },
+  refine h₁.times_cont_diff_at.comp _ (times_cont_diff_at.comp _ _ h₂.times_cont_diff_at),
+  -- this works differently depending on whether or not `E` is `nontrivial` (the condition for
+  -- `E →L[𝕜] E` to be a `normed_algebra`)
+  cases subsingleton_or_nontrivial E with _i _i; resetI,
+  { convert @times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (0 :  E →L[𝕜] E),
+    ext,
+    simp },
+  { convert times_cont_diff_at_ring_inverse 𝕜 (E →L[𝕜] E) 1,
+    simp [O₂],
+    refl },
+end
+
+end map_inverse
+
 section real
 /-!
 ### Results over `ℝ`

src/analysis/normed_space/operator_norm.lean

@@ -891,55 +891,6 @@ lemma coord_self (x : E) (h : x ≠ 0) :
   (coord 𝕜 x h) (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span 𝕜 ({x} : set E)) = 1 :=
 linear_equiv.coord_self 𝕜 E x h
 
-variable (E)
-
-/-- The continuous linear equivalences from `E` to itself form a group under composition. -/
-instance automorphism_group : group (E ≃L[𝕜] E) :=
-{ mul          := λ f g, g.trans f,
-  one          := continuous_linear_equiv.refl 𝕜 E,
-  inv          := λ f, f.symm,
-  mul_assoc    := λ f g h, by {ext, refl},
-  mul_one      := λ f, by {ext, refl},
-  one_mul      := λ f, by {ext, refl},
-  mul_left_inv := λ f, by {ext, exact f.left_inv x} }
-
-variables {𝕜 E}
-
-/-- An invertible continuous linear map `f` determines a continuous equivalence from `E` to itself.
--/
-def of_unit (f : units (E →L[𝕜] E)) : (E ≃L[𝕜] E) :=
-{ to_linear_equiv :=
-  { to_fun    := f.val,
-    map_add'  := by simp,
-    map_smul' := by simp,
-    inv_fun   := f.inv,
-    left_inv  := λ x, show (f.inv * f.val) x = x, by {rw f.inv_val, simp},
-    right_inv := λ x, show (f.val * f.inv) x = x, by {rw f.val_inv, simp}, },
-  continuous_to_fun  := f.val.continuous,
-  continuous_inv_fun := f.inv.continuous }
-
-/-- A continuous equivalence from `E` to itself determines an invertible continuous linear map. -/
-def to_unit (f : (E ≃L[𝕜] E)) : units (E →L[𝕜] E) :=
-{ val     := f,
-  inv     := f.symm,
-  val_inv := by {ext, simp},
-  inv_val := by {ext, simp} }
-
-variables (𝕜 E)
-
-/-- The units of the algebra of continuous `𝕜`-linear endomorphisms of `E` is multiplicatively
-equivalent to the type of continuous linear equivalences between `E` and itself. -/
-def units_equiv : units (E →L[𝕜] E) ≃* (E ≃L[𝕜] E) :=
-{ to_fun    := of_unit,
-  inv_fun   := to_unit,
-  left_inv  := λ f, by {ext, refl},
-  right_inv := λ f, by {ext, refl},
-  map_mul'  := λ x y, by {ext, refl} }
-
-@[simp] lemma units_equiv_to_continuous_linear_map
-  (f : units (E →L[𝕜] E)) :
-  (units_equiv 𝕜 E f : E →L[𝕜] E) = f := by {ext, refl}
-
 end continuous_linear_equiv
 
 lemma linear_equiv.uniform_embedding (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous e.symm) :

src/topology/algebra/module.lean

@@ -799,8 +799,19 @@ theorem bijective (e : M ≃L[R] M₂) : function.bijective e := e.to_linear_equ
 theorem injective (e : M ≃L[R] M₂) : function.injective e := e.to_linear_equiv.to_equiv.injective
 theorem surjective (e : M ≃L[R] M₂) : function.surjective e := e.to_linear_equiv.to_equiv.surjective
 
+@[simp] theorem trans_apply (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) (c : M) :
+  (e₁.trans e₂) c = e₂ (e₁ c) :=
+rfl
 @[simp] theorem apply_symm_apply (e : M ≃L[R] M₂) (c : M₂) : e (e.symm c) = c := e.1.6 c
 @[simp] theorem symm_apply_apply (e : M ≃L[R] M₂) (b : M) : e.symm (e b) = b := e.1.5 b
+@[simp] theorem symm_trans_apply (e₁ : M₂ ≃L[R] M) (e₂ : M₃ ≃L[R] M₂) (c : M) :
+  (e₂.trans e₁).symm c = e₂.symm (e₁.symm c) :=
+rfl
+
+@[simp, norm_cast]
+lemma comp_coe (f : M ≃L[R] M₂) (f' : M₂ ≃L[R] M₃) :
+  (f' : M₂ →L[R] M₃).comp (f : M →L[R] M₂) = (f.trans f' : M →L[R] M₃) :=
+rfl
 
 @[simp] theorem coe_comp_coe_symm (e : M ≃L[R] M₂) :
   (e : M →L[R] M₂).comp (e.symm : M₂ →L[R] M) = continuous_linear_map.id R M₂ :=
@@ -829,6 +840,10 @@ self_comp_symm e
 @[simp] theorem symm_symm (e : M ≃L[R] M₂) : e.symm.symm = e :=
 by { ext x, refl }
 
+@[simp] lemma refl_symm :
+ (continuous_linear_equiv.refl R M).symm = continuous_linear_equiv.refl R M :=
+rfl
+
 theorem symm_symm_apply (e : M ≃L[R] M₂) (x : M) : e.symm.symm x = e x :=
 rfl
 
@@ -859,6 +874,18 @@ rfl
   (equiv_of_inverse f₁ f₂ h₁ h₂).symm = equiv_of_inverse f₂ f₁ h₂ h₁ :=
 rfl
 
+variable (M)
+
+/-- The continuous linear equivalences from `M` to itself form a group under composition. -/
+instance automorphism_group : group (M ≃L[R] M) :=
+{ mul          := λ f g, g.trans f,
+  one          := continuous_linear_equiv.refl R M,
+  inv          := λ f, f.symm,
+  mul_assoc    := λ f g h, by {ext, refl},
+  mul_one      := λ f, by {ext, refl},
+  one_mul      := λ f, by {ext, refl},
+  mul_left_inv := λ f, by {ext, exact f.left_inv x} }
+
 end add_comm_monoid
 
 section add_comm_group
@@ -901,6 +928,47 @@ variables {R : Type*} [ring R]
 
 @[simp] lemma map_neg (e : M ≃L[R] M₂) (x : M) : e (-x) = -e x := (e : M →L[R] M₂).map_neg x
 
+section
+/-! The next theorems cover the identification between `M ≃L[𝕜] M`and the group of units of the ring
+`M →L[R] M`. -/
+variables [topological_add_group M]
+
+/-- An invertible continuous linear map `f` determines a continuous equivalence from `M` to itself.
+-/
+def of_unit (f : units (M →L[R] M)) : (M ≃L[R] M) :=
+{ to_linear_equiv :=
+  { to_fun    := f.val,
+    map_add'  := by simp,
+    map_smul' := by simp,
+    inv_fun   := f.inv,
+    left_inv  := λ x, show (f.inv * f.val) x = x, by {rw f.inv_val, simp},
+    right_inv := λ x, show (f.val * f.inv) x = x, by {rw f.val_inv, simp}, },
+  continuous_to_fun  := f.val.continuous,
+  continuous_inv_fun := f.inv.continuous }
+
+/-- A continuous equivalence from `M` to itself determines an invertible continuous linear map. -/
+def to_unit (f : (M ≃L[R] M)) : units (M →L[R] M) :=
+{ val     := f,
+  inv     := f.symm,
+  val_inv := by {ext, simp},
+  inv_val := by {ext, simp} }
+
+variables (R M)
+
+/-- The units of the algebra of continuous `R`-linear endomorphisms of `M` is multiplicatively
+equivalent to the type of continuous linear equivalences between `M` and itself. -/
+def units_equiv : units (M →L[R] M) ≃* (M ≃L[R] M) :=
+{ to_fun    := of_unit,
+  inv_fun   := to_unit,
+  left_inv  := λ f, by {ext, refl},
+  right_inv := λ f, by {ext, refl},
+  map_mul'  := λ x y, by {ext, refl} }
+
+@[simp] lemma units_equiv_apply (f : units (M →L[R] M)) (x : M) :
+  (units_equiv R M f) x = f x := rfl
+
+end
+
 section
 variables (R) [topological_space R] [topological_module R R]
 
@@ -958,6 +1026,87 @@ end ring
 
 end continuous_linear_equiv
 
+namespace continuous_linear_map
+
+open_locale classical
+
+variables {R : Type*} {M : Type*} {M₂ : Type*} [topological_space M] [topological_space M₂]
+
+section
+variables [semiring R]
+variables [add_comm_monoid M₂] [semimodule R M₂]
+variables [add_comm_monoid M] [semimodule R M]
+
+/-- Introduce a function `inverse` from `M →L[R] M₂` to `M₂ →L[R] M`, which sends `f` to `f.symm` if
+`f` is a continuous linear equivalence and to `0` otherwise.  This definition is somewhat ad hoc,
+but one needs a fully (rather than partially) defined inverse function for some purposes, including
+for calculus. -/
+noncomputable def inverse : (M →L[R] M₂) → (M₂ →L[R] M) :=
+λ f, if h : ∃ (e : M ≃L[R] M₂), (e : M →L[R] M₂) = f then ((classical.some h).symm : M₂ →L[R] M) else 0
+
+/-- By definition, if `f` is invertible then `inverse f = f.symm`. -/
+@[simp] lemma inverse_equiv (e : M ≃L[R] M₂) : inverse (e : M →L[R] M₂) = e.symm :=
+begin
+  have h : ∃ (e' : M ≃L[R] M₂), (e' : M →L[R] M₂) = ↑e := ⟨e, rfl⟩,
+  simp only [inverse, dif_pos h],
+  congr,
+  ext x,
+  have h' := classical.some_spec h,
+  simpa using continuous_linear_map.ext_iff.1 (h') x -- for some reason `h'` cannot be substituted here
+end
+
+/-- By definition, if `f` is not invertible then `inverse f = 0`. -/
+@[simp] lemma inverse_non_equiv (f : M →L[R] M₂) (h : ¬∃ (e' : M ≃L[R] M₂), ↑e' = f) :
+  inverse f = 0 :=
+dif_neg h
+
+end
+
+section
+variables [ring R]
+variables [add_comm_group M] [topological_add_group M] [module R M]
+variables [add_comm_group M₂] [module R M₂]
+
+@[simp] lemma ring_inverse_equiv (e : M ≃L[R] M) :
+  ring.inverse ↑e = inverse (e : M →L[R] M) :=
+begin
+  suffices :
+    ring.inverse ((((continuous_linear_equiv.units_equiv _ _).symm e) : M →L[R] M)) = inverse ↑e,
+  { convert this },
+  simp,
+  refl,
+end
+
+/-- The function `continuous_linear_equiv.inverse` can be written in terms of `ring.inverse` for the
+ring of self-maps of the domain. -/
+lemma to_ring_inverse (e : M ≃L[R] M₂) (f : M →L[R] M₂) :
+  inverse f = (ring.inverse ((e.symm : (M₂ →L[R] M)).comp f)).comp e.symm :=
+begin
+  by_cases h₁ : ∃ (e' : M ≃L[R] M₂), ↑e' = f,
+  { obtain ⟨e', he'⟩ := h₁,
+    rw ← he',
+    ext,
+    simp },
+  { suffices : ¬is_unit ((e.symm : M₂ →L[R] M).comp f),
+    { simp [this, h₁] },
+    revert h₁,
+    contrapose!,
+    rintros ⟨F, hF⟩,
+    use (continuous_linear_equiv.units_equiv _ _ F).trans e,
+    ext,
+    simp [hF] }
+end
+
+lemma ring_inverse_eq_map_inverse : ring.inverse = @inverse R M M _ _ _ _ _ _ _ :=
+begin
+  ext,
+  simp [to_ring_inverse (continuous_linear_equiv.refl R M)],
+end
+
+end
+
+end continuous_linear_map
+
 namespace submodule
 
 variables