refactor(*): midpoint, point_reflection, and Mazur-Ulam in affine spaces (#4752)

* redefine `midpoint` for points in an affine space;
* redefine `point_reflection` for affine spaces (as `equiv`,
  `affine_equiv`, and `isometric`);
* define `const_vsub` as `equiv`, `affine_equiv`, and `isometric`;
* define `affine_map.of_map_midpoint`;
* fully migrate the proof of Mazur-Ulam theorem to affine spaces;

Author: urkud

src/algebra/add_torsor.lean

@@ -437,6 +437,17 @@ def vadd_const (p : P) : G ≃ P :=
 
 @[simp] lemma coe_vadd_const_symm (p : P) : ⇑(vadd_const p).symm = λ p', p' -ᵥ p := rfl
 
+/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
+def const_vsub (p : P) : P ≃ G :=
+{ to_fun := (-ᵥ) p,
+  inv_fun := λ v, -v +ᵥ p,
+  left_inv := λ p', by simp,
+  right_inv := λ v, by simp [vsub_vadd_eq_vsub_sub] }
+
+@[simp] lemma coe_const_vsub (p : P) : ⇑(const_vsub p) = (-ᵥ) p := rfl
+
+@[simp] lemma coe_const_vsub_symm (p : P) : ⇑(const_vsub p).symm = λ v, -v +ᵥ p := rfl
+
 variables (P)
 
 /-- The permutation given by `p ↦ v +ᵥ p`. -/
@@ -464,4 +475,38 @@ def const_vadd_hom : multiplicative G →* equiv.perm P :=
   map_one' := const_vadd_zero G P,
   map_mul' := const_vadd_add P }
 
+variable {P}
+
+open function
+
+/-- Point reflection in `x` as a permutation. -/
+def point_reflection (x : P) : perm P := (const_vsub x).trans (vadd_const x)
+
+lemma point_reflection_apply (x y : P) : point_reflection x y = x -ᵥ y +ᵥ x := rfl
+
+@[simp] lemma point_reflection_symm (x : P) : (point_reflection x).symm = point_reflection x :=
+ext $ by simp [point_reflection]
+
+@[simp] lemma point_reflection_self (x : P) : point_reflection x x = x := vsub_vadd _ _
+
+lemma point_reflection_involutive (x : P) : involutive (point_reflection x : P → P) :=
+λ y, (equiv.apply_eq_iff_eq_symm_apply _).2 $ by rw point_reflection_symm
+
+/-- `x` is the only fixed point of `point_reflection x`. This lemma requires
+`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument. -/
+lemma point_reflection_fixed_iff_of_injective_bit0 {x y : P} (h : injective (bit0 : G → G)) :
+  point_reflection x y = y ↔ y = x :=
+by rw [point_reflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
+  neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
+
+omit G
+
+lemma injective_point_reflection_left_of_injective_bit0 {G P : Type*} [add_comm_group G]
+  [add_torsor G P] (h : injective (bit0 : G → G)) (y : P) :
+  injective (λ x : P, point_reflection x y) :=
+λ x₁ x₂ (hy : point_reflection x₁ y = point_reflection x₂ y),
+  by rwa [point_reflection_apply, point_reflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
+    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero,
+    h.eq_iff, vsub_eq_zero_iff_eq] at hy
+
 end equiv

src/algebra/invertible.lean

@@ -125,6 +125,10 @@ def invertible_neg [ring α] (a : α) [invertible a] : invertible (-a) :=
 @[simp] lemma inv_of_neg [ring α] (a : α) [invertible a] [invertible (-a)] : ⅟(-a) = -⅟a :=
 inv_of_eq_right_inv (by simp)
 
+@[simp] lemma one_sub_inv_of_two [ring α] [invertible (2:α)] : 1 - (⅟2:α) = ⅟2 :=
+(is_unit_of_invertible (2:α)).mul_right_inj.1 $
+  by rw [mul_sub, mul_inv_of_self, mul_one, bit0, add_sub_cancel]
+
 /-- `a` is the inverse of `⅟a`. -/
 instance invertible_inv_of [has_one α] [has_mul α] {a : α} [invertible a] : invertible (⅟a) :=
 ⟨ a, mul_inv_of_self a, inv_of_mul_self a ⟩

src/algebra/midpoint.lean

@@ -60,6 +60,8 @@ variables (R)
 
 theorem two_smul : (2 : R) • x = x + x := by rw [bit0, add_smul, one_smul]
 
+theorem two_smul' : (2 : R) • x = bit0 x := two_smul R x
+
 /-- Pullback a `semimodule` structure along an injective additive monoid homomorphism. -/
 protected def function.injective.semimodule [add_comm_monoid M₂] [has_scalar R M₂] (f : M₂ →+ M)
   (hf : injective f) (smul : ∀ (c : R) x, f (c • x) = c • f x) :

src/algebra/module/basic.lean

@@ -3,8 +3,9 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Yury Kudryashov.
 -/
-import algebra.add_torsor
+import linear_algebra.affine_space.midpoint
 import topology.metric_space.isometry
+import topology.instances.real_vector_space
 
 /-!
 # Torsors of additive normed group actions.
@@ -122,6 +123,14 @@ def vadd_const (p : P) : V ≃ᵢ P :=
 
 @[simp] lemma vadd_const_to_equiv (p : P) : (vadd_const p).to_equiv = equiv.vadd_const p := rfl
 
+/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
+def const_vsub (p : P) : P ≃ᵢ V :=
+⟨equiv.const_vsub p, isometry_emetric_iff_metric.2 $ λ p₁ p₂, dist_vsub_cancel_left _ _ _⟩
+
+@[simp] lemma coe_const_vsub (p : P) : ⇑(const_vsub p) = (-ᵥ) p := rfl
+
+@[simp] lemma coe_const_vsub_symm (p : P) : ⇑(const_vsub p).symm = λ v, -v +ᵥ p := rfl
+
 variables (P)
 
 /-- The map `p ↦ v +ᵥ p` as an isometric automorphism of `P`. -/
@@ -135,6 +144,57 @@ variable (V)
 @[simp] lemma const_vadd_zero : const_vadd P (0:V) = isometric.refl P :=
 isometric.to_equiv_inj $ equiv.const_vadd_zero V P
 
+variables {P V}
+
+/-- Point reflection in `x` as an `isometric` homeomorphism. -/
+def point_reflection (x : P) : P ≃ᵢ P :=
+(const_vsub x).trans (vadd_const x)
+
+lemma point_reflection_apply (x y : P) : point_reflection x y = x -ᵥ y +ᵥ x := rfl
+
+@[simp] lemma point_reflection_to_equiv (x : P) :
+  (point_reflection x).to_equiv = equiv.point_reflection x := rfl
+
+@[simp] lemma point_reflection_self (x : P) : point_reflection x x = x :=
+equiv.point_reflection_self x
+
+lemma point_reflection_involutive (x : P) : function.involutive (point_reflection x : P → P) :=
+equiv.point_reflection_involutive x
+
+@[simp] lemma point_reflection_symm (x : P) : (point_reflection x).symm = point_reflection x :=
+to_equiv_inj $ equiv.point_reflection_symm x
+
+@[simp] lemma dist_point_reflection_fixed (x y : P) :
+  dist (point_reflection x y) x = dist y x :=
+by rw [← (point_reflection x).dist_eq y x, point_reflection_self]
+
+lemma dist_point_reflection_self' (x y : P) :
+  dist (point_reflection x y) y = ∥bit0 (x -ᵥ y)∥ :=
+by rw [point_reflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, bit0]
+
+lemma dist_point_reflection_self (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 V] (x y : P) :
+  dist (point_reflection x y) y = ∥(2:𝕜)∥ * dist x y :=
+by rw [dist_point_reflection_self', ← two_smul' 𝕜 (x -ᵥ y), norm_smul, ← dist_eq_norm_vsub V]
+
+lemma point_reflection_fixed_iff (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 V] [invertible (2:𝕜)]
+  {x y : P} :
+  point_reflection x y = y ↔ y = x :=
+affine_equiv.point_reflection_fixed_iff_of_module 𝕜
+
+variables [normed_space ℝ V]
+
+lemma dist_point_reflection_self_real (x y : P) :
+  dist (point_reflection x y) y = 2 * dist x y :=
+by { rw [dist_point_reflection_self ℝ, real.norm_two], apply_instance }
+
+@[simp] lemma point_reflection_midpoint_left (x y : P) :
+  point_reflection (midpoint ℝ x y) x = y :=
+affine_equiv.point_reflection_midpoint_left x y
+
+@[simp] lemma point_reflection_midpoint_right (x y : P) :
+  point_reflection (midpoint ℝ x y) y = x :=
+affine_equiv.point_reflection_midpoint_right x y
+
 end isometric
 
 lemma lipschitz_with.vadd [emetric_space α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0}
@@ -225,3 +285,21 @@ begin
     (hf.comp (isometric.vadd_const p).isometry),
   exact funext hg
 end
+
+variables [normed_space ℝ V] [normed_space ℝ V']
+include V'
+
+/-- A continuous map between two normed affine spaces is an affine map provided that
+it sends midpoints to midpoints. -/
+def affine_map.of_map_midpoint (f : P → P')
+  (h : ∀ x y, f (midpoint ℝ x y) = midpoint ℝ (f x) (f y))
+  (hfc : continuous f) :
+  P →ᵃ[ℝ] P' :=
+affine_map.mk' f
+  ↑((add_monoid_hom.of_map_midpoint ℝ ℝ
+    ((affine_equiv.vadd_const ℝ (f $ classical.arbitrary P)).symm ∘ f ∘
+      (affine_equiv.vadd_const ℝ (classical.arbitrary P))) (by simp)
+      (λ x y, by simp [h])).to_real_linear_map $ by apply_rules [continuous.vadd, continuous.vsub,
+        continuous_const, hfc.comp, continuous_id])
+  (classical.arbitrary P)
+  (λ p, by simp)