refactor: rename/redefine homeomorphUnitBall (#6030)

* Add `Equiv.toLocalEquivOfImageEq`
  and `Homeomorph.toLocalHomeomorphOfImageEq`.
* Rename `homeomorphUnitBall` to `Homeomorph.unitBall`.
* Add `LocalHomeomorph.univUnitBall`,
  a `LocalHomeomorph` version of `Homeomorph.unitBall`.
* Add `LocalHomeomorph.unitBallBall` and `LocalHomeomorph.univBall`.

Inspired by a definition from the sphere eversion project.

Mathlib.lean

@@ -729,6 +729,7 @@ import Mathlib.Analysis.NormedSpace.Extr
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+import Mathlib.Analysis.NormedSpace.HomeomorphBall
 import Mathlib.Analysis.NormedSpace.IndicatorFunction
 import Mathlib.Analysis.NormedSpace.Int
 import Mathlib.Analysis.NormedSpace.IsROrC

Mathlib/Analysis/InnerProductSpace/Calculus.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.SpecialFunctions.Sqrt
+import Mathlib.Analysis.NormedSpace.HomeomorphBall
 
 #align_import analysis.inner_product_space.calculus from "leanprover-community/mathlib"@"f9dd3204df14a0749cd456fac1e6849dfe7d2b88"
 
@@ -369,29 +370,56 @@ open Metric hiding mem_nhds_iff
 
 variable {n : ℕ∞} {E : Type _} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
-theorem contDiff_homeomorphUnitBall : ContDiff ℝ n fun x : E => (homeomorphUnitBall x : E) := by
-  suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ by exact this.smul contDiff_id
+theorem LocalHomeomorph.contDiff_univUnitBall : ContDiff ℝ n (univUnitBall : E → E) := by
+  suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ from this.smul contDiff_id
   have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
   refine' ContDiff.inv _ fun x => Real.sqrt_ne_zero'.mpr (h x)
   exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'
-#align cont_diff_homeomorph_unit_ball contDiff_homeomorphUnitBall
 
-theorem contDiffOn_homeomorphUnitBall_symm {f : E → E}
-    (h : ∀ (y) (hy : y ∈ ball (0 : E) 1), f y = homeomorphUnitBall.symm ⟨y, hy⟩) :
-    ContDiffOn ℝ n f <| ball 0 1 := fun y hy ↦ by
+theorem LocalHomeomorph.contDiffOn_univUnitBall_symm :
+    ContDiffOn ℝ n univUnitBall.symm (ball (0 : E) 1) := fun y hy ↦ by
   apply ContDiffAt.contDiffWithinAt
-  have hf : f =ᶠ[𝓝 y] fun y => ((1 : ℝ) - ‖(y : E)‖ ^ 2).sqrt⁻¹ • (y : E) := by
-    filter_upwards [isOpen_ball.mem_nhds hy] with z hz
-    rw [h z hz]
-    rfl
-  refine' ContDiffAt.congr_of_eventuallyEq _ hf
-  suffices ContDiffAt ℝ n (fun y => ((1 : ℝ) - ‖(y : E)‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id
+  suffices ContDiffAt ℝ n (fun y : E => ((1 : ℝ) - ‖y‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id
   have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
     rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
   refine' ContDiffAt.inv _ (Real.sqrt_ne_zero'.mpr h)
   refine' (contDiffAt_sqrt h.ne').comp y _
   exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt
-#align cont_diff_on_homeomorph_unit_ball_symm contDiffOn_homeomorphUnitBall_symm
 
-end DiffeomorphUnitBall
+theorem Homeomorph.contDiff_unitBall : ContDiff ℝ n fun x : E => (unitBall x : E) :=
+  LocalHomeomorph.contDiff_univUnitBall
+#align cont_diff_homeomorph_unit_ball Homeomorph.contDiff_unitBall
+
+@[deprecated LocalHomeomorph.contDiffOn_univUnitBall_symm]
+theorem Homeomorph.contDiffOn_unitBall_symm {f : E → E}
+    (h : ∀ (y) (hy : y ∈ ball (0 : E) 1), f y = Homeomorph.unitBall.symm ⟨y, hy⟩) :
+    ContDiffOn ℝ n f <| ball 0 1 :=
+  LocalHomeomorph.contDiffOn_univUnitBall_symm.congr h
+#align cont_diff_on_homeomorph_unit_ball_symm Homeomorph.contDiffOn_unitBall_symm
+
+namespace LocalHomeomorph
+
+variable {c : E} {r : ℝ}
+
+theorem contDiff_unitBallBall (hr : 0 < r) : ContDiff ℝ n (unitBallBall c r hr) :=
+  (contDiff_id.const_smul _).add contDiff_const
 
+theorem contDiff_unitBallBall_symm (hr : 0 < r) : ContDiff ℝ n (unitBallBall c r hr).symm :=
+  (contDiff_id.sub contDiff_const).const_smul _
+
+theorem contDiff_univBall : ContDiff ℝ n (univBall c r) := by
+  unfold univBall; split_ifs with h
+  · exact (contDiff_unitBallBall h).comp contDiff_univUnitBall
+  · exact contDiff_id.add contDiff_const
+
+theorem contDiffOn_univBall_symm :
+    ContDiffOn ℝ n (univBall c r).symm (ball c r) := by
+  unfold univBall; split_ifs with h
+  · refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
+    rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
+    apply LocalHomeomorph.symm_mapsTo
+  · exact contDiffOn_id.sub contDiffOn_const
+
+end LocalHomeomorph
+
+end DiffeomorphUnitBall

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -177,52 +177,6 @@ instance {E : Type _} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
       Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ←
       @Int.cast_one ℝ _, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]
 
-/-- A (semi) normed real vector space is homeomorphic to the unit ball in the same space.
-This homeomorphism sends `x : E` to `(1 + ‖x‖²)^(- ½) • x`.
-
-In many cases the actual implementation is not important, so we don't mark the projection lemmas
-`homeomorphUnitBall_apply_coe` and `homeomorphUnitBall_symm_apply` as `@[simp]`.
-
-See also `contDiff_homeomorphUnitBall` and `contDiffOn_homeomorphUnitBall_symm` for
-smoothness properties that hold when `E` is an inner-product space. -/
-@[simps (config := { isSimp := false })]
-noncomputable def homeomorphUnitBall [NormedSpace ℝ E] : E ≃ₜ ball (0 : E) 1 where
-  toFun x :=
-    ⟨(1 + ‖x‖ ^ 2).sqrt⁻¹ • x, by
-      have : 0 < 1 + ‖x‖ ^ 2 := by positivity
-      rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
-        div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq,
-        abs_norm, Real.sq_sqrt this.le]
-      exact lt_one_add _⟩
-  invFun y := (1 - ‖(y : E)‖ ^ 2).sqrt⁻¹ • (y : E)
-  left_inv x := by
-    field_simp [norm_smul, smul_smul, (zero_lt_one_add_norm_sq x).ne', sq_abs,
-      Real.sq_sqrt (zero_lt_one_add_norm_sq x).le, ← Real.sqrt_div (zero_lt_one_add_norm_sq x).le]
-  right_inv y := by
-    have : 0 < 1 - ‖(y : E)‖ ^ 2 := by
-      nlinarith [norm_nonneg (y : E), (mem_ball_zero_iff.1 y.2 : ‖(y : E)‖ < 1)]
-    field_simp [norm_smul, smul_smul, this.ne', sq_abs, Real.sq_sqrt this.le,
-      ← Real.sqrt_div this.le]
-  continuous_toFun := by
-    suffices : Continuous fun (x:E) => (1 + ‖x‖ ^ 2).sqrt⁻¹;
-    exact (this.smul continuous_id).subtype_mk _
-    refine' Continuous.inv₀ _ fun x => Real.sqrt_ne_zero'.mpr (by positivity)
-    continuity
-  continuous_invFun := by
-    suffices ∀ y : ball (0 : E) 1, (1 - ‖(y : E)‖ ^ 2).sqrt ≠ 0 by
-      apply Continuous.smul (Continuous.inv₀
-        (continuous_const.sub ?_).sqrt this) continuous_induced_dom
-      continuity -- Porting note: was just this tactic for `suffices`
-    intro y
-    rw [Real.sqrt_ne_zero']
-    nlinarith [norm_nonneg (y : E), (mem_ball_zero_iff.1 y.2 : ‖(y : E)‖ < 1)]
-#align homeomorph_unit_ball homeomorphUnitBall
-
-@[simp]
-theorem coe_homeomorphUnitBall_apply_zero [NormedSpace ℝ E] :
-    (homeomorphUnitBall (0 : E) : E) = 0 := by simp [homeomorphUnitBall_apply_coe]
-#align coe_homeomorph_unit_ball_apply_zero coe_homeomorphUnitBall_apply_zero
-
 open NormedField
 
 instance ULift.normedSpace : NormedSpace α (ULift E) :=

Mathlib/Analysis/NormedSpace/HomeomorphBall.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Oliver Nash
+-/
+import Mathlib.Topology.LocalHomeomorph
+import Mathlib.Analysis.NormedSpace.AddTorsor
+import Mathlib.Analysis.NormedSpace.Pointwise
+
+#align_import analysis.normed_space.basic from "leanprover-community/mathlib"@"bc91ed7093bf098d253401e69df601fc33dde156"
+
+/-!
+# (Local) homeomorphism between a normed space and a ball
+
+In this file we show that a real (semi)normed vector space is homeomorphic to the unit ball.
+
+We formalize it in two ways:
+
+- as a `Homeomorph`, see `Homeomorph.unitBall`;
+- as a `LocalHomeomorph` with `source = Set.univ` and `target = Metric.ball (0 : E) 1`.
+
+While the former approach is more natural, the latter approach provides us
+with a globally defined inverse function which makes it easier to say
+that this homeomorphism is in fact a diffeomorphism.
+
+We also show that the unit ball `Metric.ball (0 : E) 1` is homeomorphic
+to a ball of positive radius in an affine space over `E`, see `LocalHomeomorph.unitBallBall`.
+
+## Tags
+
+homeomorphism, ball
+-/
+
+open Set Metric Pointwise
+variable {E : Type _} [SeminormedAddCommGroup E] [NormedSpace ℝ E]
+
+noncomputable section
+
+/-- Local homeomorphism between a real (semi)normed space and the unit ball.
+See also `Homeomorph.unitBall`. -/
+@[simps (config := .lemmasOnly)]
+def LocalHomeomorph.univUnitBall : LocalHomeomorph E E where
+  toFun x := (1 + ‖x‖ ^ 2).sqrt⁻¹ • x
+  invFun y := (1 - ‖(y : E)‖ ^ 2).sqrt⁻¹ • (y : E)
+  source := univ
+  target := ball 0 1
+  map_source' x _ := by
+    have : 0 < 1 + ‖x‖ ^ 2 := by positivity
+    rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
+      div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq,
+      abs_norm, Real.sq_sqrt this.le]
+    exact lt_one_add _
+  map_target' _ _ := trivial
+  left_inv' x _ := by
+    field_simp [norm_smul, smul_smul, (zero_lt_one_add_norm_sq x).ne', sq_abs,
+      Real.sq_sqrt (zero_lt_one_add_norm_sq x).le, ← Real.sqrt_div (zero_lt_one_add_norm_sq x).le]
+  right_inv' y hy := by
+    have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
+    field_simp [norm_smul, smul_smul, this.ne', sq_abs, Real.sq_sqrt this.le,
+      ← Real.sqrt_div this.le]
+  open_source := isOpen_univ
+  open_target := isOpen_ball
+  continuous_toFun := by
+    suffices Continuous fun (x:E) => (1 + ‖x‖ ^ 2).sqrt⁻¹
+     from (this.smul continuous_id).continuousOn
+    refine' Continuous.inv₀ _ fun x => Real.sqrt_ne_zero'.mpr (by positivity)
+    continuity
+  continuous_invFun := by
+    have : ∀ y ∈ ball (0 : E) 1, (1 - ‖(y : E)‖ ^ 2).sqrt ≠ 0 := fun y hy ↦ by
+      rw [Real.sqrt_ne_zero']
+      nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
+    exact ContinuousOn.smul (ContinuousOn.inv₀
+      (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this) continuousOn_id
+
+@[simp]
+theorem LocalHomeomorph.univUnitBall_apply_zero : univUnitBall (0 : E) = 0 := by
+  simp [LocalHomeomorph.univUnitBall_apply]
+
+@[simp]
+theorem LocalHomeomorph.univUnitBall_symm_apply_zero : univUnitBall.symm (0 : E) = 0 := by
+  simp [LocalHomeomorph.univUnitBall_symm_apply]
+
+/-- A (semi) normed real vector space is homeomorphic to the unit ball in the same space.
+This homeomorphism sends `x : E` to `(1 + ‖x‖²)^(- ½) • x`.
+
+In many cases the actual implementation is not important, so we don't mark the projection lemmas
+`Homeomorph.unitBall_apply_coe` and `Homeomorph.unitBall_symm_apply` as `@[simp]`.
+
+See also `Homeomorph.contDiff_unitBall` and `LocalHomeomorph.contDiffOn_unitBall_symm`
+for smoothness properties that hold when `E` is an inner-product space. -/
+@[simps! (config := .lemmasOnly)]
+def Homeomorph.unitBall : E ≃ₜ ball (0 : E) 1 :=
+  (Homeomorph.Set.univ _).symm.trans LocalHomeomorph.univUnitBall.toHomeomorphSourceTarget
+#align homeomorph_unit_ball Homeomorph.unitBall
+
+@[simp]
+theorem Homeomorph.coe_unitBall_apply_zero :
+    (Homeomorph.unitBall (0 : E) : E) = 0 :=
+  LocalHomeomorph.univUnitBall_apply_zero
+#align coe_homeomorph_unit_ball_apply_zero Homeomorph.coe_unitBall_apply_zero
+
+variable {P : Type _} [PseudoMetricSpace P] [NormedAddTorsor E P]
+
+namespace LocalHomeomorph
+
+/-- Affine homeomorphism `(r • · +ᵥ c)` between a normed space and an add torsor over this space,
+interpreted as a `LocalHomeomorph` between `Metric.ball 0 1` and `Metric.ball c r`. -/
+@[simps!]
+def unitBallBall (c : P) (r : ℝ) (hr : 0 < r) : LocalHomeomorph E P :=
+  ((Homeomorph.smulOfNeZero r hr.ne').trans
+      (IsometryEquiv.vaddConst c).toHomeomorph).toLocalHomeomorphOfImageEq
+      (ball 0 1) isOpen_ball (ball c r) <| by
+    change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
+    rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
+    simp [abs_of_pos hr]
+
+/-- If `r > 0`, then `LocalHomeomorph.univBall c r` is a smooth local homeomorphism
+with `source = Set.univ` and `target = Metric.ball c r`.
+Otherwise, it is the translation by `c`.
+Thus in all cases, it sends `0` to `c`, see `LocalHomeomorph.univBall_apply_zero`. -/ 
+def univBall (c : P) (r : ℝ) : LocalHomeomorph E P :=
+  if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) rfl
+  else (IsometryEquiv.vaddConst c).toHomeomorph.toLocalHomeomorph
+
+@[simp]
+theorem univBall_source (c : P) (r : ℝ) : (univBall c r).source = univ := by
+  unfold univBall; split_ifs <;> rfl
+
+theorem univBall_target (c : P) {r : ℝ} (hr : 0 < r) : (univBall c r).target = ball c r := by
+  rw [univBall, dif_pos hr]; rfl
+
+theorem ball_subset_univBall_target (c : P) (r : ℝ) : ball c r ⊆ (univBall c r).target := by
+  by_cases hr : 0 < r
+  · rw [univBall_target c hr]
+  · rw [univBall, dif_neg hr]
+    exact subset_univ _
+
+@[simp]
+theorem univBall_apply_zero (c : P) (r : ℝ) : univBall c r 0 = c := by
+  unfold univBall; split_ifs <;> simp
+
+@[simp]
+theorem univBall_symm_apply_center (c : P) (r : ℝ) : (univBall c r).symm c = 0 := by
+  have : 0 ∈ (univBall c r).source := by simp
+  simpa only [univBall_apply_zero] using (univBall c r).left_inv this
+
+@[continuity]
+theorem continuous_univBall (c : P) (r : ℝ) : Continuous (univBall c r) := by
+  simpa [continuous_iff_continuousOn_univ] using (univBall c r).continuousOn
+
+theorem continuousOn_univBall_symm (c : P) (r : ℝ) : ContinuousOn (univBall c r).symm (ball c r) :=
+  (univBall c r).symm.continuousOn.mono <| ball_subset_univBall_target c r

Mathlib/Logic/Equiv/LocalEquiv.lean

@@ -244,17 +244,27 @@ protected theorem surjOn : SurjOn e e.source e.target :=
   e.bijOn.surjOn
 #align local_equiv.surj_on LocalEquiv.surjOn
 
-/-- Associate a `LocalEquiv` to an `Equiv`. -/
-@[simps (config := mfld_cfg)]
-def _root_.Equiv.toLocalEquiv (e : α ≃ β) : LocalEquiv α β where
+/-- Interpret an `Equiv` as a `LocalEquiv` by restricting it to `s` in the domain
+and to `t` in the codomain. -/
+@[simps (config := .asFn)]
+def _root_.Equiv.toLocalEquivOfImageEq (e : α ≃ β) (s : Set α) (t : Set β) (h : e '' s = t) :
+    LocalEquiv α β where
   toFun := e
   invFun := e.symm
-  source := univ
-  target := univ
-  map_source' _ _ := mem_univ _
-  map_target' _ _ := mem_univ _
-  left_inv' x _ := e.left_inv x
-  right_inv' x _ := e.right_inv x
+  source := s
+  target := t
+  map_source' x hx := h ▸ mem_image_of_mem _ hx
+  map_target' x hx := by
+    subst t
+    rcases hx with ⟨x, hx, rfl⟩
+    rwa [e.symm_apply_apply]
+  left_inv' x _ := e.symm_apply_apply x
+  right_inv' x _ := e.apply_symm_apply x
+
+/-- Associate a `LocalEquiv` to an `Equiv`. -/
+@[simps! (config := mfld_cfg)]
+def _root_.Equiv.toLocalEquiv (e : α ≃ β) : LocalEquiv α β :=
+  e.toLocalEquivOfImageEq univ univ <| by rw [image_univ, e.surjective.range_eq]
 #align equiv.to_local_equiv Equiv.toLocalEquiv
 #align equiv.to_local_equiv_symm_apply Equiv.toLocalEquiv_symm_apply
 #align equiv.to_local_equiv_target Equiv.toLocalEquiv_target

Mathlib/Topology/LocalHomeomorph.lean

@@ -194,14 +194,22 @@ protected theorem surjOn : SurjOn e e.source e.target :=
   e.bijOn.surjOn
 #align local_homeomorph.surj_on LocalHomeomorph.surjOn
 
-/-- A homeomorphism induces a local homeomorphism on the whole space -/
-@[simps! (config := mfld_cfg)]
-def _root_.Homeomorph.toLocalHomeomorph (e : α ≃ₜ β) : LocalHomeomorph α β where
-  toLocalEquiv := e.toEquiv.toLocalEquiv
-  open_source := isOpen_univ
-  open_target := isOpen_univ
+/-- Interpret a `Homeomorph` as a `LocalHomeomorph` by restricting it
+to an open set `s` in the domain and to `t` in the codomain. -/
+@[simps! (config := .asFn) apply symm_apply toLocalEquiv,
+  simps! (config := .lemmasOnly) source target]
+def _root_.Homeomorph.toLocalHomeomorphOfImageEq (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s)
+    (t : Set β) (h : e '' s = t) : LocalHomeomorph α β where
+  toLocalEquiv := e.toLocalEquivOfImageEq s t h
+  open_source := hs
+  open_target := by simpa [← h]
   continuous_toFun := e.continuous.continuousOn
   continuous_invFun := e.symm.continuous.continuousOn
+
+/-- A homeomorphism induces a local homeomorphism on the whole space -/
+@[simps! (config := mfld_cfg)]
+def _root_.Homeomorph.toLocalHomeomorph (e : α ≃ₜ β) : LocalHomeomorph α β :=
+  e.toLocalHomeomorphOfImageEq univ isOpen_univ univ <| by rw [image_univ, e.surjective.range_eq]
 #align homeomorph.to_local_homeomorph Homeomorph.toLocalHomeomorph
 
 /-- Replace `toLocalEquiv` field to provide better definitional equalities. -/