geometry.euclidean.angle.oriented.rotation

source

noncomputable def orientation.rotation_aux {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

V →ₗᵢ[ℝ ] V

Auxiliary construction to build a rotation by the oriented angle θ.

Equations

o.rotation_aux θ = (θ.cos • linear_map.id + θ.sin • ↑(o.right_angle_rotation.to_linear_equiv)).isometry_of_inner _

source

@[simp]

theorem orientation.rotation_aux_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (x : V) :

⇑(o.rotation_aux θ) x = θ.cos • x + θ.sin • ⇑(o.right_angle_rotation) x

source

@[irreducible]

noncomputable def orientation.rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

V ≃ₗᵢ[ℝ ] V

A rotation by the oriented angle θ.

Equations

o.rotation θ = linear_isometry_equiv.of_linear_isometry (o.rotation_aux θ) (θ.cos • linear_map.id - θ.sin • ↑(o.right_angle_rotation.to_linear_equiv)) _ _

source

theorem orientation.rotation_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (x : V) :

⇑(o.rotation θ) x = θ.cos • x + θ.sin • ⇑(o.right_angle_rotation) x

source

theorem orientation.rotation_symm_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (x : V) :

⇑((o.rotation θ).symm) x = θ.cos • x - θ.sin • ⇑(o.right_angle_rotation) x

source

theorem orientation.rotation_eq_matrix_to_lin {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) {x : V} (hx : x ≠ 0) :

(o.rotation θ).to_linear_equiv.to_linear_map = ⇑(matrix.to_lin (o.basis_right_angle_rotation x hx) (o.basis_right_angle_rotation x hx)) (⇑matrix.of ![![θ.cos, -θ.sin], ![θ.sin, θ.cos]])

source

@[simp]

theorem orientation.det_rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

⇑linear_map.det (o.rotation θ).to_linear_equiv.to_linear_map = 1

The determinant of rotation (as a linear map) is equal to 1.

source

@[simp]

theorem orientation.linear_equiv_det_rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

⇑linear_equiv.det (o.rotation θ).to_linear_equiv = 1

The determinant of rotation (as a linear equiv) is equal to 1.

source

@[simp]

theorem orientation.rotation_symm {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

(o.rotation θ).symm = o.rotation (-θ)

The inverse of rotation is rotation by the negation of the angle.

source

@[simp]

theorem orientation.rotation_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) :

o.rotation 0 = linear_isometry_equiv.refl ℝ V

Rotation by 0 is the identity.

source

@[simp]

theorem orientation.rotation_pi {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) :

o.rotation ↑real.pi = linear_isometry_equiv.neg ℝ

Rotation by π is negation.

source

theorem orientation.rotation_pi_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) :

⇑(o.rotation ↑real.pi) x = -x

Rotation by π is negation.

source

theorem orientation.rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) :

o.rotation ↑(real.pi / 2) = o.right_angle_rotation

Rotation by π / 2 is the "right-angle-rotation" map J.

source

@[simp]

theorem orientation.rotation_rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ₁ θ₂ : real.angle) (x : V) :

⇑(o.rotation θ₁) (⇑(o.rotation θ₂) x) = ⇑(o.rotation (θ₁ + θ₂)) x

Rotating twice is equivalent to rotating by the sum of the angles.

source

@[simp]

theorem orientation.rotation_trans {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ₁ θ₂ : real.angle) :

(o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)

Rotating twice is equivalent to rotating by the sum of the angles.

source

@[simp]

theorem orientation.kahler_rotation_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) (θ : real.angle) :

⇑(⇑(o.kahler) (⇑(o.rotation θ) x)) y = ⇑(star_ring_end ℂ) ↑(θ.exp_map_circle) * ⇑(⇑(o.kahler) x) y

Rotating the first of two vectors by θ scales their Kahler form by cos θ - sin θ * I.

source

theorem orientation.neg_rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (x : V) :

-⇑(o.rotation θ) x = ⇑(o.rotation (↑real.pi + θ)) x

Negating a rotation is equivalent to rotation by π plus the angle.

source

@[simp]

theorem orientation.neg_rotation_neg_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) :

-⇑(o.rotation ↑(-real.pi / 2)) x = ⇑(o.rotation ↑(real.pi / 2)) x

Negating a rotation by -π / 2 is equivalent to rotation by π / 2.

source

theorem orientation.neg_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) :

