Orientation.inner_rotation_pi_div_two_left
theorem Orientation.inner_rotation_pi_div_two_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
⟪(o.rotation ↑(Real.pi / 2)) x, x⟫_ℝ = 0
The theorem `Orientation.inner_rotation_pi_div_two_left` states that for any 2-dimensional real vector space `V` with an orientation `o` and any vector `x` in `V`, the inner product of `x` with its own image under a rotation by an angle of `π/2` (90 degrees) is zero. In mathematical terms, this implies that the rotation results in a vector that is orthogonal to the original vector `x` in the chosen orientation.
More concisely: For any 2-dimensional real vector space with orientation, and any vector x, the inner product of x and its rotation by π/2 is zero.
|
Orientation.inner_rotation_pi_div_two_left_smul
theorem Orientation.inner_rotation_pi_div_two_left_smul :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ),
⟪(o.rotation ↑(Real.pi / 2)) x, r • x⟫_ℝ = 0
This theorem states that for any real vector space `V` that is also an inner product space, given that it has a finite rank of 2, any orientation `o` of `V`, any vector `x` in `V`, and any real number `r`, the inner product of a `π / 2` rotation of the vector `x` under the orientation `o` and the scalar multiple of `x` by `r` is equal to zero. In other words, a 90-degree rotation of a vector and any scalar multiple of the original vector are orthogonal to each other in a 2-dimensional real vector space.
More concisely: In a 2-dimensional real inner product space, the inner product of a vector and its 90-degree rotation under a given orientation is zero for any scalar multiple of the original vector.
|
Orientation.rotation_eq_self_iff
theorem Orientation.rotation_eq_self_iff :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle),
(o.rotation θ) x = x ↔ x = 0 ∨ θ = 0
This theorem states that for a two-dimensional real inner product space (a plane), given an orientation of this space, a vector in this plane, and an angle, rotating the vector by the given angle results in the original vector if and only if either the vector is the zero vector or the angle is zero. This is the mathematical way of saying that a rotation changes a vector unless the rotation angle is zero (which leaves the vector unchanged) or the vector is the zero vector (which is invariant under rotations).
More concisely: In a two-dimensional real inner product space with a fixed orientation, a non-zero vector is unchanged under rotation if and only if the rotation angle is zero.
|
Orientation.rotation_pi_apply
theorem Orientation.rotation_pi_apply :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
(o.rotation ↑Real.pi) x = -x
The theorem `Orientation.rotation_pi_apply` states that for any 2-dimensional real vector space `V` with a chosen orientation `o` and any vector `x` in `V`, the operation of rotation by an angle of `π` radians, as defined by the given orientation, is equivalent to negating the vector `x`. This means that rotating any vector in this space by `π` radians, which is equivalent to a 180-degree rotation, results in the vector pointing in the opposite direction.
More concisely: For any 2-dimensional real vector space with orientation and any vector, rotating the vector by angle π radians (180 degrees) according to the given orientation is equivalent to negating the vector.
|
Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero
theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
This theorem states that for a real inner product space of finite dimension 2 with a given orientation, the angle `θ` between two nonzero vectors `x` and `y` is equal to the argument of the complex number obtained by rotating `x` by `θ` and scaling by the ratio of the norms of `y` to `x` if and only if `y` is the result of this rotation and scaling of `x`. Specifically, if `x` and `y` are nonzero vectors in our space, and `θ` is a real angle, then the orientation angle of `x` and `y` is `θ` if and only if `y` equals the norm of `y` divided by the norm of `x`, scaled by `x` rotated by `θ`.
More concisely: For two nonzero vectors x and y in a real inner product space of finite dimension 2 with given orientation, their angle θ is equal to the argument of the norm of y divided by the norm of x times the rotation of x by θ if and only if y is obtained by rotating x by θ and scaling by the ratio of the norms.
|
Orientation.inner_smul_rotation_pi_div_two_smul_left
theorem Orientation.inner_smul_rotation_pi_div_two_smul_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ r₂ : ℝ),
⟪r₁ • (o.rotation ↑(Real.pi / 2)) x, r₂ • x⟫_ℝ = 0
This theorem states that for a certain 2-dimensional vector space `V` over the real numbers with an orientation `o`, if a vector `x` in this space is rotated by `π / 2` (90 degrees) and then scaled by a real number `r₁`, and the original vector `x` is scaled by another real number `r₂`, the inner product between these two resultant vectors is always zero. In other words, these two vectors are orthogonal.
More concisely: For any vector space `V` over the real numbers with orientation `o`, and vectors `x` and `y` in `V`, if `y` is obtained from `x` by rotating 90 degrees and scaling by `r₁`, and `x` is scaled by `r₂`, then `x · y = 0` (where `·` denotes the inner product).
|
Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero
theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (θ : Real.Angle),
o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
The theorem `Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero` states that for a 2-dimensional normed, inner product space V over the real numbers ℝ with a given orientation o, the angle θ between two vectors x and y is equal to `o.oangle x y` if and only if either:
1) both x and y are non-zero vectors and y is equal to the vector obtained by rotating x by angle θ and scaling it by the ratio of the norms of y to x, i.e., `‖y‖ / ‖x‖`;
or 2) θ is equal to zero and at least one of the vectors x or y is zero.
More concisely: The angle between two vectors x and y in a 2-dimensional real normed inner product space with orientation o is equal to o.oangle x y if and only if either both are non-zero and y is a scaled and rotated version of x, or the angle is zero and at least one is zero.
|
Orientation.neg_rotation
theorem Orientation.neg_rotation :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V),
-(o.rotation θ) x = (o.rotation (↑Real.pi + θ)) x
This theorem, `Orientation.neg_rotation`, states that for every 2-dimensional inner product space `V` over the real numbers `ℝ`, for every orientation `o` of `V`, for every angle `θ`, and for every vector `x` in `V`, the negative of the rotation by `θ` applied to `x` is equivalent to the rotation by `π + θ` applied to `x`. In simpler terms, this means reversing the direction (negating) of a rotation is the same as rotating by an additional 180 degrees (π radians).
More concisely: For every 2-dimensional real inner product space, every orientation, every angle θ, and every vector x, the negative of the rotation by θ about the origin is equivalent to the rotation by π + θ about the origin.
|
Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero
theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (θ : Real.Angle),
o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
The theorem `Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero` states that for any vectors `x` and `y` in a two-dimensional real inner product space with a given orientation, the orientation angle between `x` and `y` is equal to a real angle `θ` if and only if either both `x` and `y` are non-zero vectors and `y` is a positive real scalar multiple of `x` rotated by `θ`, or `θ` is zero and at least one of the vectors is zero.
More concisely: The orientation angle between two non-zero vectors in a 2-dimensional real inner product space is equal to the angle of rotation of one vector into the other plus or minus zero, if and only if they are scalar multiples, or one is zero.
|
Orientation.kahler_rotation_left'
theorem Orientation.kahler_rotation_left' :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
(o.kahler ((o.rotation θ) x)) y = ↑(-θ).expMapCircle * (o.kahler x) y
This theorem states that for a vector space `V` which is a normed add commutative group and has an inner product space over `ℝ` with finite dimension of 2, given an orientation `o` of `V`, and two vectors `x` and `y` in `V`, and an angle `θ` in `Real.Angle`, rotating the first vector `x` by `θ` scales their Kahler form by `cos (-θ) + sin (-θ) * I`. More specifically, the Kahler form of the rotation of `x` by `θ` and `y` is equal to the product of the complex number obtained by mapping `-θ` to the unit circle via the exponential function and the Kahler form of `x` and `y`.
More concisely: The Kahler form of the rotation of a 2-dimensional vector `x` by an angle `θ` in a complex inner product space `V` is equal to the product of the complex number `cos(-θ) + i * sin(-θ)` and the Kahler form of `x` and another vector `y`.
|
Orientation.oangle_rotation_right
theorem Orientation.oangle_rotation_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x ((o.rotation θ) y) = o.oangle x y + θ
This theorem states that for a given real inner product space `V` of finite rank 2 with an orientation `o`, and any two non-zero vectors `x` and `y` in this space, rotating the vector `y` by an angle `θ` (using the rotation operation defined by the orientation) results in the angle between the vector `x` and the rotated vector being equal to the original angle between the vectors `x` and `y` plus the rotation angle `θ`. This essentially encapsulates the intuitive geometric concept that rotating a vector in a plane by an angle essentially increases the angle between it and any other vector by the same amount.
More concisely: For any real inner product space of finite rank 2 with orientation, and two non-zero vectors x and y, the angle between x and the rotated vector y' obtained by rotating y by an angle θ using the orientation is equal to the sum of the original angle between x and y and the rotation angle θ.
|
Orientation.rotation_eq_self_iff_angle_eq_zero
theorem Orientation.rotation_eq_self_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (θ : Real.Angle), (o.rotation θ) x = x ↔ θ = 0
This theorem states that in a 2-dimensional real inner product space, a rotation of a nonzero vector equals the original vector if and only if the rotation angle is zero. It means that for any vector that is not the zero vector, the only rotational transformation that leaves it unchanged is the one with a rotation angle of zero. This is in essence a formalization of a fundamental property of rotational transformations in two-dimensional space.
More concisely: In a 2-dimensional real inner product space, a nonzero vector is invariant under rotation if and only if the rotation angle is zero.
|
Orientation.neg_rotation_neg_pi_div_two
theorem Orientation.neg_rotation_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
-(o.rotation ↑(-Real.pi / 2)) x = (o.rotation ↑(Real.pi / 2)) x
The theorem `Orientation.neg_rotation_neg_pi_div_two` states that for any normed additive commutative group `V` which is also an inner product space over real numbers `ℝ` and has a finite rank of 2, for any orientation `o` of `V` and for any vector `x` in `V`, the negation of the rotation of `x` by `-π / 2` degrees under the orientation `o` is equivalent to the rotation of `x` by `π / 2` degrees under the same orientation `o`. In simpler terms, it says that if we rotate a vector in a two-dimensional space first by `-π / 2` degrees and then negate the result, it's as if we rotate the vector by `π / 2` degrees.
More concisely: For any orientation `o` of a 2-dimensional inner product space `V` over the real numbers, and for any vector `x` in `V`, negating the result of rotating `x` by `-π / 2` degrees under `o` is equivalent to rotating `x` by `π / 2` degrees under `o`.
|
Orientation.rotation_trans
theorem Orientation.rotation_trans :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ₁ θ₂ : Real.Angle),
(o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)
The theorem `Orientation.rotation_trans` states that for a two-dimensional real vector space `V` with a given orientation `o`, the composition of two rotations by angles `θ₁` and `θ₂` respectively, is equivalent to a single rotation by the sum of the angles `θ₁` and `θ₂`. In other words, rotating `V` twice, first by `θ₁` and then by `θ₂`, is the same as rotating it once by the angle `(θ₂ + θ₁)`.
More concisely: For any two-dimensional real vector space `V` with orientation `o` and angles `θ₁` and `θ₂`, the composition of rotations by `θ₁` and `θ₂` is equivalent to a single rotation by the angle `(θ₁ + θ₂)`.
|
Orientation.rotation_pi
theorem Orientation.rotation_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)),
o.rotation ↑Real.pi = LinearIsometryEquiv.neg ℝ
The theorem `Orientation.rotation_pi` states that for any normed additive commutative group `V` that also forms an inner product space over the real numbers, and which has rank 2 (as a fact), the rotation by a value of π (pi) in any orientation of `V` is equivalent to the negation operation. Essentially, it means that rotation by π radians (180 degrees) in a 2-dimensional real vector space is the same as flipping the vector to its additive inverse, or "negation".
More concisely: In a rank 2 real inner product space, rotating a vector by π radians is equivalent to negating it.
|
Orientation.rotation_oangle_eq_iff_norm_eq
theorem Orientation.rotation_oangle_eq_iff_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.rotation (o.oangle x y)) x = y ↔ ‖x‖ = ‖y‖
The theorem `Orientation.rotation_oangle_eq_iff_norm_eq` states that for any two vectors `x` and `y` in a real inner product space `V` of finite dimension 2, rotating the vector `x` by the angle to the vector `y` (given by the orientation `o`) results in the vector `y` if and only if the norms of `x` and `y` are equal. This theorem connects the rotation of vectors, the angle between them and their norms in a two-dimensional real inner product space.
More concisely: In a 2-dimensional real inner product space, the vector obtained by rotating another vector about the origin through the angle between them is equal to the second vector if and only if both vectors have equal norms.
|
Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero
theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x y = θ ↔ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x
This theorem states that in a 2-dimensional inner product space `V` over the real numbers with a given orientation `o`, for any two nonzero vectors `x` and `y`, and any angle `θ` from the set of Real Angles, the orientation angle between `x` and `y` equals `θ` if and only if there exists a positive real number `r`, such that `y` is equal to `x` rotated by `θ` and then scaled by `r`. In other words, it characterizes the angle `θ` between two nonzero vectors in terms of rotation and scaling.
More concisely: In a 2-dimensional real inner product space with given orientation, the angle between two nonzero vectors is equal to the rotation and scaling relationship between them if and only if they are equal up to a positive scalar and a counterclockwise rotation.
|
Orientation.oangle_rotation
theorem Orientation.oangle_rotation :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y
This theorem, `Orientation.oangle_rotation`, states that for any real vector space `V` of rank 2, any orientation `o` of this space, any two vectors `x` and `y` in this space, and any real angle `θ`, rotating both vectors `x` and `y` by the same angle `θ` does not alter the orientation-angle between the two vectors. In other words, the orientation-angle between the rotated versions of `x` and `y` is equal to the orientation-angle between `x` and `y` before rotation. This is equivalent to the geometric intuition that the angle between two vectors is preserved under rotation.
More concisely: For any real vector space of rank 2 with orientation, two vectors, and a real angle, the orientation-angle between the rotated vectors is equal to the original orientation-angle.
|
Orientation.eq_rotation_self_iff_angle_eq_zero
theorem Orientation.eq_rotation_self_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (θ : Real.Angle), x = (o.rotation θ) x ↔ θ = 0
This theorem states that for any 2-dimensional real inner product space, given a non-zero vector and an orientation of the space, the vector equals its own rotation under the orientation if and only if the rotation's angle is zero. In other words, a non-zero vector is invariant under a specific rotation if and only if the rotation is a null rotation.
More concisely: A non-zero vector in a 2-dimensional real inner product space is invariant under a given orientation if and only if the orientation's angle is zero.
|
Orientation.kahler_rotation_left
theorem Orientation.kahler_rotation_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
(o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.expMapCircle * (o.kahler x) y
This theorem states that for a real vector space `V` which is a normed add commutative group and an inner product space, and has finite dimension equal to `2`, given an orientation `o` of `V`, two vectors `x` and `y` in `V`, and an angle `θ`, if the first vector `x` is rotated by angle `θ` according to the orientation `o`, then the Kahler form of the rotated vector with respect to `y` is scaled by `cos θ - sin θ * I`, where `I` is the imaginary unit. Here, `cos θ - sin θ * I` is represented as the image of `θ` under the exponential map from ℝ to the unit circle in ℂ, expressed in the star ring end of ℂ.
More concisely: For a 2-dimensional real inner product space `V` with orientation `o`, given vectors `x`, `y` in `V` and angle `θ`, the Kahler form of the rotated vector `x'` with respect to `y` is `(cos θ - sin θ * I) * (x' · y)`, where `x'` is the rotation of `x` by `θ` according to `o` and `I` is the imaginary unit.
|
Orientation.oangle_rotation_self_right
theorem Orientation.oangle_rotation_self_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (θ : Real.Angle), o.oangle x ((o.rotation θ) x) = θ
This theorem states that for any two-dimensional real inner product space `V` with a given orientation `o`, for any non-zero vector `x` in `V`, and any real angle `θ`, the angle from `x` to the vector obtained by rotating `x` by `θ` according to the orientation `o` is `θ`. In simpler terms, it asserts that the angle between a vector and its rotation by a given angle is indeed that angle itself, considering a specific orientation of the space.
More concisely: For any two-dimensional real inner product space `V` with orientation `o`, the angle between a vector `x` and its rotation `x'` around `o` by angle `θ` is equal to `θ`.
|
Orientation.inner_smul_rotation_pi_div_two_left
theorem Orientation.inner_smul_rotation_pi_div_two_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ),
⟪r • (o.rotation ↑(Real.pi / 2)) x, x⟫_ℝ = 0
This theorem states that for a 2-dimensional real inner product space `V`, and any orientation `o` of `V` and vector `x` in `V`, the inner product of the vector `x` and the vector obtained by rotating `x` by `π / 2` radians and then scaling by a factor `r` is zero. In other words, it asserts that the vector `x` and the π/2-rotated and scaled version of `x` are orthogonal.
More concisely: For any 2-dimensional real inner product space `V`, orientation `o`, vector `x`, and scalar `r`, the inner product of `x` and the `π/2`-rotated and scaled version of `x` (with respect to `o`) is zero. That is, `⟨x, r * ρ(x)⟩ = 0`, where `ρ(x)` denotes the vector obtained by rotating `x` by `π/2` radians around the origin.
|
Orientation.rotation_rotation
theorem Orientation.rotation_rotation :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ₁ θ₂ : Real.Angle) (x : V),
(o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x
This theorem states that for a given vector space `V`, which is a normed add commutative group and an inner product space over the real numbers `ℝ`, and for which the dimension of `V` over `ℝ` is 2, if we rotate a vector `x` in `V` first by an angle `θ₂` and then by an angle `θ₁`, it is equivalent to rotating the vector `x` directly by the sum of the angles `θ₁` and `θ₂`. This orientation operation is applied using a given orientation 'o' of the vector space `V`.
More concisely: For a 2-dimensional real inner product space `V` with given orientation `o`, rotating a vector `x` by angles `θ₁` then `θ₂` is equivalent to rotating it once by the sum `θ₁ + θ₂` around `o`.
|
Orientation.oangle_rotation_oangle_right
theorem Orientation.oangle_rotation_oangle_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle y ((o.rotation (o.oangle x y)) x) = 0
The theorem `Orientation.oangle_rotation_oangle_right` takes as input a 2-dimensional real vector space `V` with a given orientation `o`, and two vectors `x` and `y` from this space. It states that if you rotate the first vector `x` by the angle between `x` and `y` under orientation `o` and then compute the oriented angle between the resulting vector and `y`, you get zero. In other words, after performing the rotation, `y` and the rotated `x` are aligned, which means they have an oriented angle of zero between them.
More concisely: Given a 2-dimensional real vector space with orientation, the oriented angle between a vector and its rotation by the angle between them and another vector is zero.
|
Orientation.det_rotation
theorem Orientation.det_rotation :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle),
LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
The theorem `Orientation.det_rotation` states that for a normed additive commutative group `V` which is also an inner product space over the reals, with the condition that the rank of `V` is 2, for any orientation `o` of `V` and for any real angle `θ`, the determinant of the rotation defined by `θ` as a linear map, when evaluated, is equal to `1`. This means that rotating a two-dimensional vector space doesn't change the area (since the determinant can be thought of as a scaling factor for area in this context).
More concisely: For any orientation `o` of a 2-dimensional real inner product space `V`, and real angle `θ`, the determinant of the resulting rotation matrix is equal to 1.
|
Orientation.oangle_rotation_left
theorem Orientation.oangle_rotation_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle ((o.rotation θ) x) y = o.oangle x y - θ
This theorem states that if you have a 2-dimensional real inner product space `V` and two non-zero vectors `x` and `y` in this space, as well as an orientation `o` of the space and an angle `θ`, then the angle between the vector obtained by rotating `x` by `θ` and `y` (according to the orientation `o`) is equal to the original angle between `x` and `y` minus `θ`. Essentially, this theorem formalizes the intuition that rotating a vector in a plane by a certain angle decreases the angle between it and another fixed vector by the same amount.
More concisely: Given a 2-dimensional real inner product space `V`, vectors `x ≠ 0` and `y ≠ 0`, orientation `o`, and angle `θ`, the angle between `x` rotated by `θ` and `y` according to `o` equals the original angle between `x` and `y` minus `θ`.
|
Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two
theorem Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
⟪x, y⟫_ℝ = 0 ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(Real.pi / 2)) x = y
This theorem establishes a condition for the inner product between two vectors in a real inner product space of dimension 2 to be zero. Specifically, the inner product of two vectors `x` and `y` is zero if and only if one of the two conditions is met: either the vector `x` is the zero vector, or the vector `y` is obtained by rotating the vector `x` by an angle of `π / 2` (equivalent to 90 degrees) and scaling it by a certain real number `r`. This rotation is defined according to an orientation `o` of the vector space.
More concisely: In a real inner product space of dimension 2, the inner product of vectors `x` and `y` is zero if and only if `x` is the zero vector or `y` is obtained by rotating `x` counterclockwise by 90 degrees and scaling by a real number `r` according to the orientation `o` of the vector space.
|
Orientation.eq_rotation_self_iff
theorem Orientation.eq_rotation_self_iff :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle),
x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0
This theorem states that for a vector `x` in a real inner product space `V` of finite dimension 2, with a given orientation `o`, and for a given real angle `θ`, the vector `x` equals its own rotation by angle `θ` if and only if the vector `x` is equal to zero or the angle `θ` is equal to zero. Essentially, it says that the only way for a vector's rotation to result in the original vector (in a 2-dimensional space) is if the vector is the zero vector or the rotation angle is zero.
More concisely: In a 2-dimensional real inner product space with a given orientation, a non-zero vector `x` equals its rotation by angle `θ` if and only if `θ` is zero.
|
Orientation.rotation_symm
theorem Orientation.rotation_symm :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle),
(o.rotation θ).symm = o.rotation (-θ)
This theorem states that for any 2-dimensional real vector space `V`, for any given orientation `o` of the vector space, and for any real angle `θ`, the inverse of `rotation` by angle `θ` is equivalent to the `rotation` by the negation of the angle `θ`. In other words, rotating by `θ` and then rotating by `-θ` is equivalent to doing nothing (which is the very definition of the inverse operation in the concept of rotation).
More concisely: For any 2-dimensional real vector space `V` and orientation `o`, the inverse of the rotation by angle `θ` is equivalent to the rotation by angle `-θ`.
|
Orientation.linearEquiv_det_rotation
theorem Orientation.linearEquiv_det_rotation :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle),
LinearEquiv.det (o.rotation θ).toLinearEquiv = 1
The theorem `Orientation.linearEquiv_det_rotation` states that for any real vector space `V` that is a normed add commutative group and an inner product space, and has a finite dimension equal to two, along with any orientation `o` of `V` and any real angle `θ`, the determinant of the linear equivalence transformation that corresponds to a rotation by `θ` in the orientation `o` is always equal to `1`. This means that rotating the space doesn't change its oriented volume, as expected.
More concisely: For any two-dimensional real vector space endowed with an inner product and orientation, the determinant of the linear transformation representing a rotation is equal to 1.
|
Orientation.inner_rotation_pi_div_two_right
theorem Orientation.inner_rotation_pi_div_two_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
⟪x, (o.rotation ↑(Real.pi / 2)) x⟫_ℝ = 0
This theorem states that for a vector space `V` over the real numbers `ℝ` with a normed additive commutative group structure and an inner product space structure, and whose finite rank (dimension) equals two, given an orientation `o` of `V` and a vector `x` in `V`, the inner product of the vector `x` and its `π/2` rotation under the orientation `o` is zero. This is similar to stating that in a two-dimensional space, a vector and its 90 degrees rotated version are orthogonal to each other.
More concisely: In a two-dimensional real vector space equipped with both a norm and an inner product, for any orientation and vector, the inner product of the vector with its counterclockwise 90-degree rotation under the given orientation is zero.
|
Orientation.exists_linearIsometryEquiv_eq_of_det_pos
theorem Orientation.exists_linearIsometryEquiv_eq_of_det_pos :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {f : V ≃ₗᵢ[ℝ] V},
0 < LinearMap.det ↑f.toLinearEquiv → ∃ θ, f = o.rotation θ
The theorem `Orientation.exists_linearIsometryEquiv_eq_of_det_pos` states that for any vector space `V` that is a normed add commutative group and an inner-product space over the real numbers ℝ, and that has a finite rank of 2, along with any orientation `o` of `V` and a linear isometric equivalence `f` in `V`, if the determinant of the linear map equivalent to `f` is positive, then there exists a real number `θ` such that `f` is the same as the rotation of the orientation `o` by the angle `θ`.
More concisely: Given a finite-dimensional real inner-product space `V` with orientation `o`, if there exists a linear isometric equivalence `f` with positive determinant, then there exists an angle `θ` such that `f` is equivalent to the rotation of `o` by `θ`.
|
Orientation.inner_rotation_pi_div_two_right_smul
theorem Orientation.inner_rotation_pi_div_two_right_smul :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ),
⟪r • x, (o.rotation ↑(Real.pi / 2)) x⟫_ℝ = 0
This theorem states that the inner product of a vector scaled by a real number and a π/2 rotation of the original vector, in a two-dimensional real inner product space, is zero. It indicates that in such a space, the π/2 rotation of a vector is orthogonal to the original vector, and this property holds even if the original vector is scaled by any real number.
More concisely: In a two-dimensional real inner product space, the inner product of a vector and its π/2 rotation, scaled by any real number, is zero.
|
Orientation.rotation_pi_div_two
theorem Orientation.rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)),
o.rotation ↑(Real.pi / 2) = o.rightAngleRotation
This theorem states that for any 2-dimensional normed add-commutative group `V` with an inner product space over the real numbers, rotation by π/2 radians (90 degrees) is equivalent to the "right-angle-rotation" map `J`. This is true for any orientation `o` of `V`. Essentially, it is stating that in any 2D space, rotating by 90 degrees gives the same result as applying the right-angle rotation operator.
More concisely: For any 2-dimensional normed add-commutative group `V` with an inner product space over the real numbers and orientation `o`, rotation by π/2 radians is equivalent to the right-angle-rotation map `J`, that is, `(rot π/2) x = J (o x)` for all `x` in `V`.
|
Orientation.kahler_rotation_right
theorem Orientation.kahler_rotation_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
(o.kahler x) ((o.rotation θ) y) = ↑θ.expMapCircle * (o.kahler x) y
This theorem states that for a real inner product space `V` of finite dimension 2, given an orientation `o` of this space, and any two vectors `x` and `y` in `V`, along with an angle `θ` from the real numbers, rotating the second vector `y` by the angle `θ` scales their Kähler form by `cos θ + sin θ * I`. Here, the Kähler form is a bilinear form associated with a complex structure on a real vector space. Rotation is performed using the `o.rotation θ` operation on `y`, and the angle `θ` is mapped to the unit circle in the complex plane using the exponential map `expMapCircle`. The resulting complex number multiplies the original value of the Kähler form of `x` and `y`.
More concisely: For any real inner product space of dimension 2 with orientation, the Kähler form of vectors `x` and `y` is scaled by `cos θ + sin θ * I` when `y` is rotated by angle `θ` using the given orientation, where I is the imaginary unit.
|
Orientation.rotation_neg_orientation_eq_neg
theorem Orientation.rotation_neg_orientation_eq_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle),
(-o).rotation θ = o.rotation (-θ)
This theorem, `Orientation.rotation_neg_orientation_eq_neg`, states that for any real vector space `V` with `NormedAddCommGroup` and `InnerProductSpace` structures, and a specific finite rank of 2, given any orientation `o` on `V` and any real angle `θ`, the rotation of angle `θ` for the negated orientation `-o` is equal to the rotation of the negated angle `-θ` for the original orientation `o`. In simpler terms, negating the orientation of a 2-dimensional space is equivalent to negating the angle in rotation for that space.
More concisely: For any orientation `o` on a 2-dimensional real vector space `V` with `NormedAddCommGroup` and `InnerProductSpace` structures, and any real angle `θ`, the rotation of `-o` by `-θ` is equal to the rotation of `o` by `θ`.
|
Orientation.inner_smul_rotation_pi_div_two_smul_right
theorem Orientation.inner_smul_rotation_pi_div_two_smul_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ r₂ : ℝ),
⟪r₂ • x, r₁ • (o.rotation ↑(Real.pi / 2)) x⟫_ℝ = 0
This theorem states that for a vector space `V` which is also a normed add commutative group and an inner product space over the real numbers `ℝ`, given that the rank of this vector space `V` is 2, then for any orientation `o` of `V`, any vector `x` in `V`, and any two real numbers `r₁` and `r₂`, the inner product in `ℝ` between `r₂` times `x` and `r₁` times the `π / 2` rotation of `x` according to the orientation `o` is zero. In mathematical terms, it states that for certain 2-dimensional spaces, the inner product of a vector and a rotated version of the vector (rotated by π/2 radians) is zero when both vectors are scaled by any two real numbers.
More concisely: For any 2-dimensional real vector space endowed with both a norm and an inner product, and for any orientation, vectors `x` and scalars `r₁, r₂`, the inner product of `r₁` times the `π / 2` rotation of `x` around the orientation and `r₂` times `x` is zero.
|
Orientation.rotation_zero
theorem Orientation.rotation_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)),
o.rotation 0 = LinearIsometryEquiv.refl ℝ V
This theorem, `Orientation.rotation_zero`, states that for any 2-dimensional real vector space `V` with a given orientation `o`, rotation by `0` is the identity transformation. In other words, if you take an element of the vector space and rotate it by `0` degrees, it stays the same, which is equivalent to applying the identity transformation. This is true regardless of the specific orientation of the vector space.
More concisely: For any 2-dimensional real vector space and orientation, rotation by 0 degrees is the identity transformation.
|
Orientation.inner_smul_rotation_pi_div_two_right
theorem Orientation.inner_smul_rotation_pi_div_two_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ),
⟪x, r • (o.rotation ↑(Real.pi / 2)) x⟫_ℝ = 0
This theorem states that for a real-valued inner product space V of finite dimension 2, given any orientation `o` of `V`, and any vector `x` in `V` and a real number `r`, the inner product of `x` and the vector obtained by rotating `x` by an angle of `π/2` radians and then scaling by `r` is zero. In other words, the `π/2` rotation leads to a vector that is orthogonal to the original vector `x`, and scaling the rotated vector by `r` does not change this orthogonality.
More concisely: For any real-valued inner product space V of finite dimension 2, the inner product of a vector x and the rotation of x by π/2 radians and scaled by r is zero, i.e., x is orthogonal to the rotated and scaled vector.
|
Orientation.oangle_rotation_self_left
theorem Orientation.oangle_rotation_self_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (θ : Real.Angle), o.oangle ((o.rotation θ) x) x = -θ
This theorem states that for any 2-dimensional real vector space `V` with a given orientation `o`, and for any non-zero vector `x` in `V`, the angle between `x` and its image under the rotation by an angle `θ` is equal to `-θ`. In other words, if you rotate a vector by an angle `θ`, the angle from the rotated vector back to the original vector is `-θ`. This theorem captures a fundamental property of rotations in 2-dimensional real vector spaces.
More concisely: The angle between a vector and its rotation is equal but opposite to the angle of rotation.
|
Orientation.oangle_rotation_oangle_left
theorem Orientation.oangle_rotation_oangle_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle ((o.rotation (o.oangle x y)) x) y = 0
The theorem `Orientation.oangle_rotation_oangle_left` states that for a two-dimensional real inner product space `V`, given an orientation `o` of this space and two vectors `x` and `y` from this space, if you rotate the vector `x` by the angle between `x` and `y` according to the orientation `o`, then the angle between the rotated vector and `y` will be `0`. In other words, applying the rotation operation to the first vector by the angle between these two vectors aligns the rotated vector with the second vector. This theorem essentially describes how the rotation operation affects the orientation-based angle (`oangle`) between two vectors in a two-dimensional space.
More concisely: In a 2-dimensional real inner product space, given an orientation and two vectors, the angle between the rotated first vector by the angle between them and the second vector according to the orientation is zero.
|
Orientation.rotation_map_complex
theorem Orientation.rotation_map_complex :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle)
(f : V ≃ₗᵢ[ℝ] ℂ),
(Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
∀ (x : V), f ((o.rotation θ) x) = ↑θ.expMapCircle * f x
This theorem states that in an oriented real inner product space of dimension 2, the action of rotation can be expressed in terms of a complex-number representation of the space. Specifically, given an orientation `o` of the space, an angle `θ`, and a linear isometry `f` from the space to the complex numbers that maps the orientation `o` to the standard complex orientation, the image under `f` of the rotation of a vector `x` by angle `θ` is equal to the product of the image under the exponential map of `θ` and the image under `f` of `x`. This effectively translates the geometric concept of rotation in the plane to the algebraic operation of multiplication by a complex number of modulus 1.
More concisely: In a 2-dimensional oriented real inner product space, rotation by angle θ of a vector x, with respect to orientation o, is equivalent to multiplying the complex representation of x, under a linear isometry f mapping o to the standard complex orientation, by the complex number e^(iθ).
|
Orientation.neg_rotation_pi_div_two
theorem Orientation.neg_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
-(o.rotation ↑(Real.pi / 2)) x = (o.rotation ↑(-Real.pi / 2)) x
The theorem `Orientation.neg_rotation_pi_div_two` states that for any real vector space `V` of dimension 2, and for any orientation `o` of this space, if you rotate any vector `x` from this space by π/2 radians in the orientation `o` and then negate the result, it is equivalent to rotating the original vector `x` by -π/2 radians in the orientation `o`. It essentially describes how negation of a rotation in a 2-dimensional vector space corresponds to rotation in the opposite direction.
More concisely: For any 2-dimensional real vector space orientation `o`, negating the result of rotating a vector `x` by π/2 radians in `o` is equivalent to rotating `x` by -π/2 radians in `o`.
|