feat(topology/metric_space/isometry): (pre)image of a (closed) ball o…

…r a sphere (#10813)

Also specialize for translations in a normed add torsor.

src/analysis/normed_space/add_torsor.lean

@@ -89,11 +89,52 @@ by simp [dist_eq_norm_vsub V _ x]
 @[simp] lemma dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ∥v∥ :=
 by rw [dist_comm, dist_vadd_left]
 
+/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
+addition/subtraction of `x : P`. -/
+@[simps] def isometric.vadd_const (x : P) : V ≃ᵢ P :=
+{ to_equiv := equiv.vadd_const x,
+  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_right _ _ _ }
+
+section
+
+variable (P)
+
+/-- Self-isometry of a (semi)normed add torsor given by addition of a constant vector `x`. -/
+@[simps] def isometric.const_vadd (x : V) : P ≃ᵢ P :=
+{ to_equiv := equiv.const_vadd P x,
+  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_left _ _ _ }
+
+end
+
 @[simp] lemma dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z :=
 by rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
 
+/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
+subtraction from `x : P`. -/
+@[simps] def isometric.const_vsub (x : P) : P ≃ᵢ V :=
+{ to_equiv := equiv.const_vsub x,
+  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_vsub_cancel_left _ _ _ }
+
 @[simp] lemma dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
-by rw [dist_eq_norm, vsub_sub_vsub_cancel_right, dist_eq_norm_vsub V]
+(isometric.vadd_const z).symm.dist_eq x y
+
+section pointwise
+
+open_locale pointwise
+
+@[simp] lemma vadd_ball (x : V) (y : P) (r : ℝ) :
+  x +ᵥ metric.ball y r = metric.ball (x +ᵥ y) r :=
+(isometric.const_vadd P x).image_ball y r
+
+@[simp] lemma vadd_closed_ball (x : V) (y : P) (r : ℝ) :
+  x +ᵥ metric.closed_ball y r = metric.closed_ball (x +ᵥ y) r :=
+(isometric.const_vadd P x).image_closed_ball y r
+
+@[simp] lemma vadd_sphere (x : V) (y : P) (r : ℝ) :
+  x +ᵥ metric.sphere y r = metric.sphere (x +ᵥ y) r :=
+(isometric.const_vadd P x).image_sphere y r
+
+end pointwise
 
 lemma dist_vadd_vadd_le (v v' : V) (p p' : P) :
   dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' :=

src/analysis/normed_space/mazur_ulam.lean

@@ -135,8 +135,8 @@ def to_real_linear_isometry_equiv (f : E ≃ᵢ F) : E ≃ₗᵢ[ℝ] F :=
 normed vector spaces over `ℝ`, then `f` is an affine isometry equivalence. -/
 def to_real_affine_isometry_equiv (f : PE ≃ᵢ PF) : PE ≃ᵃⁱ[ℝ] PF :=
 affine_isometry_equiv.mk' f
-  (((vadd_const ℝ (classical.arbitrary PE)).to_isometric.trans $ f.trans
-    (vadd_const ℝ (f $ classical.arbitrary PE)).to_isometric.symm).to_real_linear_isometry_equiv)
+  (((vadd_const (classical.arbitrary PE)).trans $ f.trans
+    (vadd_const (f $ classical.arbitrary PE)).symm).to_real_linear_isometry_equiv)
   (classical.arbitrary PE) (λ p, by simp)
 
 @[simp] lemma coe_fn_to_real_affine_isometry_equiv (f : PE ≃ᵢ PF) :

src/topology/metric_space/isometry.lean

@@ -23,7 +23,7 @@ universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 open function set
-open_locale topological_space
+open_locale topological_space ennreal
 
 /-- An isometry (also known as isometric embedding) is a map preserving the edistance
 between pseudoemetric spaces, or equivalently the distance between pseudometric space.  -/
@@ -81,6 +81,11 @@ theorem isometry.uniform_inducing (hf : isometry f) :
   uniform_inducing f :=
 hf.antilipschitz.uniform_inducing hf.lipschitz.uniform_continuous
 
+lemma isometry.tendsto_nhds_iff {ι : Type*} {f : α → β}
+  {g : ι → α} {a : filter ι} {b : α} (hf : isometry f) :
+  filter.tendsto g a (𝓝 b) ↔ filter.tendsto (f ∘ g) a (𝓝 (f b)) :=
+hf.uniform_inducing.inducing.tendsto_nhds_iff
+
 /-- An isometry is continuous. -/
 lemma isometry.continuous (hf : isometry f) : continuous f :=
 hf.lipschitz.continuous
@@ -100,6 +105,14 @@ lemma isometry.ediam_range (hf : isometry f) :
   emetric.diam (range f) = emetric.diam (univ : set α) :=
 by { rw ← image_univ, exact hf.ediam_image univ }
 
+lemma isometry.maps_to_emetric_ball (hf : isometry f) (x : α) (r : ℝ≥0∞) :
+  maps_to f (emetric.ball x r) (emetric.ball (f x) r) :=
+λ y hy, by rwa [emetric.mem_ball, hf]
+
+lemma isometry.maps_to_emetric_closed_ball (hf : isometry f) (x : α) (r : ℝ≥0∞) :
+  maps_to f (emetric.closed_ball x r) (emetric.closed_ball (f x) r) :=
+λ y hy, by rwa [emetric.mem_closed_ball, hf]
+
 /-- The injection from a subtype is an isometry -/
 lemma isometry_subtype_coe {s : set α} : isometry (coe : s → α) :=
 λx y, rfl
@@ -133,22 +146,33 @@ theorem isometry.closed_embedding [complete_space α] [emetric_space β]
   {f : α → β} (hf : isometry f) : closed_embedding f :=
 hf.antilipschitz.closed_embedding hf.lipschitz.uniform_continuous
 
-lemma isometry.tendsto_nhds_iff [emetric_space β] {ι : Type*} {f : α → β}
-  {g : ι → α} {a : filter ι} {b : α} (hf : isometry f) :
-  filter.tendsto g a (𝓝 b) ↔ filter.tendsto (f ∘ g) a (𝓝 (f b)) :=
-hf.embedding.tendsto_nhds_iff
-
 end emetric_isometry --section
 
+namespace isometry
+
+variables [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β}
+
 /-- An isometry preserves the diameter in pseudometric spaces. -/
-lemma isometry.diam_image [pseudo_metric_space α] [pseudo_metric_space β]
-  {f : α → β} (hf : isometry f) (s : set α) : metric.diam (f '' s) = metric.diam s :=
+lemma diam_image (hf : isometry f) (s : set α) : metric.diam (f '' s) = metric.diam s :=
 by rw [metric.diam, metric.diam, hf.ediam_image]
 
-lemma isometry.diam_range [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β}
-  (hf : isometry f) : metric.diam (range f) = metric.diam (univ : set α) :=
+lemma diam_range (hf : isometry f) : metric.diam (range f) = metric.diam (univ : set α) :=
 by { rw ← image_univ, exact hf.diam_image univ }
 
+lemma maps_to_ball (hf : isometry f) (x : α) (r : ℝ) :
+  maps_to f (metric.ball x r) (metric.ball (f x) r) :=
+λ y hy, by rwa [metric.mem_ball, hf.dist_eq]
+
+lemma maps_to_sphere (hf : isometry f) (x : α) (r : ℝ) :
+  maps_to f (metric.sphere x r) (metric.sphere (f x) r) :=
+λ y hy, by rwa [metric.mem_sphere, hf.dist_eq]
+
+lemma maps_to_closed_ball (hf : isometry f) (x : α) (r : ℝ) :
+  maps_to f (metric.closed_ball x r) (metric.closed_ball (f x) r) :=
+λ y hy, by rwa [metric.mem_closed_ball, hf.dist_eq]
+
+end isometry
+
 /-- `α` and `β` are isometric if there is an isometric bijection between them. -/
 @[nolint has_inhabited_instance] -- such a bijection need not exist
 structure isometric (α : Type*) (β : Type*) [pseudo_emetric_space α] [pseudo_emetric_space β]
@@ -267,6 +291,22 @@ by rw [← h.range_eq_univ, h.isometry.ediam_range]
 @[simp] lemma ediam_preimage (h : α ≃ᵢ β) (s : set β) : emetric.diam (h ⁻¹' s) = emetric.diam s :=
 by rw [← image_symm, ediam_image]
 
+@[simp] lemma preimage_emetric_ball (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
+  h ⁻¹' (emetric.ball x r) = emetric.ball (h.symm x) r :=
+by { ext y, simp [← h.edist_eq] }
+
+@[simp] lemma preimage_emetric_closed_ball (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
+  h ⁻¹' (emetric.closed_ball x r) = emetric.closed_ball (h.symm x) r :=
+by { ext y, simp [← h.edist_eq] }
+
+@[simp] lemma image_emetric_ball (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
+  h '' (emetric.ball x r) = emetric.ball (h x) r :=
+by rw [← h.preimage_symm, h.symm.preimage_emetric_ball, symm_symm]
+
+@[simp] lemma image_emetric_closed_ball (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
+  h '' (emetric.closed_ball x r) = emetric.closed_ball (h x) r :=
+by rw [← h.preimage_symm, h.symm.preimage_emetric_closed_ball, symm_symm]
+
 /-- The (bundled) homeomorphism associated to an isometric isomorphism. -/
 @[simps to_equiv] protected def to_homeomorph (h : α ≃ᵢ β) : α ≃ₜ β :=
 { continuous_to_fun  := h.continuous,
@@ -332,6 +372,30 @@ by rw [← image_symm, diam_image]
 lemma diam_univ : metric.diam (univ : set α) = metric.diam (univ : set β) :=
 congr_arg ennreal.to_real h.ediam_univ
 
+@[simp] lemma preimage_ball (h : α ≃ᵢ β) (x : β) (r : ℝ) :
+  h ⁻¹' (metric.ball x r) = metric.ball (h.symm x) r :=
+by { ext y, simp [← h.dist_eq] }
+
+@[simp] lemma preimage_sphere (h : α ≃ᵢ β) (x : β) (r : ℝ) :
+  h ⁻¹' (metric.sphere x r) = metric.sphere (h.symm x) r :=
+by { ext y, simp [← h.dist_eq] }
+
+@[simp] lemma preimage_closed_ball (h : α ≃ᵢ β) (x : β) (r : ℝ) :
+  h ⁻¹' (metric.closed_ball x r) = metric.closed_ball (h.symm x) r :=
+by { ext y, simp [← h.dist_eq] }
+
+@[simp] lemma image_ball (h : α ≃ᵢ β) (x : α) (r : ℝ) :
+  h '' (metric.ball x r) = metric.ball (h x) r :=
+by rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
+
+@[simp] lemma image_sphere (h : α ≃ᵢ β) (x : α) (r : ℝ) :
+  h '' (metric.sphere x r) = metric.sphere (h x) r :=
+by rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
+
+@[simp] lemma image_closed_ball (h : α ≃ᵢ β) (x : α) (r : ℝ) :
+  h '' (metric.closed_ball x r) = metric.closed_ball (h x) r :=
+by rw [← h.preimage_symm, h.symm.preimage_closed_ball, symm_symm]
+
 end pseudo_metric_space
 
 end isometric