Orthogonal projection in Euclidean affine spaces #
This file defines orthogonal projection onto an affine subspace in a Euclidean affine space, and reflection of a point in an affine subspace.
Main definitions #
EuclideanGeometry.orthogonalProjection
is the orthogonal projection of a point onto an affine subspace.EuclideanGeometry.reflection
is the reflection of a point in an affine subspace.
The orthogonal projection of a point onto a nonempty affine
subspace, whose direction is complete, as an unbundled function. This
definition is only intended for use in setting up the bundled version
orthogonalProjection
and should not be used once that is
defined.
Equations
Instances For
The intersection of the subspace and the orthogonal subspace
through the given point is the orthogonalProjectionFn
of that
point onto the subspace. This lemma is only intended for use in
setting up the bundled version and should not be used once that is
defined.
The orthogonalProjectionFn
lies in the given subspace. This
lemma is only intended for use in setting up the bundled version and
should not be used once that is defined.
The orthogonalProjectionFn
lies in the orthogonal
subspace. This lemma is only intended for use in setting up the
bundled version and should not be used once that is defined.
Subtracting p
from its orthogonalProjectionFn
produces a
result in the orthogonal direction. This lemma is only intended for
use in setting up the bundled version and should not be used once that
is defined.
Auxiliary definition for setting up the orthogonal projection. This one is a bundled affine
map; the final orthogonalProjection
is a continuous affine map.
Equations
- EuclideanGeometry.orthogonalProjectionAux s = { toFun := fun (p : P) => ⟨EuclideanGeometry.orthogonalProjectionFn s p, ⋯⟩, linear := ↑s.direction.orthogonalProjection, map_vadd' := ⋯ }
Instances For
The orthogonal projection of a point onto a nonempty affine
subspace, whose direction is complete. The corresponding linear map
(mapping a vector to the difference between the projections of two
points whose difference is that vector) is the orthogonalProjection
for real inner product spaces, onto the direction of the affine
subspace being projected onto.
Equations
- EuclideanGeometry.orthogonalProjection s = { toAffineMap := EuclideanGeometry.orthogonalProjectionAux s, cont := ⋯ }
Instances For
The linear map corresponding to orthogonalProjection
.
The continuous linear map corresponding to orthogonalProjection
.
The intersection of the subspace and the orthogonal subspace
through the given point is the orthogonalProjection
of that point
onto the subspace.
The orthogonalProjection
lies in the given subspace.
The orthogonalProjection
lies in the orthogonal subspace.
Subtracting a point in the given subspace from the
orthogonalProjection
produces a result in the direction of the
given subspace.
Subtracting the orthogonalProjection
from a point in the given
subspace produces a result in the direction of the given subspace.
A point equals its orthogonal projection if and only if it lies in the subspace.
Orthogonal projection is idempotent.
The distance to a point's orthogonal projection is 0 iff it lies in the subspace.
The distance between a point and its orthogonal projection is nonzero if it does not lie in the subspace.
Subtracting p
from its orthogonalProjection
produces a result
in the orthogonal direction.
Subtracting the orthogonalProjection
from p
produces a result
in the orthogonal direction.
Subtracting the orthogonalProjection
from p
produces a result in the kernel of the linear
part of the orthogonal projection.
Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector was in the orthogonal direction.
Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.
The square of the distance from a point in s
to p₂
equals the
sum of the squares of the distances of the two points to the
orthogonalProjection
.
The distance between a point and its orthogonal projection to a subspace equals the distance
to that subspace as given by Metric.infDist
. This is not a simp
lemma since the simplest form
depends on the context (if any calculations are to be done with the distance, the version with
the orthogonal projection gives access to more lemmas about orthogonal projections that may be
useful).
The nonnegative distance between a point and its orthogonal projection to a subspace equals
the distance to that subspace as given by Metric.infNndist
. This is not a simp
lemma since
the simplest form depends on the context (if any calculations are to be done with the distance,
the version with the orthogonal projection gives access to more lemmas about orthogonal
projections that may be useful).
The square of the distance between two points constructed by adding multiples of the same orthogonal vector to points in the same subspace.
p
is equidistant from two points in s
if and only if its
orthogonalProjection
is.
p
is equidistant from a set of points in s
if and only if its
orthogonalProjection
is.
There exists r
such that p
has distance r
from all the
points of a set of points in s
if and only if there exists (possibly
different) r
such that its orthogonalProjection
has that distance
from all the points in that set.
Reflection in an affine subspace, which is expected to be nonempty and complete. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in an affine subspace, is a more general sense of the word that includes both those common cases.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The result of reflecting.
Reflecting twice in the same subspace.
Reflection is its own inverse.
Reflection is involutive.
A point is its own reflection if and only if it is in the subspace.
Reflecting a point in two subspaces produces the same result if and only if the point has the same orthogonal projection in each of those subspaces.
The distance between p₁
and the reflection of p₂
equals that
between the reflection of p₁
and p₂
.
A point in the subspace is equidistant from another point and its reflection.
The reflection of a point in a subspace is contained in any larger subspace containing both the point and the subspace reflected in.
Reflecting an orthogonal vector plus a point in the subspace produces the negation of that vector plus the point.
Reflecting a vector plus a point in the subspace produces the negation of that vector plus the point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.
The orthogonal projection of a point p
onto the hyperplane spanned by the simplex's points.
Equations
Instances For
Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.