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.
Main definitions #
AffineSubspace.signedDistis the signed distance between an affine subspace and a point.Affine.Simplex.signedDistis the signed distance between a face of a simplex and a point. In the case of a triangle, these distances are trilinear coordinates.
References #
noncomputable def
AffineSubspace.signedDist
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace ℝ P)
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
(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
- One or more equations did not get rendered due to their size.
Instances For
theorem
AffineSubspace.signedDist_apply
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace ℝ P)
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
(p x : P)
:
(s.signedDist p) x = inner
(‖p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)‖⁻¹ • (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)))
(x -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) x))
theorem
AffineSubspace.signedDist_linear
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace ℝ P)
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
(p : P)
:
(s.signedDist p).linear = (innerₗ V)
(‖p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)‖⁻¹ • (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) ∘ₗ (LinearMap.id - s.direction.subtype ∘ₗ ↑(orthogonalProjection s.direction))
theorem
AffineSubspace.signedDist_linear_apply
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace ℝ P)
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
(p : P)
(v : V)
:
(s.signedDist p).linear v = inner
(‖p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)‖⁻¹ • (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)))
(v - ↑((orthogonalProjection s.direction) v))
@[simp]
theorem
AffineSubspace.signedDist_apply_self
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace ℝ P)
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
(p : P)
:
@[simp]
theorem
AffineSubspace.signedDist_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]
[HasOrthogonalProjection s.direction]
(p : P)
{x : P}
(hx : x ∈ s)
:
@[simp]
theorem
AffineSubspace.signedDist_eq_const_of_left_mem
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{s : AffineSubspace ℝ P}
[Nonempty ↥s]
[HasOrthogonalProjection s.direction]
{p : P}
(h : p ∈ s)
:
theorem
AffineSubspace.abs_signedDist_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]
[HasOrthogonalProjection s.direction]
{p x : P}
(h : x ∈ affineSpan ℝ (insert p ↑s))
:
noncomputable def
Affine.Simplex.signedDist
{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))
:
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.signedDist i = (affineSpan ℝ (Set.range (s.faceOpposite i).points)).signedDist (s.points i)
Instances For
theorem
Affine.Simplex.signedDist_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.signedDist i) (s.points i) = ‖s.points i -ᵥ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i))‖
theorem
Affine.Simplex.signedDist_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)
:
theorem
Affine.Simplex.signedDist_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.signedDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = w i * ‖s.points i -ᵥ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i))‖
theorem
Affine.Simplex.abs_signedDist_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.signedDist i) p| = dist p ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) p)