Documentation

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Rotations by oriented angles. #

This file defines rotations by oriented angles in real inner product spaces.

Main definitions #

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

Equations
  • o.rotationAux θ = (θ.cos LinearMap.id + θ.sin o.rightAngleRotation.toLinearEquiv).isometryOfInner
Instances For
    @[simp]
    theorem Orientation.rotationAux_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) (x : V) :
    (o.rotationAux θ) x = θ.cos x + θ.sin o.rightAngleRotation x

    A rotation by the oriented angle θ.

    Equations
    Instances For
      theorem Orientation.rotation_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) (x : V) :
      (o.rotation θ) x = θ.cos x + θ.sin o.rightAngleRotation x
      theorem Orientation.rotation_symm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) (x : V) :
      (o.rotation θ).symm x = θ.cos x - θ.sin o.rightAngleRotation x
      theorem Orientation.rotation_eq_matrix_toLin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) {x : V} (hx : x 0) :
      (o.rotation θ).toLinearEquiv = (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]
      @[simp]
      theorem Orientation.det_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) :
      LinearMap.det (o.rotation θ).toLinearEquiv = 1

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

      @[simp]
      theorem Orientation.linearEquiv_det_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) :
      LinearEquiv.det (o.rotation θ).toLinearEquiv = 1

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

      @[simp]
      theorem Orientation.rotation_symm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      @[simp]

      Rotation by 0 is the identity.

      @[simp]

      Rotation by π is negation.

      theorem Orientation.rotation_pi_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) :
      (o.rotation Real.pi) x = -x

      Rotation by π is negation.

      theorem Orientation.rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) :
      o.rotation (Real.pi / 2) = o.rightAngleRotation

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

      @[simp]
      theorem Orientation.rotation_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ₁ : Real.Angle) (θ₂ : Real.Angle) (x : V) :
      (o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x

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

      @[simp]
      theorem Orientation.rotation_trans {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
      (o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)

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

      @[simp]
      theorem Orientation.kahler_rotation_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) :
      (o.kahler ((o.rotation θ) x)) y = (starRingEnd ) θ.expMapCircle * (o.kahler x) y

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

      theorem Orientation.neg_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      @[simp]
      theorem Orientation.neg_rotation_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      theorem Orientation.neg_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      theorem Orientation.kahler_rotation_left' {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) :
      (o.kahler ((o.rotation θ) x)) y = (-θ).expMapCircle * (o.kahler x) y

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

      @[simp]
      theorem Orientation.kahler_rotation_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) :
      (o.kahler x) ((o.rotation θ) y) = θ.expMapCircle * (o.kahler x) y

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

      @[simp]
      theorem Orientation.oangle_rotation_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      @[simp]
      theorem Orientation.oangle_rotation_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      @[simp]
      theorem Orientation.oangle_rotation_self_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      @[simp]
      theorem Orientation.oangle_rotation_self_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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 θ.

      @[simp]
      theorem Orientation.oangle_rotation_oangle_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (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 in an angle of 0.

      @[simp]
      theorem Orientation.oangle_rotation_oangle_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (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 in an angle of 0.

      @[simp]
      theorem Orientation.oangle_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (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.

      @[simp]
      theorem Orientation.rotation_eq_self_iff_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      @[simp]
      theorem Orientation.eq_rotation_self_iff_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      theorem Orientation.rotation_eq_self_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      theorem Orientation.eq_rotation_self_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank 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.

      @[simp]
      theorem Orientation.rotation_oangle_eq_iff_norm_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (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.

      theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {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.

      theorem Orientation.exists_linearIsometryEquiv_eq_of_det_pos {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {f : V ≃ₗᵢ[] V} (hd : 0 < LinearMap.det f.toLinearEquiv) :
      ∃ (θ : Real.Angle), f = o.rotation θ

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

      theorem Orientation.rotation_map {V : Type u_1} {V' : Type u_2} [NormedAddCommGroup V] [NormedAddCommGroup V'] [InnerProductSpace V] [InnerProductSpace V'] [Fact (FiniteDimensional.finrank V = 2)] [Fact (FiniteDimensional.finrank V' = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[] V') (x : V') :
      (((Orientation.map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))
      @[simp]
      theorem Complex.rotation (θ : Real.Angle) (z : ) :
      (Complex.orientation.rotation θ) z = θ.expMapCircle * z
      theorem Orientation.rotation_map_complex {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[] ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : V) :
      f ((o.rotation θ) x) = θ.expMapCircle * 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.

      theorem Orientation.rotation_neg_orientation_eq_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (θ : Real.Angle) :
      (-o).rotation θ = o.rotation (-θ)

      Negating the orientation negates the angle in rotation.

      @[simp]
      theorem Orientation.inner_rotation_pi_div_two_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) :
      (o.rotation (Real.pi / 2)) x, x⟫_ = 0

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

      @[simp]
      theorem Orientation.inner_rotation_pi_div_two_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) :
      x, (o.rotation (Real.pi / 2)) x⟫_ = 0

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

      @[simp]
      theorem Orientation.inner_smul_rotation_pi_div_two_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r : ) :
      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.

      @[simp]
      theorem Orientation.inner_smul_rotation_pi_div_two_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r : ) :
      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.

      @[simp]
      theorem Orientation.inner_rotation_pi_div_two_left_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r : ) :
      (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.

      @[simp]
      theorem Orientation.inner_rotation_pi_div_two_right_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r : ) :
      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.

      @[simp]
      theorem Orientation.inner_smul_rotation_pi_div_two_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r₁ : ) (r₂ : ) :
      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.

      @[simp]
      theorem Orientation.inner_smul_rotation_pi_div_two_smul_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) (x : V) (r₁ : ) (r₂ : ) :
      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.

      theorem Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [Fact (FiniteDimensional.finrank V = 2)] (o : Orientation V (Fin 2)) {x : V} {y : V} :
      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.