feat(geometry/euclidean): Euclidean space (#2852)

Define Euclidean affine spaces (not necessarily finite-dimensional),
and a corresponding instance for the standard Euclidean space `fin n → ℝ`.

This just defines the type class and the instance, with some other
basic geometric definitions and results to be added separately once
this is in.

I haven't attempted to do anything about the `euclidean_space`
definition in geometry/manifold/real_instances.lean that comes with a
comment that it uses the wrong norm.  That might better be refactored
by someone familiar with the manifold code.

By defining Euclidean spaces such that they are defined to be metric
spaces, and providing an instance, this probably implicitly gives item
91 "The Triangle Inequality" from the 100-theorems list, if that's
taken to have a geometric interpretation as in the Coq version, but
it's not very clear how something implicit like that from various
different pieces of the library, and where the item on the list could
be interpreted in several different ways anyway, should be entered in
100.yaml.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/normed_space/real_inner_product.lean

@@ -43,6 +43,7 @@ The Coq code is available at the following address: <http://www.lri.fr/~sboldo/e
 noncomputable theory
 
 open real set
+open_locale big_operators
 open_locale topological_space
 
 universes u v w
@@ -96,9 +97,13 @@ by { rw [← zero_smul ℝ (0:α), inner_smul_left, zero_mul] }
 @[simp] lemma inner_zero_right {x : α} : inner x 0 = 0 :=
 by { rw [inner_comm, inner_zero_left] }
 
-lemma inner_self_eq_zero (x : α) : inner x x = 0 ↔ x = 0 :=
+@[simp] lemma inner_self_eq_zero {x : α} : inner x x = 0 ↔ x = 0 :=
 iff.intro (inner_product_space.definite _) (by { rintro rfl, exact inner_zero_left })
 
+@[simp] lemma inner_self_nonpos {x : α} : inner x x ≤ 0 ↔ x = 0 :=
+⟨λ h, inner_self_eq_zero.1 (le_antisymm h inner_self_nonneg),
+  λ h, h.symm ▸ le_of_eq inner_zero_left⟩
+
 @[simp] lemma inner_neg_left {x y : α} : inner (-x) y = -inner x y :=
 by { rw [← neg_one_smul ℝ x, inner_smul_left], simp }
 
@@ -154,7 +159,8 @@ instance inner_product_space_has_norm : has_norm α := ⟨λx, sqrt (inner x x)
 
 lemma norm_eq_sqrt_inner {x : α} : ∥x∥ = sqrt (inner x x) := rfl
 
-lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ := (mul_self_sqrt inner_self_nonneg).symm
+lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ :=
+(mul_self_sqrt inner_self_nonneg).symm
 
 /-- Expand the square -/
 lemma norm_add_pow_two {x y : α} : ∥x + y∥^2 = ∥x∥^2 + 2 * inner x y + ∥y∥^2 :=
@@ -192,7 +198,7 @@ by { simp only [(inner_self_eq_norm_square _).symm], exact parallelogram_law }
 instance inner_product_space_is_normed_group : normed_group α :=
 normed_group.of_core α
 { norm_eq_zero_iff := assume x, iff.intro
-    (λ h : sqrt (inner x x) = 0, (inner_self_eq_zero x).1 $ (sqrt_eq_zero inner_self_nonneg).1 h )
+    (λ h : sqrt (inner x x) = 0, inner_self_eq_zero.1 $ (sqrt_eq_zero inner_self_nonneg).1 h )
     (by {rintro rfl, show sqrt (inner (0:α) 0) = 0, simp }),
   triangle := assume x y,
   begin
@@ -221,6 +227,58 @@ instance inner_product_space_is_normed_space : normed_space ℝ α :=
 
 end norm
 
+-- TODO [Lean 3.15]: drop some of these `show`s
+/-- If `ι` is a finite type and each space `f i`, `i : ι`, is an inner product space,
+then `Π i, f i` is an inner product space as well. This is not an instance to avoid conflict
+with the default instance for the norm on `Π i, f i`. -/
+def pi.inner_product_space (ι : Type*) [fintype ι] (f : ι → Type*) [Π i, inner_product_space (f i)] :
+  inner_product_space (Π i, f i) :=
+{ inner := λ x y, ∑ i, inner (x i) (y i),
+  comm := λ x y, finset.sum_congr rfl $ λ i hi, inner_comm (x i) (y i),
+  nonneg := λ x, show (0:ℝ) ≤ ∑ i, inner (x i) (x i),
+    from finset.sum_nonneg (λ i hi, inner_self_nonneg),
+  definite := λ x h, begin
+    have : ∀ i ∈ (finset.univ : finset ι), 0 ≤ inner (x i) (x i) := λ i hi, inner_self_nonneg,
+    simpa [inner, finset.sum_eq_zero_iff_of_nonneg this, function.funext_iff] using h,
+  end,
+  add_left := λ x y z,
+    show ∑ i, inner (x i + y i) (z i) = ∑ i, inner (x i) (z i) + ∑ i, inner (y i) (z i),
+    by simp only [inner_add_left, finset.sum_add_distrib],
+  smul_left := λ x y r,
+    show ∑ (i : ι), inner (r • x i) (y i) = r * ∑ i, inner (x i) (y i),
+    by simp only [finset.mul_sum, inner_smul_left] }
+
+/-- The set of real numbers is an inner product space. While the norm given by this definition
+is equal to the default norm `∥x∥ = abs x`, it is not definitionally equal, so we don't turn this
+definition into an instance.
+
+TODO: do the same trick as with `metric_space` and `emetric_space`? -/
+def real.inner_product_space : inner_product_space ℝ :=
+{ inner := (*),
+  comm := mul_comm,
+  nonneg := mul_self_nonneg,
+  definite := λ x, mul_self_eq_zero.1,
+  add_left := add_mul,
+  smul_left := λ _ _ _, mul_assoc _ _ _ }
+
+section instances
+/-- The standard Euclidean space, functions on a finite type. For an `n`-dimensional space
+use `euclidean_space (fin n)`.  -/
+@[derive add_comm_group, nolint unused_arguments]
+def euclidean_space (n : Type*) [fintype n] : Type* := n → ℝ
+
+variables {n : Type*} [fintype n]
+
+instance : inhabited (euclidean_space n) := ⟨0⟩
+
+local attribute [instance] real.inner_product_space
+
+instance : inner_product_space (euclidean_space n) := pi.inner_product_space n (λ _, ℝ)
+
+lemma euclidean_space.inner_def (x y : euclidean_space n) : inner x y = ∑ i, x i * y i := rfl
+
+end instances
+
 section orthogonal
 
 open filter

src/geometry/euclidean.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2020 Joseph Myers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joseph Myers.
+-/
+import analysis.normed_space.real_inner_product
+import analysis.normed_space.add_torsor
+
+noncomputable theory
+
+/-!
+# Euclidean spaces
+
+This file defines Euclidean affine spaces.
+
+## Implementation notes
+
+Rather than requiring Euclidean affine spaces to be finite-dimensional
+(as in the definition on Wikipedia), this is specified only for those
+theorems that need it.
+
+## References
+
+* https://en.wikipedia.org/wiki/Euclidean_space
+
+-/
+
+/-- A `euclidean_affine_space V P` is an affine space with points `P`
+over an `inner_product_space V`. -/
+abbreviation euclidean_affine_space (V : Type*) (P : Type*) [inner_product_space V]
+    [metric_space P] :=
+normed_add_torsor V P
+
+example (n : Type*) [fintype n] : euclidean_affine_space (euclidean_space n) (euclidean_space n) :=
+by apply_instance

src/geometry/manifold/real_instances.lean

@@ -14,10 +14,10 @@ or with boundary or with corners. As a concrete example, we construct explicitly
 boundary structure on the real interval `[x, y]`.
 
 More specifically, we introduce
-* `euclidean_space n` for a model vector space of dimension `n`.
-* `model_with_corners ℝ (euclidean_space n) (euclidean_half_space n)` for the model space used
+* `euclidean_space2 n` for a model vector space of dimension `n`.
+* `model_with_corners ℝ (euclidean_space2 n) (euclidean_half_space n)` for the model space used
 to define `n`-dimensional real manifolds with boundary
-* `model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n)` for the model space used
+* `model_with_corners ℝ (euclidean_space2 n) (euclidean_quadrant n)` for the model space used
 to define `n`-dimensional real manifolds with corners
 
 ## Implementation notes
@@ -34,38 +34,38 @@ The space `ℝ^n`. Note that the name is slightly misleading, as we only need a
 structure on `ℝ^n`, but the one we use here is the sup norm and not the euclidean one -- this is not
 a problem for the manifold applications, but should probably be refactored at some point.
 -/
-def euclidean_space (n : ℕ) : Type := (fin n → ℝ)
+def euclidean_space2 (n : ℕ) : Type := (fin n → ℝ)
 
 /--
 The half-space in `ℝ^n`, used to model manifolds with boundary. We only define it when
 `1 ≤ n`, as the definition only makes sense in this case.
 -/
 def euclidean_half_space (n : ℕ) [has_zero (fin n)] : Type :=
-{x : euclidean_space n // 0 ≤ x 0}
+{x : euclidean_space2 n // 0 ≤ x 0}
 
 /--
 The quadrant in `ℝ^n`, used to model manifolds with corners, made of all vectors with nonnegative
 coordinates.
 -/
-def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space n // ∀i:fin n, 0 ≤ x i}
+def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space2 n // ∀i:fin n, 0 ≤ x i}
 
 section
 /- Register class instances for euclidean space and half-space and quadrant -/
-local attribute [reducible] euclidean_space euclidean_half_space euclidean_quadrant
+local attribute [reducible] euclidean_space2 euclidean_half_space euclidean_quadrant
 variable {n : ℕ}
 
  -- short-circuit type class inference
-instance : vector_space ℝ (euclidean_space n) := by apply_instance
-instance : normed_group (euclidean_space n) := by apply_instance
-instance : normed_space ℝ (euclidean_space n) := by apply_instance
+instance : vector_space ℝ (euclidean_space2 n) := by apply_instance
+instance : normed_group (euclidean_space2 n) := by apply_instance
+instance : normed_space ℝ (euclidean_space2 n) := by apply_instance
 instance [has_zero (fin n)] : topological_space (euclidean_half_space n) := by apply_instance
 instance : topological_space (euclidean_quadrant n) := by apply_instance
-instance : finite_dimensional ℝ (euclidean_space n) := by apply_instance
-instance : inhabited (euclidean_space n) := ⟨0⟩
+instance : finite_dimensional ℝ (euclidean_space2 n) := by apply_instance
+instance : inhabited (euclidean_space2 n) := ⟨0⟩
 instance [has_zero (fin n)] : inhabited (euclidean_half_space n) := ⟨⟨0, by simp⟩⟩
 instance : inhabited (euclidean_quadrant n) := ⟨⟨0, λ i, by simp⟩⟩
 
-@[simp] lemma findim_euclidean_space : finite_dimensional.findim ℝ (euclidean_space n) = n :=
+@[simp] lemma findim_euclidean_space : finite_dimensional.findim ℝ (euclidean_space2 n) = n :=
 by simp
 
 lemma range_half_space (n : ℕ) [has_zero (fin n)] :
@@ -79,11 +79,11 @@ by simp
 end
 
 /--
-Definition of the model with corners `(euclidean_space n, euclidean_half_space n)`, used as a
+Definition of the model with corners `(euclidean_space2 n, euclidean_half_space n)`, used as a
 model for manifolds with boundary.
 -/
 def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
-  model_with_corners ℝ (euclidean_space n) (euclidean_half_space n) :=
+  model_with_corners ℝ (euclidean_space2 n) (euclidean_half_space n) :=
 { to_fun      := λx, x.val,
   inv_fun     := λx, ⟨λi, if h : i = 0 then max (x i) 0 else x i, by simp [le_refl]⟩,
   source      := univ,
@@ -108,10 +108,10 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
     `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
     rw range_half_space,
     apply unique_diff_on_convex,
-    show convex {y : euclidean_space n | 0 ≤ y 0},
+    show convex {y : euclidean_space2 n | 0 ≤ y 0},
     { assume x y hx hy a b ha hb hab,
       simpa using add_le_add (mul_nonneg ha hx) (mul_nonneg hb hy) },
-    show (interior {y : euclidean_space n | 0 ≤ y 0}).nonempty,
+    show (interior {y : euclidean_space2 n | 0 ≤ y 0}).nonempty,
     { use (λi, 1),
       rw mem_interior,
       refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,
@@ -137,10 +137,10 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
   end }
 
 /--
-Definition of the model with corners `(euclidean_space n, euclidean_quadrant n)`, used as a
+Definition of the model with corners `(euclidean_space2 n, euclidean_quadrant n)`, used as a
 model for manifolds with corners -/
 def model_with_corners_euclidean_quadrant (n : ℕ) :
-  model_with_corners ℝ (euclidean_space n) (euclidean_quadrant n) :=
+  model_with_corners ℝ (euclidean_space2 n) (euclidean_quadrant n) :=
 { to_fun      := λx, x.val,
   inv_fun     := λx, ⟨λi, max (x i) 0, λi, by simp [le_refl]⟩,
   source      := univ,
@@ -163,10 +163,10 @@ def model_with_corners_euclidean_quadrant (n : ℕ) :
     `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/
     rw range_quadrant,
     apply unique_diff_on_convex,
-    show convex {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i},
+    show convex {y : euclidean_space2 n | ∀ (i : fin n), 0 ≤ y i},
     { assume x y hx hy a b ha hb hab i,
       simpa using add_le_add (mul_nonneg ha (hx i)) (mul_nonneg hb (hy i)) },
-    show (interior {y : euclidean_space n | ∀ (i : fin n), 0 ≤ y i}).nonempty,
+    show (interior {y : euclidean_space2 n | ∀ (i : fin n), 0 ≤ y i}).nonempty,
     { use (λi, 1),
       rw mem_interior,
       refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _,