feat(Geometry/Euclidean/SignedDist): signedDist between two points (leanprover-community#27260)

original PR: leanprover-community#24245

This PR defines `signedDist`, the signed distance between two points.

It also redefines `signedInfDist` so that it uses `signedDist`.

The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point

[#mathlib4 > Signed distance between points](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Signed.20distance.20between.20points)

some comments:

* should `signedDistLinear` be `private`?
* I'm not too happy about the hypothesis in `signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w)`. This relationship between `v` and `w` is a symmetric one that should have some API around it, similar to `SameRay`. It could also be spelled as `(ℝ≥0 ∙ v) = ℝ≥0 ∙ w`

Author: JovanGerb

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -670,6 +670,7 @@ theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {x : F} {r
     mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]
   exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))
 
+variable (𝕜) in
 theorem norm_inner_eq_norm_tfae (x y : E) :
     List.TFAE [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖,
       x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x,
@@ -701,7 +702,7 @@ theorem norm_inner_eq_norm_iff {x y : E} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
     ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
   calc
     ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ x = 0 ∨ ∃ r : 𝕜, y = r • x :=
-      (@norm_inner_eq_norm_tfae 𝕜 _ _ _ _ x y).out 0 2
+      (norm_inner_eq_norm_tfae 𝕜 x y).out 0 2
     _ ↔ ∃ r : 𝕜, y = r • x := or_iff_right hx₀
     _ ↔ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
       ⟨fun ⟨r, h⟩ => ⟨r, fun hr₀ => hy₀ <| h.symm ▸ smul_eq_zero.2 <| Or.inl hr₀, h⟩,
@@ -735,7 +736,7 @@ theorem inner_eq_norm_mul_iff_div {x y : E} (h₀ : x ≠ 0) :
   rw [← norm_ne_zero_iff, Ne, ← @ofReal_eq_zero 𝕜] at h₀'
   constructor <;> intro h
   · have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
-      ((@norm_inner_eq_norm_tfae 𝕜 _ _ _ _ x y).out 0 1).1 (by simp [h])
+      ((norm_inner_eq_norm_tfae 𝕜 x y).out 0 1).1 (by simp [h])
     rw [this.resolve_left h₀, h]
     simp [norm_smul, inner_self_ofReal_norm, mul_div_cancel_right₀ _ h₀']
   · conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]

Mathlib/Geometry/Euclidean/SignedDist.lean

@@ -4,18 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Geometry.Euclidean.Projection
-import Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv
-import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
-import Mathlib.Topology.Algebra.AffineSubspace
 
 /-!
 # Signed distance to an affine subspace in a Euclidean space.
 
-This file defines the signed distance between an affine subspace and a point, in the direction
-of a given reference point.
+This file defines the signed distance between two points, in the direction of a given a vector, and
+the signed distance between an affine subspace and a point, in the direction of a given
+reference point.
 
 ## Main definitions
 
+* `signedDist` is the signed distance between two points
 * `AffineSubspace.signedInfDist` is the signed distance between an affine subspace and a point.
 * `Affine.Simplex.signedInfDist` is the signed distance between a face of a simplex and a point.
   In the case of a triangle, these distances are trilinear coordinates.
@@ -33,48 +32,222 @@ open scoped RealInnerProductSpace
 variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
 variable [NormedAddTorsor V P]
 
+section signedDist
+
+/-- Auxiliary definition for `signedDist`. It is the underlying linear map of `signedDist`. -/
+private noncomputable def signedDistLinear (v : V) : V →ₗ[ℝ] P →ᴬ[ℝ] ℝ where
+  toFun w := .const ℝ P ⟪-(‖v‖⁻¹ • v), w⟫
+  map_add' x y := by ext; simp [inner_add_right]
+  map_smul' r x := by ext; simp [inner_smul_right]
+
+private lemma signedDistLinear_apply (v w : V) :
+    signedDistLinear v w = .const ℝ P ⟪-(‖v‖⁻¹ • v), w⟫ := rfl
+
+/--
+The signed distance between two points `p` and `q`, in the direction of a reference vector `v`.
+It is the size of `q - p` in the direction of `v`.
+In the degenerate case `v = 0`, it returns `0`.
+
+TODO: once we have a topology on `P →ᴬ[ℝ] ℝ`, the type should be `P →ᴬ[ℝ] P →ᴬ[ℝ] ℝ`.
+-/
+noncomputable def signedDist (v : V) : P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ where
+  toFun p := (innerSL ℝ (‖v‖⁻¹ • v)).toContinuousAffineMap.comp
+    (ContinuousAffineMap.id ℝ P -ᵥ .const ℝ P p)
+  linear := signedDistLinear v
+  map_vadd' p v' := by
+    ext q
+    rw [signedDistLinear_apply]
+    generalize ‖v‖⁻¹ • v = x
+    simp [vsub_vadd_eq_vsub_sub, inner_sub_right, ← sub_eq_neg_add]
+
+variable (v w : V) (p q r : P)
+
+-- Lemmas about the definition of `signedDist`
+
+lemma signedDist_apply : signedDist v p = (innerSL ℝ (‖v‖⁻¹ • v)).toContinuousAffineMap.comp
+    (ContinuousAffineMap.id ℝ P -ᵥ .const ℝ P p) :=
+  rfl
+
+lemma signedDist_apply_apply : signedDist v p q = ⟪‖v‖⁻¹ • v, q -ᵥ p⟫ :=
+  rfl
+
+lemma signedDist_apply_linear : (signedDist v p).linear = innerₗ V (‖v‖⁻¹ • v) := by
+  change (innerₗ V (‖v‖⁻¹ • v)).comp (LinearMap.id - 0) = _
+  simp
+
+lemma signedDist_apply_linear_apply : (signedDist v p).linear w = ⟪‖v‖⁻¹ • v, w⟫ := by
+  simp [signedDist_apply_linear, real_inner_smul_left]
+
+lemma signedDist_linear_apply : (signedDist v).linear w = .const ℝ P ⟪-(‖v‖⁻¹ • v), w⟫ :=
+  rfl
+
+lemma signedDist_linear_apply_apply : (signedDist v).linear w p = ⟪-(‖v‖⁻¹ • v), w⟫ :=
+  rfl
+
+-- Lemmas about the vector argument of `signedDist`
+
+lemma signedDist_smul (r : ℝ) : signedDist (r • v) p q = SignType.sign r * signedDist v p q := by
+  simp only [signedDist_apply_apply]
+  rw [norm_smul, mul_inv_rev, smul_smul, mul_rotate, ← smul_smul, real_inner_smul_left]
+  congr
+  by_cases h : r = 0
+  · simp [h]
+  · rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
+    simp only [Real.norm_eq_abs, abs_mul_sign]
+
+@[simp] lemma signedDist_zero : signedDist 0 p q = 0 := by
+  simpa using signedDist_smul 0 p q 0
+
+@[simp] lemma signedDist_neg : signedDist (-v) p q = -signedDist v p q := by
+  simpa using signedDist_smul v p q (-1)
+
+lemma signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w) : signedDist (P := P) v = signedDist w := by
+  obtain ⟨r, _, _⟩ := h
+  ext p q
+  simpa [*] using (signedDist_smul v p q r).symm
+
+-- Lemmas about permuting the point arguments of `signedDist`, analogous to lemmas about `dist`
+
+@[simp] lemma signedDist_self : signedDist v p p = 0 := by
+  simp [signedDist_apply_apply]
+
+@[simp] lemma signedDist_anticomm : -signedDist v p q = signedDist v q p := by
+  simp [signedDist_apply_apply, ← inner_neg_right]
+
+@[simp]
+lemma signedDist_triangle : signedDist v p q + signedDist v q r = signedDist v p r := by
+  simp only [signedDist_apply_apply]
+  rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]
+
+@[simp]
+lemma signedDist_triangle_left : signedDist v p q - signedDist v p r = signedDist v r q := by
+  rw [sub_eq_iff_eq_add', signedDist_triangle]
+
+@[simp]
+lemma signedDist_triangle_right : signedDist v p r - signedDist v q r = signedDist v p q := by
+  rw [sub_eq_iff_eq_add, signedDist_triangle]
+
+-- Lemmas about offsetting the point arguments of `signedDist` (with `+ᵥ` or `-ᵥ`)
+
+lemma signedDist_vadd_left : signedDist v (w +ᵥ p) q = -⟪‖v‖⁻¹ • v, w⟫ + signedDist v p q := by
+  simp [signedDist_linear_apply_apply]
+
+lemma signedDist_vadd_right : signedDist v p (w +ᵥ q) = ⟪‖v‖⁻¹ • v, w⟫ + signedDist v p q := by
+  simp [signedDist_apply_linear_apply]
+
+-- TODO: find a better name for these 2 lemmas
+lemma signedDist_vadd_left_swap : signedDist v (w +ᵥ p) q = signedDist v p (-w +ᵥ q) := by
+  rw [signedDist_vadd_left, signedDist_vadd_right, inner_neg_right]
+
+lemma signedDist_vadd_right_swap : signedDist v p (w +ᵥ q) = signedDist v (-w +ᵥ p) q := by
+  rw [signedDist_vadd_left_swap, neg_neg]
+
+lemma signedDist_vadd_vadd : signedDist v (w +ᵥ p) (w +ᵥ q) = signedDist v p q := by
+  rw [signedDist_vadd_left_swap, neg_vadd_vadd]
+
+variable {v p q} in
+lemma signedDist_left_congr (h : ⟪v, p -ᵥ q⟫ = 0) : signedDist v p = signedDist v q := by
+  ext r
+  simpa [real_inner_smul_left, h] using signedDist_vadd_left v (p -ᵥ q) q r
+
+variable {v q r} in
+lemma signedDist_right_congr (h : ⟪v, q -ᵥ r⟫ = 0) : signedDist v p q = signedDist v p r := by
+  simpa [real_inner_smul_left, h] using signedDist_vadd_right v (q -ᵥ r) p r
+
+variable {v p q} in
+lemma signedDist_eq_zero_of_orthogonal (h : ⟪v, q -ᵥ p⟫ = 0) : signedDist v p q = 0 := by
+  simpa using signedDist_right_congr p h
+
+-- Lemmas relating `signedDist` to `dist`
+
+lemma abs_signedDist_le_dist : |signedDist v p q| ≤ dist p q := by
+  rw [signedDist_apply_apply]
+  by_cases h : v = 0
+  · simp [h]
+  · convert abs_real_inner_le_norm (‖v‖⁻¹ • v) (q -ᵥ p)
+    simp [norm_smul, dist_eq_norm_vsub']
+    field_simp
+
+lemma signedDist_le_dist : signedDist v p q ≤ dist p q :=
+  le_trans (le_abs_self _) (abs_signedDist_le_dist _ _ _)
+
+lemma abs_signedDist_eq_dist_iff_vsub_mem_span :
+    |signedDist v p q| = dist p q ↔ q -ᵥ p ∈ ℝ ∙ v := by
+  rw [Submodule.mem_span_singleton]
+  rw [signedDist_apply_apply, dist_eq_norm_vsub', real_inner_smul_left, abs_mul, abs_inv, abs_norm]
+  by_cases h : v = 0
+  · simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
+  rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
+  rw [← Real.norm_eq_abs, ((norm_inner_eq_norm_tfae ℝ v (q -ᵥ p)).out 0 2:)]
+  simp [h, eq_comm]
+
+open NNReal in
+lemma signedDist_eq_dist_iff_vsub_mem_span : signedDist v p q = dist p q ↔ q -ᵥ p ∈ ℝ≥0 ∙ v := by
+  rw [Submodule.mem_span_singleton]
+  rw [signedDist_apply_apply, dist_eq_norm_vsub', real_inner_smul_left]
+  by_cases h : v = 0
+  · simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
+  rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
+  rw [inner_eq_norm_mul_iff_real]
+  simp only [smul_def]
+  refine ⟨fun h => ?_, fun ⟨c, h⟩ => ?_⟩
+  · simp only [NNReal.exists, coe_mk, exists_prop]
+    use ‖v‖⁻¹ * ‖q -ᵥ p‖
+    constructor
+    · positivity
+    · rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
+  · rw [← h, norm_smul, smul_smul, mul_comm]
+    simp
+
+@[simp] lemma signedDist_vsub_self : signedDist (q -ᵥ p) p q = dist p q := by
+  rw [signedDist_eq_dist_iff_vsub_mem_span]
+  apply Submodule.mem_span_singleton_self
+
+@[simp] lemma signedDist_vsub_self_rev : signedDist (p -ᵥ q) p q = -dist p q := by
+  rw [← neg_eq_iff_eq_neg, ← signedDist_neg, neg_vsub_eq_vsub_rev]
+  apply signedDist_vsub_self
+
+end signedDist
+
 namespace AffineSubspace
 
-variable (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P)
+variable (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] (p q : P)
 
 /-- The signed distance between `s` and a point, in the direction of the reference point `p`.
 This is expected to be used when `p` does not lie in `s` (in the degenerate case where `p` lies
 in `s`, this yields 0) and when the point at which the distance is evaluated lies in the affine
 span of `s` and `p` (any component of the distance orthogonal to that span is disregarded). -/
 noncomputable def signedInfDist : P →ᴬ[ℝ] ℝ :=
-  (innerSL ℝ (‖p -ᵥ orthogonalProjection s p‖⁻¹ •
-      (p -ᵥ orthogonalProjection s p))).toContinuousAffineMap.comp
-    ((ContinuousAffineEquiv.refl ℝ P).toContinuousAffineMap -ᵥ
-      s.subtypeA.comp (orthogonalProjection s))
-
-lemma signedInfDist_apply (x : P) :
-    s.signedInfDist p x = ⟪‖p -ᵥ orthogonalProjection s p‖⁻¹ • (p -ᵥ orthogonalProjection s p),
-      x -ᵥ orthogonalProjection s x⟫ :=
-  rfl
+  signedDist (p -ᵥ orthogonalProjection s p) (Classical.ofNonempty : s)
 
-lemma signedInfDist_linear : (s.signedInfDist p).linear =
-    (innerₗ V (‖p -ᵥ orthogonalProjection s p‖⁻¹ • (p -ᵥ orthogonalProjection s p))).comp
-      (LinearMap.id (R := ℝ) (M := V) -
-        s.direction.subtype.comp s.direction.orthogonalProjection.toLinearMap) :=
+lemma signedInfDist_def :
+    s.signedInfDist p = signedDist (p -ᵥ orthogonalProjection s p) ↑(Classical.ofNonempty : s) :=
   rfl
 
-lemma signedInfDist_linear_apply (v : V) : (s.signedInfDist p).linear v =
-    ⟪‖p -ᵥ orthogonalProjection s p‖⁻¹ • (p -ᵥ orthogonalProjection s p),
-     v - s.direction.orthogonalProjection v⟫ :=
-  rfl
+variable {s p q} in
+lemma signedInfDist_eq_signedDist_of_mem (h : q ∈ s) :
+    s.signedInfDist p = signedDist (p -ᵥ orthogonalProjection s p) q := by
+  apply signedDist_left_congr
+  apply s.direction.inner_left_of_mem_orthogonal
+  · exact vsub_mem_direction (SetLike.coe_mem _) h
+  · exact vsub_orthogonalProjection_mem_direction_orthogonal s p
+
+lemma signedInfDist_eq_signedDist_orthogonalProjection {x : P} : s.signedInfDist p x =
+    signedDist (p -ᵥ orthogonalProjection s p) ↑(orthogonalProjection s x) x := by
+  rw [signedInfDist_eq_signedDist_of_mem (orthogonalProjection_mem x)]
 
 @[simp] lemma signedInfDist_apply_self : s.signedInfDist p p = ‖p -ᵥ orthogonalProjection s p‖ := by
-  simp [signedInfDist_apply, inner_smul_left, real_inner_self_eq_norm_sq, pow_two, ← mul_assoc]
+  rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']
 
 variable {s} in
 @[simp] lemma signedInfDist_apply_of_mem {x : P} (hx : x ∈ s) : s.signedInfDist p x = 0 := by
-  simp [signedInfDist_apply, orthogonalProjection_eq_self_iff.2 hx]
+  simp [signedInfDist_eq_signedDist_orthogonalProjection, orthogonalProjection_eq_self_iff.2 hx]
 
 variable {s p} in
 @[simp] lemma signedInfDist_eq_const_of_mem (h : p ∈ s) :
     s.signedInfDist p = AffineMap.const ℝ P (0 : ℝ) := by
   ext x
-  simp [signedInfDist_apply, orthogonalProjection_eq_self_iff.2 h]
+  simp [signedInfDist_def, orthogonalProjection_eq_self_iff.2 h]
 
 variable {s p} in
 lemma abs_signedInfDist_eq_dist_of_mem_affineSpan_insert {x : P}
@@ -85,6 +258,10 @@ lemma abs_signedInfDist_eq_dist_of_mem_affineSpan_insert {x : P}
   simp [hp₀, dist_eq_norm_vsub, orthogonalProjection_eq_self_iff.2 hp₀,
     orthogonalProjection_vsub_orthogonalProjection, norm_smul, abs_mul]
 
+lemma signedInfDist_singleton :
+    (affineSpan ℝ ({q} : Set P)).signedInfDist p = signedDist (p -ᵥ q) q := by
+  simpa using signedInfDist_eq_signedDist_of_mem (mem_affineSpan ℝ (Set.mem_singleton q))
+
 end AffineSubspace
 
 namespace Affine