chore(analysis/normed_space/mazur_ulam): add to_affine_map (#2963)

src/analysis/normed_space/mazur_ulam.lean

@@ -5,20 +5,28 @@ Author: Yury Kudryashov
 -/
 import analysis.normed_space.point_reflection
 import topology.instances.real_vector_space
+import analysis.normed_space.add_torsor
+import linear_algebra.affine_space
 
 /-!
 # Mazur-Ulam Theorem
 
 Mazur-Ulam theorem states that an isometric bijection between two normed spaces over `ℝ` is affine.
-Since `mathlib` has no notion of an affine map (yet?), we formalize it in two definitions:
+We formalize it in two definitions:
 
 * `isometric.to_real_linear_equiv_of_map_zero` : given `E ≃ᵢ F` sending `0` to `0`,
   returns `E ≃L[ℝ] F` with the same `to_fun` and `inv_fun`;
 * `isometric.to_real_linear_equiv` : given `f : E ≃ᵢ F`,
   returns `g : E ≃L[ℝ] F` with `g x = f x - f 0`.
+* `isometric.to_affine_map` : given `PE ≃ᵢ PF`, returns `g : affine_map ℝ E PE F PF` with the same
+  `to_fun`.
 
 The formalization is based on [Jussi Väisälä, *A Proof of the Mazur-Ulam Theorem*][Vaisala_2003].
 
+## TODO
+
+Once we have affine equivalences, upgrade `isometric.to_affine_map` to `isometric.to_affine_equiv`.
+
 ## Tags
 
 isometry, affine map, linear map
@@ -121,4 +129,17 @@ def to_real_linear_equiv (f : E ≃ᵢ F) : E ≃L[ℝ] F :=
 @[simp] lemma to_real_linear_equiv_symm_apply (f : E ≃ᵢ F) (y : F) :
   (f.to_real_linear_equiv.symm : F → E) y = f.symm (y + f 0) := rfl
 
+variables (E F) {PE : Type*} {PF : Type*} [metric_space PE] [normed_add_torsor E PE]
+  [metric_space PF] [normed_add_torsor F PF]
+
+/-- Convert an isometric equivalence between two affine spaces to an `affine_map`. -/
+def to_affine_map (f : PE ≃ᵢ PF) : affine_map ℝ E PE F PF :=
+affine_map.mk' f
+ (((vadd_const E (classical.choice $ add_torsor.nonempty E : PE)).trans $ f.trans
+    (vadd_const F (f $ classical.choice $ add_torsor.nonempty E : PF)).symm).to_real_linear_equiv)
+ (classical.choice $ add_torsor.nonempty E) $ λ p',
+ by simp
+
+@[simp] lemma coe_to_affine_map (f : PE ≃ᵢ PF) : ⇑(f.to_affine_map E F) = f := rfl
+
 end isometric

src/linear_algebra/affine_space.lean

@@ -190,7 +190,7 @@ structure affine_map (k : Type*) (V1 : Type*) (P1 : Type*) (V2 : Type*) (P2 : Ty
     [add_comm_group V2] [module k V2] [affine_space k V2 P2] :=
 (to_fun : P1 → P2)
 (linear : linear_map k V1 V2)
-(map_vadd' : ∀ (p : P1) (v : V1), to_fun (v +ᵥ p) =  linear.to_fun v +ᵥ to_fun p)
+(map_vadd' : ∀ (p : P1) (v : V1), to_fun (v +ᵥ p) =  linear v +ᵥ to_fun p)
 
 namespace affine_map
 
@@ -237,6 +237,19 @@ begin
   erw [← f_add, ← g_add]
 end
 
+/-- Construct an affine map by verifying the relation between the map and its linear part at one
+base point. Namely, this function takes a map `f : P₁ → P₂`, a linear map `f' : V₁ →ₗ[k] V₂`, and
+a point `p` such that for any other point `p'` we have `f p' = f' (p' -ᵥ p) +ᵥ f p`. -/
+def mk' (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ p' : P1, f p' = f' (p' -ᵥ p) +ᵥ f p) :
+  affine_map k V1 P1 V2 P2 :=
+{ to_fun := f,
+  linear := f',
+  map_vadd' := λ p' v, by rw [h, h p', vadd_vsub_assoc, f'.map_add, add_action.vadd_assoc] }
+
+@[simp] lemma coe_mk' (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : ⇑(mk' f f' p h) = f := rfl
+
+@[simp] lemma mk'_linear (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : (mk' f f' p h).linear = f' := rfl
+
 variables (k V1 P1)
 
 /-- Identity map as an affine map. -/