feat(analysis/normed_space/add_torsor): normed_add_torsor (#2814)

Define the metric space structure on torsors of additive normed group
actions.  The motivating case is Euclidean affine spaces.

See
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations
for the discussion leading to this particular handling of the
distance.

Note: I'm not sure what the right way is to address the
dangerous_instance linter error "The following arguments become
metavariables. argument 1: (V : Type u_1)".

Author: jsm28

src/algebra/add_torsor.lean

@@ -74,6 +74,16 @@ instance add_group_is_add_torsor (G : Type*) [add_group G] :
   vsub_vadd' := sub_add_cancel,
   vadd_vsub' := add_sub_cancel }
 
+/-- Simplify addition for a torsor for an `add_group G` over
+itself. -/
+@[simp] lemma vadd_eq_add (G : Type*) [add_group G] (g1 g2 : G) : g1 +ᵥ g2 = g1 + g2 :=
+rfl
+
+/-- Simplify subtraction for a torsor for an `add_group G` over
+itself. -/
+@[simp] lemma vsub_eq_sub (G : Type*) [add_group G] (g1 g2 : G) : g1 -ᵥ g2 = g1 - g2 :=
+rfl
+
 namespace add_action
 
 section general

src/analysis/normed_space/add_torsor.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2020 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joseph Myers.
+-/
+import algebra.add_torsor
+import analysis.normed_space.basic
+
+noncomputable theory
+
+/-!
+# Torsors of additive normed group actions.
+
+This file defines torsors of additive normed group actions, with a
+metric space structure.  The motivating case is Euclidean affine
+spaces.
+
+-/
+
+universes u v
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
+/-- A `normed_add_torsor V P` is a torsor of an additive normed group
+action by a `normed_group V` on points `P`. We bundle the metric space
+structure and require the distance to be the same as results from the
+norm (which in fact implies the distance yields a metric space, but
+bundling just the distance and using an instance for the metric space
+results in type class problems). -/
+class normed_add_torsor (V : Type u) (P : Type v) [normed_group V] [metric_space P]
+  extends add_torsor V P :=
+(dist_eq_norm' : ∀ (x y : P), dist x y = ∥(x -ᵥ y : V)∥)
+end prio
+
+/-- The distance equals the norm of subtracting two points. This lemma
+is needed to make V an explicit rather than implicit argument. -/
+lemma add_torsor.dist_eq_norm (V : Type u) {P : Type v} [normed_group V] [metric_space P]
+    [normed_add_torsor V P] (x y : P) :
+  dist x y = ∥(x -ᵥ y : V)∥ :=
+normed_add_torsor.dist_eq_norm' x y
+
+/-- A `normed_group` is a `normed_add_torsor` over itself. -/
+instance normed_group.normed_add_torsor (V : Type u) [normed_group V] :
+  normed_add_torsor V V :=
+{ dist_eq_norm' := dist_eq_norm }
+
+open add_torsor
+
+/-- The distance defines a metric space structure on the torsor. This
+is not an instance because it depends on `V` to define a `metric_space
+P`. -/
+def metric_space_of_normed_group_of_add_torsor (V : Type u) (P : Type v) [normed_group V]
+    [add_torsor V P] : metric_space P :=
+{ dist := λ x y, ∥(x -ᵥ y : V)∥,
+  dist_self := λ x, by simp,
+  eq_of_dist_eq_zero := λ x y h, by simpa using h,
+  dist_comm := λ x y, by simp only [←neg_vsub_eq_vsub_rev V y x, norm_neg],
+  dist_triangle := begin
+    intros x y z,
+    change ∥x -ᵥ z∥ ≤ ∥x -ᵥ y∥ + ∥y -ᵥ z∥,
+    rw ←vsub_add_vsub_cancel,
+    apply norm_add_le
+  end }

src/analysis/normed_space/basic.lean

@@ -141,7 +141,7 @@ by simpa only [dist_add_left, dist_add_right, dist_comm h₂]
 @[simp] lemma norm_nonneg (g : α) : 0 ≤ ∥g∥ :=
 by { rw[←dist_zero_right], exact dist_nonneg }
 
-lemma norm_eq_zero {g : α} : ∥g∥ = 0 ↔ g = 0 :=
+@[simp] lemma norm_eq_zero {g : α} : ∥g∥ = 0 ↔ g = 0 :=
 dist_zero_right g ▸ dist_eq_zero
 
 @[simp] lemma norm_zero : ∥(0:α)∥ = 0 := norm_eq_zero.2 rfl