Oriented angles. #
This file defines oriented angles in real inner product spaces.
Main definitions #
-
orientation.oangle
is the oriented angle between two vectors with respect to an orientation. -
orientation.rotation
is the rotation by an oriented angle with respect to an orientation.
Implementation notes #
The definitions here use the real.angle
type, angles modulo 2 * π
. For some purposes,
angles modulo π
are more convenient, because results are true for such angles with less
configuration dependence. Results that are only equalities modulo π
can be represented
modulo 2 * π
as equalities of (2 : ℤ) • θ
.
Definitions and results in the orthonormal
namespace, with respect to a particular choice
of orthonormal basis, are mainly for use in setting up the API and proving that certain
definitions do not depend on the choice of basis for a given orientation. Applications should
generally use the definitions and results in the orientation
namespace instead.
References #
- Evan Chen, Euclidean Geometry in Mathematical Olympiads.
The oriented angle from x
to y
, modulo 2 * π
. If either vector is 0, this is 0.
Oriented angles are continuous when the vectors involved are nonzero.
If the first vector passed to oangle
is 0, the result is 0.
If the second vector passed to oangle
is 0, the result is 0.
If the two vectors passed to oangle
are the same, the result is 0.
Swapping the two vectors passed to oangle
negates the angle.
Adding the angles between two vectors in each order results in 0.
Negating both vectors passed to oangle
does not change the angle.
Negating the first vector produces the same angle as negating the second vector.
Twice the angle between the negation of a vector and that vector is 0.
Twice the angle between a vector and its negation is 0.
Adding the angles between two vectors in each order, with the first vector in each angle negated, results in 0.
Adding the angles between two vectors in each order, with the second vector in each angle negated, results in 0.
Multiplying the first vector passed to oangle
by a positive real does not change the
angle.
Multiplying the second vector passed to oangle
by a positive real does not change the
angle.
Multiplying the first vector passed to oangle
by a negative real produces the same angle
as negating that vector.
Multiplying the second vector passed to oangle
by a negative real produces the same angle
as negating that vector.
The angle between a nonnegative multiple of a vector and that vector is 0.
The angle between a vector and a nonnegative multiple of that vector is 0.
The angle between two nonnegative multiples of the same vector is 0.
Multiplying the first vector passed to oangle
by a nonzero real does not change twice the
angle.
Multiplying the second vector passed to oangle
by a nonzero real does not change twice the
angle.
Twice the angle between a multiple of a vector and that vector is 0.
Twice the angle between a vector and a multiple of that vector is 0.
The oriented angle between two vectors is zero if and only if the angle with the vectors swapped is zero.
The oriented angle between two vectors is zero if and only if they are on the same ray.
The oriented angle between two vectors is π
if and only if the angle with the vectors
swapped is π
.
The oriented angle between two vectors is π
if and only they are nonzero and the first is
on the same ray as the negation of the second.
The oriented angle between two vectors is zero or π
if and only if those two vectors are
not linearly independent.
The oriented angle between two vectors is zero or π
if and only if the first vector is zero
or the second is a multiple of the first.
The oriented angle between two vectors is not zero or π
if and only if those two vectors
are linearly independent.
Given three nonzero vectors, the angle between the first and the second plus the angle between the second and the third equals the angle between the first and the third.
Given three nonzero vectors, the angle between the second and the third plus the angle between the first and the second equals the angle between the first and the third.
Given three nonzero vectors, the angle between the first and the third minus the angle between the first and the second equals the angle between the second and the third.
Given three nonzero vectors, the angle between the first and the third minus the angle between the second and the third equals the angle between the first and the second.
Given three nonzero vectors, adding the angles between them in cyclic order results in 0.
Given three nonzero vectors, adding the angles between them in cyclic order, with the first vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.
Given three nonzero vectors, adding the angles between them in cyclic order, with the second vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.
The angle at the apex of an isosceles triangle is π
minus twice a base angle, oriented
vector angle form.
Angle at center of a circle equals twice angle at circumference, oriented vector angle form.
Angle at center of a circle equals twice angle at circumference, oriented vector angle form with radius specified.
Oriented vector angle version of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result), represented here as equality of twice the angles.
A rotation by the oriented angle θ
.
Equations
- hb.rotation θ = ((complex.isometry_of_orthonormal hb).symm.trans (⇑rotation θ.exp_map_circle)).trans (complex.isometry_of_orthonormal hb)
The determinant of rotation
(as a linear map) is equal to 1
.
The determinant of rotation
(as a linear equiv) is equal to 1
.
The inverse of rotation
is rotation by the negation of the angle.
Rotation by 0 is the identity.
Rotation by π is negation.
Rotating twice is equivalent to rotating by the sum of the angles.
Rotating the first vector by θ
subtracts θ
from the angle between two vectors.
Rotating the second vector by θ
adds θ
to the angle between two vectors.
The rotation of a vector by θ
has an angle of -θ
from that vector.
A vector has an angle of θ
from the rotation of that vector by θ
.
Rotating the first vector by the angle between the two vectors results an an angle of 0.
Rotating the first vector by the angle between the two vectors and swapping the vectors results an an angle of 0.
Rotating both vectors by the same angle does not change the angle between those vectors.
A rotation of a nonzero vector equals that vector if and only if the angle is zero.
A nonzero vector equals a rotation of that vector if and only if the angle is zero.
A rotation of a vector equals that vector if and only if the vector or the angle is zero.
A vector equals a rotation of that vector if and only if the vector or the angle is zero.
Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.
The angle between two nonzero vectors is θ
if and only if the second vector is the first
rotated by θ
and scaled by the ratio of the norms.
The angle between two nonzero vectors is θ
if and only if the second vector is the first
rotated by θ
and scaled by a positive real.
The angle between two vectors is θ
if and only if they are nonzero and the second vector
is the first rotated by θ
and scaled by the ratio of the norms, or θ
and at least one of the
vectors are zero.
The angle between two vectors is θ
if and only if they are nonzero and the second vector
is the first rotated by θ
and scaled by a positive real, or θ
and at least one of the
vectors are zero.
Complex conjugation as a linear isometric equivalence in V
. Note that this definition
depends on the choice of basis, not just on its orientation; for most geometrical purposes,
the reflection
definitions should be preferred instead.
Equations
The determinant of conj_lie
(as a linear map) is equal to -1
.
The determinant of conj_lie
(as a linear equiv) is equal to -1
.
conj_lie
is its own inverse.
Any linear isometric equivalence in V
is rotation
or conj_lie
composed with
rotation
.
Any linear isometric equivalence in V
with positive determinant is rotation
.
Any linear isometric equivalence in V
with negative determinant is conj_lie
composed
with rotation
.
Two bases with the same orientation are related by a rotation
.
Two bases with opposite orientations are related by conj_lie
composed with a rotation
.
The angle between two vectors, with respect to a basis given by basis.map
with a linear
isometric equivalence, equals the angle between those two vectors, transformed by the inverse of
that equivalence, with respect to the original basis.
The value of oangle
does not depend on the choice of basis for a given orientation.
Negating the orientation negates the value of oangle
.
rotation
does not depend on the choice of basis for a given orientation.
Negating the orientation negates the angle in rotation
.
The inner product of two vectors is the product of the norms and the cosine of the oriented angle between the vectors.
The cosine of the oriented angle between two nonzero vectors is the inner product divided by the product of the norms.
The cosine of the oriented angle between two nonzero vectors equals that of the unoriented angle.
The oriented angle between two nonzero vectors is plus or minus the unoriented angle.
The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, converted to a real.
If the sign of the oriented angle between two vectors is zero, either one of the vectors is zero or the unoriented angle is 0 or π.
If two unoriented angles are equal, and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (even in degenerate cases).
If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are equal if and only if the unoriented angles are equal.
The oriented angle between two nonzero vectors is zero if and only if the unoriented angle is zero.
The oriented angle between two vectors is π
if and only if the unoriented angle is π
.
The oriented angle from x
to y
, modulo 2 * π
. If either vector is 0, this is 0.
See inner_product_geometry.angle
for the corresponding unoriented angle definition.
Oriented angles are continuous when the vectors involved are nonzero.
If the first vector passed to oangle
is 0, the result is 0.
If the second vector passed to oangle
is 0, the result is 0.
If the two vectors passed to oangle
are the same, the result is 0.
Swapping the two vectors passed to oangle
negates the angle.
Adding the angles between two vectors in each order results in 0.
Negating the first vector passed to oangle
adds π
to the angle.
Negating the second vector passed to oangle
adds π
to the angle.
Negating the first vector passed to oangle
does not change twice the angle.
Negating the second vector passed to oangle
does not change twice the angle.
Negating both vectors passed to oangle
does not change the angle.
Negating the first vector produces the same angle as negating the second vector.
The angle between the negation of a nonzero vector and that vector is π
.
The angle between a nonzero vector and its negation is π
.
Twice the angle between the negation of a vector and that vector is 0.
Twice the angle between a vector and its negation is 0.
Adding the angles between two vectors in each order, with the first vector in each angle negated, results in 0.
Adding the angles between two vectors in each order, with the second vector in each angle negated, results in 0.
Multiplying the first vector passed to oangle
by a positive real does not change the
angle.
Multiplying the second vector passed to oangle
by a positive real does not change the
angle.
Multiplying the first vector passed to oangle
by a negative real produces the same angle
as negating that vector.
Multiplying the second vector passed to oangle
by a negative real produces the same angle
as negating that vector.
The angle between a nonnegative multiple of a vector and that vector is 0.
The angle between a vector and a nonnegative multiple of that vector is 0.
The angle between two nonnegative multiples of the same vector is 0.
Multiplying the first vector passed to oangle
by a nonzero real does not change twice the
angle.
Multiplying the second vector passed to oangle
by a nonzero real does not change twice the
angle.
Twice the angle between a multiple of a vector and that vector is 0.
Twice the angle between a vector and a multiple of that vector is 0.
Twice the angle between two multiples of a vector is 0.
The oriented angle between two vectors is zero if and only if the angle with the vectors swapped is zero.
The oriented angle between two vectors is zero if and only if they are on the same ray.
The oriented angle between two vectors is π
if and only if the angle with the vectors
swapped is π
.
The oriented angle between two vectors is π
if and only they are nonzero and the first is
on the same ray as the negation of the second.
The oriented angle between two vectors is zero or π
if and only if those two vectors are
not linearly independent.
The oriented angle between two vectors is zero or π
if and only if the first vector is zero
or the second is a multiple of the first.
The oriented angle between two vectors is not zero or π
if and only if those two vectors
are linearly independent.
Two vectors are equal if and only if they have equal norms and zero angle between them.
Two vectors with equal norms are equal if and only if they have zero angle between them.
Two vectors with zero angle between them are equal if and only if they have equal norms.
Given three nonzero vectors, the angle between the first and the second plus the angle between the second and the third equals the angle between the first and the third.
Given three nonzero vectors, the angle between the second and the third plus the angle between the first and the second equals the angle between the first and the third.
Given three nonzero vectors, the angle between the first and the third minus the angle between the first and the second equals the angle between the second and the third.
Given three nonzero vectors, the angle between the first and the third minus the angle between the second and the third equals the angle between the first and the second.
Given three nonzero vectors, adding the angles between them in cyclic order results in 0.
Given three nonzero vectors, adding the angles between them in cyclic order, with the first vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.
Given three nonzero vectors, adding the angles between them in cyclic order, with the second vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.
The angle at the apex of an isosceles triangle is π
minus twice a base angle, oriented
vector angle form.
Angle at center of a circle equals twice angle at circumference, oriented vector angle form.
Angle at center of a circle equals twice angle at circumference, oriented vector angle form with radius specified.
Oriented vector angle version of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result), represented here as equality of twice the angles.
A rotation by the oriented angle θ
.
The determinant of rotation
(as a linear map) is equal to 1
.
The determinant of rotation
(as a linear equiv) is equal to 1
.
The inverse of rotation
is rotation by the negation of the angle.
Rotation by 0 is the identity.
Rotation by π is negation.
Rotating twice is equivalent to rotating by the sum of the angles.
Rotating the first vector by θ
subtracts θ
from the angle between two vectors.
Rotating the second vector by θ
adds θ
to the angle between two vectors.
The rotation of a vector by θ
has an angle of -θ
from that vector.
A vector has an angle of θ
from the rotation of that vector by θ
.
Rotating the first vector by the angle between the two vectors results an an angle of 0.
Rotating the first vector by the angle between the two vectors and swapping the vectors results an an angle of 0.
Rotating both vectors by the same angle does not change the angle between those vectors.
A rotation of a nonzero vector equals that vector if and only if the angle is zero.
A nonzero vector equals a rotation of that vector if and only if the angle is zero.
A rotation of a vector equals that vector if and only if the vector or the angle is zero.
A vector equals a rotation of that vector if and only if the vector or the angle is zero.
Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.
The angle between two nonzero vectors is θ
if and only if the second vector is the first
rotated by θ
and scaled by the ratio of the norms.
The angle between two nonzero vectors is θ
if and only if the second vector is the first
rotated by θ
and scaled by a positive real.
The angle between two vectors is θ
if and only if they are nonzero and the second vector
is the first rotated by θ
and scaled by the ratio of the norms, or θ
and at least one of the
vectors are zero.
The angle between two vectors is θ
if and only if they are nonzero and the second vector
is the first rotated by θ
and scaled by a positive real, or θ
and at least one of the
vectors are zero.
Any linear isometric equivalence in V
with positive determinant is rotation
.
The angle between two vectors, with respect to an orientation given by orientation.map
with a linear isometric equivalence, equals the angle between those two vectors, transformed by
the inverse of that equivalence, with respect to the original orientation.
orientation.oangle
equals orthonormal.oangle
for any orthonormal basis with that
orientation.
Negating the orientation negates the value of oangle
.
orientation.rotation
equals orthonormal.rotation
for any orthonormal basis with that
orientation.
Negating the orientation negates the angle in rotation
.
The inner product of two vectors is the product of the norms and the cosine of the oriented angle between the vectors.
The cosine of the oriented angle between two nonzero vectors is the inner product divided by the product of the norms.
The cosine of the oriented angle between two nonzero vectors equals that of the unoriented angle.
The oriented angle between two nonzero vectors is plus or minus the unoriented angle.
The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, converted to a real.
If the sign of the oriented angle between two vectors is zero, either one of the vectors is zero or the unoriented angle is 0 or π.
If two unoriented angles are equal, and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (even in degenerate cases).
If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are equal if and only if the unoriented angles are equal.
The oriented angle between two nonzero vectors is zero if and only if the unoriented angle is zero.
The oriented angle between two vectors is π
if and only if the unoriented angle is π
.