Euclidean spaces
This file makes some definitions and proves very basic geometrical
results about real inner product spaces and Euclidean affine spaces.
Results about real inner product spaces that involve the norm and
inner product but not angles generally go in
analysis.normed_space.real_inner_product. Results with longer
proofs or more geometrical content generally go in separate files.
Main definitions
inner_product_geometry.angleis the undirected angle between two vectors.euclidean_geometry.angle, with notation∠, is the undirected angle determined by three points.euclidean_geometry.orthogonal_projectionis the orthogonal projection of a point onto an affine subspace.
Implementation notes
To declare P as the type of points in a Euclidean affine space with
V as the type of vectors, use [inner_product_space V] [metric_space P]
[normed_add_torsor V P]. This works better with out_param to make
V implicit in most cases than having a separate type alias for
Euclidean affine spaces.
Rather than requiring Euclidean affine spaces to be finite-dimensional (as in the definition on Wikipedia), this is specified only for those theorems that need it.
References
- https://en.wikipedia.org/wiki/Euclidean_space
Geometrical results on real inner product spaces
This section develops some geometrical definitions and results on real inner product spaces, where those definitions and results can most conveniently be developed in terms of vectors and then used to deduce corresponding results for Euclidean affine spaces.
The undirected angle between two vectors. If either vector is 0, this is π/2.
Equations
- inner_product_geometry.angle x y = (has_inner.inner x y / (∥x∥ * ∥y∥)).arccos
The cosine of the angle between two vectors.
The angle between two vectors does not depend on their order.
The angle between the negation of two vectors.
The angle between two vectors is nonnegative.
The angle between two vectors is at most π.
The angle between a vector and the negation of another vector.
The angle between the negation of a vector and another vector.
The angle between the zero vector and a vector.
The angle between a vector and the zero vector.
The angle between a nonzero vector and itself.
The angle between a nonzero vector and its negation.
The angle between the negation of a nonzero vector and that vector.
The angle between a vector and a positive multiple of a vector.
The angle between a positive multiple of a vector and a vector.
The angle between a vector and a negative multiple of a vector.
The angle between a negative multiple of a vector and a vector.
The cosine of the angle between two vectors, multiplied by the product of their norms.
The sine of the angle between two vectors, multiplied by the product of their norms.
The angle between two vectors is zero if and only if they are nonzero and one is a positive multiple of the other.
The angle between two vectors is π if and only if they are nonzero and one is a negative multiple of the other.
If the angle between two vectors is π, the angles between those vectors and a third vector add to π.
Two vectors have inner product 0 if and only if the angle between them is π/2.
Geometrical results on Euclidean affine spaces
This section develops some geometrical definitions and results on Euclidean affine spaces.
The undirected angle at p2 between the line segments to p1 and
p3. If either of those points equals p2, this is π/2. Use
open_locale euclidean_geometry to access the ∠ p1 p2 p3
notation.
Equations
- euclidean_geometry.angle p1 p2 p3 = inner_product_geometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2)
The angle at a point does not depend on the order of the other two points.
The angle at a point is nonnegative.
The angle at a point is at most π.
The angle ∠AAB at a point.
The angle ∠ABB at a point.
The angle ∠ABA at a point.
If the angle ∠ABC at a point is π, the angle ∠BAC is 0.
If the angle ∠ABC at a point is π, the angle ∠BCA is 0.
If ∠BCD = π, then ∠ABC = ∠ABD.
If ∠BCD = π, then ∠ACB + ∠ACD = π.
The inner product of two vectors given with weighted_vsub, in
terms of the pairwise distances.
The distance between two points given with affine_combination,
in terms of the pairwise distances between the points in that
combination.
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
orthogonal_projection and should not be used once that is
defined.
Equations
The intersection of the subspace and the orthogonal subspace
through the given point is the orthogonal_projection_fn 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 orthogonal_projection_fn 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 orthogonal_projection_fn 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 orthogonal_projection_fn 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.
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 orthogonal_projection
for real inner product spaces, onto the direction of the affine
subspace being projected onto.
Equations
- euclidean_geometry.orthogonal_projection hn hc = {to_fun := euclidean_geometry.orthogonal_projection_fn hn hc, linear := orthogonal_projection hc, map_vadd' := _}
The intersection of the subspace and the orthogonal subspace
through the given point is the orthogonal_projection of that point
onto the subspace.
The orthogonal_projection lies in the given subspace.
The orthogonal_projection lies in the orthogonal subspace.
Subtracting a point in the given subspace from the
orthogonal_projection produces a result in the direction of the
given subspace.
Subtracting the orthogonal_projection 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.
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 orthogonal_projection produces a result
in the orthogonal direction.
Subtracting the orthogonal_projection from p produces a result
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 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
orthogonal_projection.
The square of the distance between two points constructed by adding multiples of the same orthogonal vector to points in the same subspace.