-⇑(o.rotation ↑(real.pi / 2)) x = ⇑(o.rotation ↑(-real.pi / 2)) x

Negating a rotation by π / 2 is equivalent to rotation by -π / 2.

source

theorem orientation.kahler_rotation_left' {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) (θ : real.angle) :

⇑(⇑(o.kahler) (⇑(o.rotation θ) x)) y = ↑((-θ).exp_map_circle) * ⇑(⇑(o.kahler) x) y

Rotating the first of two vectors by θ scales their Kahler form by cos (-θ) + sin (-θ) * I.

source

@[simp]

theorem orientation.kahler_rotation_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) (θ : real.angle) :

⇑(⇑(o.kahler) x) (⇑(o.rotation θ) y) = ↑(θ.exp_map_circle) * ⇑(⇑(o.kahler) x) y

Rotating the second of two vectors by θ scales their Kahler form by cos θ + sin θ * I.

source

@[simp]

theorem orientation.oangle_rotation_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : real.angle) :

o.oangle (⇑(o.rotation θ) x) y = o.oangle x y - θ

Rotating the first vector by θ subtracts θ from the angle between two vectors.

source

@[simp]

theorem orientation.oangle_rotation_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : real.angle) :

o.oangle x (⇑(o.rotation θ) y) = o.oangle x y + θ

Rotating the second vector by θ adds θ to the angle between two vectors.

source

@[simp]

theorem orientation.oangle_rotation_self_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x : V} (hx : x ≠ 0) (θ : real.angle) :

o.oangle (⇑(o.rotation θ) x) x = -θ

The rotation of a vector by θ has an angle of -θ from that vector.

source

@[simp]

theorem orientation.oangle_rotation_self_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x : V} (hx : x ≠ 0) (θ : real.angle) :

o.oangle x (⇑(o.rotation θ) x) = θ

A vector has an angle of θ from the rotation of that vector by θ.

source

@[simp]

theorem orientation.oangle_rotation_oangle_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) :

o.oangle (⇑(o.rotation (o.oangle x y)) x) y = 0

Rotating the first vector by the angle between the two vectors results an an angle of 0.

source

@[simp]

theorem orientation.oangle_rotation_oangle_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) :

o.oangle y (⇑(o.rotation (o.oangle x y)) x) = 0

Rotating the first vector by the angle between the two vectors and swapping the vectors results an an angle of 0.

source

@[simp]

theorem orientation.oangle_rotation {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) (θ : real.angle) :

o.oangle (⇑(o.rotation θ) x) (⇑(o.rotation θ) y) = o.oangle x y

Rotating both vectors by the same angle does not change the angle between those vectors.

source

@[simp]

theorem orientation.rotation_eq_self_iff_angle_eq_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x : V} (hx : x ≠ 0) (θ : real.angle) :

⇑(o.rotation θ) x = x ↔ θ = 0

A rotation of a nonzero vector equals that vector if and only if the angle is zero.

source

@[simp]

theorem orientation.eq_rotation_self_iff_angle_eq_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x : V} (hx : x ≠ 0) (θ : real.angle) :

x = ⇑(o.rotation θ) x ↔ θ = 0

A nonzero vector equals a rotation of that vector if and only if the angle is zero.

source

theorem orientation.rotation_eq_self_iff {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (θ : real.angle) :

⇑(o.rotation θ) x = x ↔ x = 0 ∨ θ = 0

A rotation of a vector equals that vector if and only if the vector or the angle is zero.

source

theorem orientation.eq_rotation_self_iff {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (θ : real.angle) :

x = ⇑(o.rotation θ) x ↔ x = 0 ∨ θ = 0

A vector equals a rotation of that vector if and only if the vector or the angle is zero.

source

@[simp]

theorem orientation.rotation_oangle_eq_iff_norm_eq {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x y : V) :

⇑(o.rotation (o.oangle x y)) x = y ↔ ‖x‖ = ‖y‖

Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.

source

theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : real.angle) :

o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • ⇑(o.rotation θ) x

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.

source

theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : real.angle) :

o.oangle x y = θ ↔ ∃ (r : ℝ), 0 < r ∧ y = r • ⇑(o.rotation θ) x

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.

source

theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim 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 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.

source

theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim 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 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.

source

