style(geometry/euclidean): consistently use inner product notation (#…

…16961)

Make `geometry.euclidean` files consistently use notation for the inner product, rather than mixing notation with non-notation calls to `inner`.  Also always get that notation from `open_locale real_inner_product_space` instead of a local `notation` declaration.

src/geometry/euclidean/angle/unoriented/basic.lean

@@ -30,7 +30,7 @@ variables {V : Type*} [inner_product_space ℝ V]
 /-- The undirected angle between two vectors. If either vector is 0,
 this is π/2. See `orientation.oangle` for the corresponding oriented angle
 definition. -/
-def angle (x y : V) : ℝ := real.arccos (inner x y / (∥x∥ * ∥y∥))
+def angle (x y : V) : ℝ := real.arccos (⟪x, y⟫ / (∥x∥ * ∥y∥))
 
 lemma continuous_at_angle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
   continuous_at (λ y : V × V, angle y.1 y.2) x :=
@@ -72,7 +72,7 @@ lemma conformal_at.preserves_angle {E F : Type*}
 let ⟨f₁, h₁, c⟩ := H in h₁.unique h ▸ is_conformal_map.preserves_angle c u v
 
 /-- The cosine of the angle between two vectors. -/
-lemma cos_angle (x y : V) : real.cos (angle x y) = inner x y / (∥x∥ * ∥y∥) :=
+lemma cos_angle (x y : V) : real.cos (angle x y) = ⟪x, y⟫ / (∥x∥ * ∥y∥) :=
 real.cos_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
                 (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2
 
@@ -167,7 +167,7 @@ by rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]
 
 /-- The cosine of the angle between two vectors, multiplied by the
 product of their norms. -/
-lemma cos_angle_mul_norm_mul_norm (x y : V) : real.cos (angle x y) * (∥x∥ * ∥y∥) = inner x y :=
+lemma cos_angle_mul_norm_mul_norm (x y : V) : real.cos (angle x y) * (∥x∥ * ∥y∥) = ⟪x, y⟫ :=
 begin
   rw [cos_angle, div_mul_cancel_of_imp],
   simp [or_imp_distrib] { contextual := tt },
@@ -176,7 +176,7 @@ end
 /-- The sine of the angle between two vectors, multiplied by the
 product of their norms. -/
 lemma sin_angle_mul_norm_mul_norm (x y : V) : real.sin (angle x y) * (∥x∥ * ∥y∥) =
