Signed distance to an affine subspace in a Euclidean space.

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.

References

• https://en.wikipedia.org/wiki/Trilinear_coordinates

noncomputable def signedDist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) : P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ

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 →ᴬ[ℝ] ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem signedDist_apply {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p : P) : (signedDist v) p = ((innerSL ℝ) (‖v‖⁻¹ • v)).toContinuousAffineMap.comp (ContinuousAffineMap.id ℝ P -ᵥ ContinuousAffineMap.const ℝ P p)

theorem signedDist_apply_apply {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : ((signedDist v) p) q = inner ℝ (‖v‖⁻¹ • v) (q -ᵥ p)

theorem signedDist_apply_linear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p : P) : (↑((signedDist v) p)).linear = (innerₗ V) (‖v‖⁻¹ • v)

theorem signedDist_apply_linear_apply {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p : P) : (↑((signedDist v) p)).linear w = inner ℝ (‖v‖⁻¹ • v) w

theorem signedDist_linear_apply {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) : (signedDist v).linear w = ContinuousAffineMap.const ℝ P (inner ℝ (-(‖v‖⁻¹ • v)) w)

theorem signedDist_linear_apply_apply {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p : P) : ((signedDist v).linear w) p = inner ℝ (-(‖v‖⁻¹ • v)) w

theorem signedDist_smul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) (r : ℝ) : ((signedDist (r • v)) p) q = ↑(SignType.sign r) * ((signedDist v) p) q

@[simp]

theorem signedDist_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p q : P) : ((signedDist 0) p) q = 0

@[simp]

theorem signedDist_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : ((signedDist (-v)) p) q = -((signedDist v) p) q

theorem signedDist_congr {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (h : ∃ r > 0, r • v = w) : signedDist v = signedDist w

@[simp]

theorem signedDist_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p : P) : ((signedDist v) p) p = 0

@[simp]

theorem signedDist_anticomm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : -((signedDist v) p) q = ((signedDist v) q) p

@[simp]

theorem signedDist_triangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q r : P) : ((signedDist v) p) q + ((signedDist v) q) r = ((signedDist v) p) r

@[simp]

theorem signedDist_triangle_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q r : P) : ((signedDist v) p) q - ((signedDist v) p) r = ((signedDist v) r) q

@[simp]

theorem signedDist_triangle_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q r : P) : ((signedDist v) p) r - ((signedDist v) q) r = ((signedDist v) p) q

theorem signedDist_vadd_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p q : P) : ((signedDist v) (w +ᵥ p)) q = -inner ℝ (‖v‖⁻¹ • v) w + ((signedDist v) p) q

theorem signedDist_vadd_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p q : P) : ((signedDist v) p) (w +ᵥ q) = inner ℝ (‖v‖⁻¹ • v) w + ((signedDist v) p) q

theorem signedDist_vadd_left_swap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p q : P) : ((signedDist v) (w +ᵥ p)) q = ((signedDist v) p) (-w +ᵥ q)

theorem signedDist_vadd_right_swap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p q : P) : ((signedDist v) p) (w +ᵥ q) = ((signedDist v) (-w +ᵥ p)) q

theorem signedDist_vadd_vadd {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v w : V) (p q : P) : ((signedDist v) (w +ᵥ p)) (w +ᵥ q) = ((signedDist v) p) q

theorem signedDist_left_congr {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} {p q : P} (h : inner ℝ v (p -ᵥ q) = 0) : (signedDist v) p = (signedDist v) q

theorem signedDist_right_congr {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} (p : P) {q r : P} (h : inner ℝ v (q -ᵥ r) = 0) : ((signedDist v) p) q = ((signedDist v) p) r

theorem signedDist_eq_zero_of_orthogonal {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} {p q : P} (h : inner ℝ v (q -ᵥ p) = 0) : ((signedDist v) p) q = 0

theorem abs_signedDist_le_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : |((signedDist v) p) q| ≤ dist p q

theorem signedDist_le_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : ((signedDist v) p) q ≤ dist p q

theorem abs_signedDist_eq_dist_iff_vsub_mem_span {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : |((signedDist v) p) q| = dist p q ↔ q -ᵥ p ∈ Submodule.span ℝ {v}

theorem signedDist_eq_dist_iff_vsub_mem_span {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p q : P) : ((signedDist v) p) q = dist p q ↔ q -ᵥ p ∈ Submodule.span NNReal {v}

@[simp]

theorem signedDist_vsub_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p q : P) : ((signedDist (q -ᵥ p)) p) q = dist p q

@[simp]

theorem signedDist_vsub_self_rev {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p q : P) : ((signedDist (p -ᵥ q)) p) q = -dist p q

noncomputable def AffineSubspace.signedInfDist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : 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).

Equations

• s.signedInfDist p = (signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) ↑Classical.ofNonempty

theorem AffineSubspace.signedInfDist_def {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : s.signedInfDist p = (signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) ↑Classical.ofNonempty

theorem AffineSubspace.signedInfDist_eq_signedDist_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p q : P} (h : q ∈ s) : s.signedInfDist p = (signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) q

theorem AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) {x : P} : (s.signedInfDist p) x = ((signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) ↑((EuclideanGeometry.orthogonalProjection s) x)) x

@[simp]

theorem AffineSubspace.signedInfDist_apply_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (s.signedInfDist p) p = ‖p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)‖

@[simp]

theorem AffineSubspace.signedInfDist_apply_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) {x : P} (hx : x ∈ s) : (s.signedInfDist p) x = 0

@[simp]

theorem AffineSubspace.signedInfDist_eq_const_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} (h : p ∈ s) : ↑(s.signedInfDist p) = AffineMap.const ℝ P 0

theorem AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p x : P} (h : x ∈ affineSpan ℝ (insert p ↑s)) : |(s.signedInfDist p) x| = dist x ↑((EuclideanGeometry.orthogonalProjection s) x)

theorem AffineSubspace.signedInfDist_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p q : P) : (affineSpan ℝ {q}).signedInfDist p = (signedDist (p -ᵥ q)) q

noncomputable def Affine.Simplex.signedInfDist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : P →ᴬ[ℝ] ℝ

The signed distance between the face of s excluding point i of that simplex and a point, in the direction of the reference point i. This is expected to be used when the point at which the distance is evaluated lies in the affine span of the simplex (any component of the distance orthogonal to that span is disregarded). In the case of a triangle, these distances are trilinear coordinates; in a tetrahedron, they are quadriplanar coordinates.

Equations

• s.signedInfDist i = (affineSpan ℝ (s.points '' {i}ᶜ)).signedInfDist (s.points i)

theorem Affine.Simplex.signedInfDist_apply_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : (s.signedInfDist i) (s.points i) = ‖s.points i -ᵥ ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))‖

theorem Affine.Simplex.signedInfDist_apply_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {i j : Fin (n + 1)} (h : j ≠ i) : (s.signedInfDist i) (s.points j) = 0

theorem Affine.Simplex.signedInfDist_affineCombination {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) {w : Fin (n + 1) → ℝ} (h : ∑ i : Fin (n + 1), w i = 1) : (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = w i * ‖s.points i -ᵥ ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))‖

theorem Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} (i : Fin (n + 1)) {p : P} (h : p ∈ affineSpan ℝ (Set.range s.points)) : |(s.signedInfDist i) p| = dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p)