theorem orientation.exists_linear_isometry_equiv_eq_of_det_pos {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {f : V ≃ₗᵢ[ℝ ] V} (hd : 0 < ⇑linear_map.det ↑(f.to_linear_equiv)) :

∃ (θ : real.angle), f = o.rotation θ

Any linear isometric equivalence in V with positive determinant is rotation.

source

theorem orientation.rotation_map {V : Type u_1} {V' : Type u_2} [normed_add_comm_group V] [normed_add_comm_group V'] [inner_product_space ℝ V] [inner_product_space ℝ V'] [fact (fdim V = 2)] [fact (fdim V' = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (f : V ≃ₗᵢ[ℝ ] V') (x : V') :

⇑((⇑(orientation.map (fin 2) f.to_linear_equiv) o).rotation θ) x = ⇑f (⇑(o.rotation θ) (⇑(f.symm) x))

source

@[protected, simp]

theorem complex.rotation (θ : real.angle) (z : ℂ) :

⇑(complex.orientation.rotation θ) z = ↑(θ.exp_map_circle) * z

source

theorem orientation.rotation_map_complex {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) (f : V ≃ₗᵢ[ℝ ] ℂ) (hf : ⇑(orientation.map (fin 2) f.to_linear_equiv) o = complex.orientation) (x : V) :

⇑f (⇑(o.rotation θ) x) = ↑(θ.exp_map_circle) * ⇑f x

Rotation in an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

source

theorem orientation.rotation_neg_orientation_eq_neg {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (θ : real.angle) :

(-o).rotation θ = o.rotation (-θ)

Negating the orientation negates the angle in rotation.

source

@[simp]

theorem orientation.inner_rotation_pi_div_two_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) :

has_inner.inner (⇑(o.rotation ↑(real.pi / 2)) x) x = 0

The inner product between a π / 2 rotation of a vector and that vector is zero.

source

@[simp]

theorem orientation.inner_rotation_pi_div_two_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) :

has_inner.inner x (⇑(o.rotation ↑(real.pi / 2)) x) = 0

The inner product between a vector and a π / 2 rotation of that vector is zero.

source

@[simp]

theorem orientation.inner_smul_rotation_pi_div_two_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r : ℝ) :

has_inner.inner (r • ⇑(o.rotation ↑(real.pi / 2)) x) x = 0

The inner product between a multiple of a π / 2 rotation of a vector and that vector is zero.

source

@[simp]

theorem orientation.inner_smul_rotation_pi_div_two_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r : ℝ) :

has_inner.inner x (r • ⇑(o.rotation ↑(real.pi / 2)) x) = 0

The inner product between a vector and a multiple of a π / 2 rotation of that vector is zero.

source

@[simp]

theorem orientation.inner_rotation_pi_div_two_left_smul {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r : ℝ) :

has_inner.inner (⇑(o.rotation ↑(real.pi / 2)) x) (r • x) = 0

The inner product between a π / 2 rotation of a vector and a multiple of that vector is zero.

source

@[simp]

theorem orientation.inner_rotation_pi_div_two_right_smul {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r : ℝ) :

has_inner.inner (r • x) (⇑(o.rotation ↑(real.pi / 2)) x) = 0

The inner product between a multiple of a vector and a π / 2 rotation of that vector is zero.

source

@[simp]

theorem orientation.inner_smul_rotation_pi_div_two_smul_left {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r₁ r₂ : ℝ) :

has_inner.inner (r₁ • ⇑(o.rotation ↑(real.pi / 2)) x) (r₂ • x) = 0

The inner product between a multiple of a π / 2 rotation of a vector and a multiple of that vector is zero.

source

@[simp]

theorem orientation.inner_smul_rotation_pi_div_two_smul_right {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) (x : V) (r₁ r₂ : ℝ) :

has_inner.inner (r₂ • x) (r₁ • ⇑(o.rotation ↑(real.pi / 2)) x) = 0

The inner product between a multiple of a vector and a multiple of a π / 2 rotation of that vector is zero.

source

theorem orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim V = 2)] (o : orientation ℝ V (fin 2)) {x y : V} :

has_inner.inner x y = 0 ↔ x = 0 ∨ ∃ (r : ℝ), r • ⇑(o.rotation ↑(real.pi / 2)) x = y

The inner product between two vectors is zero if and only if the first vector is zero or the second is a multiple of a π / 2 rotation of that vector.

mathlib3 documentation

Rotations by oriented angles. #

Main definitions #