-    real.sqrt (inner x x * inner y y - inner x y * inner x y) :=
+    real.sqrt (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) :=
 begin
   unfold angle,
   rw [real.sin_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
@@ -294,8 +294,8 @@ begin
   rw ← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy,
   obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
   rw [← sq_eq_sq hxy₁ hxy₂, norm_sub_pow_two_real] at h,
-  calc inner x y = (∥x∥ ^ 2 + ∥y∥ ^ 2 - (∥x∥ + ∥y∥) ^ 2) / 2 : by linarith
-  ...            = -(∥x∥ * ∥y∥) : by ring,
+  calc ⟪x, y⟫ = (∥x∥ ^ 2 + ∥y∥ ^ 2 - (∥x∥ + ∥y∥) ^ 2) / 2 : by linarith
+  ...         = -(∥x∥ * ∥y∥) : by ring,
 end
 
 /-- The norm of the sum of two non-zero vectors equals the sum of their norms
@@ -307,8 +307,8 @@ begin
   rw ← inner_eq_mul_norm_iff_angle_eq_zero hx hy,
   obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
   rw [← sq_eq_sq hxy₁ hxy₂, norm_add_pow_two_real] at h,
-  calc inner x y = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
-  ...            = ∥x∥ * ∥y∥ : by ring,
+  calc ⟪x, y⟫ = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
+  ...         = ∥x∥ * ∥y∥ : by ring,
 end
 
 /-- The norm of the difference of two non-zero vectors equals the absolute value
@@ -320,8 +320,8 @@ begin
   rw ← inner_eq_mul_norm_iff_angle_eq_zero hx hy,
   have h1 : ∥x - y∥ ^ 2 = (∥x∥ - ∥y∥) ^ 2, { rw h, exact sq_abs (∥x∥ - ∥y∥) },
   rw norm_sub_pow_two_real at h1,
-  calc inner x y = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
-  ...            = ∥x∥ * ∥y∥ : by ring,
+  calc ⟪x, y⟫ = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
+  ...         = ∥x∥ * ∥y∥ : by ring,
 end
 
 /-- The norm of the sum of two vectors equals the norm of their difference if and only if

src/geometry/euclidean/basic.lean

@@ -57,7 +57,6 @@ Euclidean affine spaces.
 
 variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
     [normed_add_torsor V P]
-local notation `⟪`x`, `y`⟫` := @inner ℝ V _ x y
 include V
 
 /-- The midpoint of the segment AB is the same distance from A as it is from B. -/
@@ -70,7 +69,7 @@ terms of the pairwise distances. -/
 lemma inner_weighted_vsub {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P)
     (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P)
     (h₂ : ∑ i in s₂, w₂ i = 0) :
-  inner (s₁.weighted_vsub p₁ w₁) (s₂.weighted_vsub p₂ w₂) =
+  ⟪s₁.weighted_vsub p₁ w₁, s₂.weighted_vsub p₂ w₂⟫ =
     (-∑ i₁ in s₁, ∑ i₂ in s₂,
       w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2 :=
 begin
@@ -138,7 +137,7 @@ begin
                  ←real_inner_self_eq_norm_mul_norm, sub_self] },
   have hvi : ⟪v, v⟫ ≠ 0, by simpa using hv,
   have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 =
-    (2 * inner v (p₁ -ᵥ p₂)) * (2 * inner v (p₁ -ᵥ p₂)),
+    (2 * ⟪v, p₁ -ᵥ p₂⟫) * (2 * ⟪v, p₁ -ᵥ p₂⟫),
   { rw discrim, ring },
   rw [quadratic_eq_zero_iff hvi hd, add_left_neg, zero_div, neg_mul_eq_neg_mul,
       ←mul_sub_right_distrib, sub_eq_add_neg, ←mul_two, mul_assoc, mul_div_assoc,

src/geometry/euclidean/triangle.lean

@@ -123,12 +123,12 @@ begin
                 ∥x∥ * ∥y∥ * ∥x - y∥ * ∥x - y∥ =
               (real.sin (angle x (x - y)) * (∥x∥ * ∥x - y∥)) *
                 (real.sin (angle y (y - x)) * (∥y∥ * ∥x - y∥)), { ring },
-    have H2 : ⟪x, x⟫ * (inner x x - inner x y - (inner x y - inner y y)) -
-                (inner x x - inner x y) * (inner x x - inner x y) =
-              inner x x * inner y y - inner x y * inner x y, { ring },
-    have H3 : ⟪y, y⟫ * (inner y y - inner x y - (inner x y - inner x x)) -
-                (inner y y - inner x y) * (inner y y - inner x y) =
-              inner x x * inner y y - inner x y * inner x y, { ring },
+    have H2 : ⟪x, x⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) -
+                (⟪x, x⟫ - ⟪x, y⟫) * (⟪x, x⟫ - ⟪x, y⟫) =
+              ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫, { ring },
+    have H3 : ⟪y, y⟫ * (⟪y, y⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪x, x⟫)) -
+                (⟪y, y⟫ - ⟪x, y⟫) * (⟪y, y⟫ - ⟪x, y⟫) =
+              ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫, { ring },
     rw [mul_sub_right_distrib, mul_sub_right_distrib, mul_sub_right_distrib,
         mul_sub_right_distrib, H1, sin_angle_mul_norm_mul_norm, norm_sub_rev x y,
         sin_angle_mul_norm_mul_norm, norm_sub_rev y x, inner_sub_left, inner_sub_left,