Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

The type of angles #

In this file we define Real.Angle to be the quotient group ℝ/2πℤ and prove a few simple lemmas about trigonometric functions and angles.

The type of angles

Equations
    Instances For

      The canonical map from to the quotient Angle.

      Equations
        Instances For

          Coercion ℝ → Angle as an additive homomorphism.

          Equations
            Instances For
              theorem Real.Angle.induction_on {p : AngleProp} (θ : Angle) (h : ∀ (x : ), p x) :
              p θ

              An induction principle to deduce results for Angle from those for , used with induction θ using Real.Angle.induction_on.

              @[simp]
              theorem Real.Angle.coe_zero :
              0 = 0
              @[simp]
              theorem Real.Angle.coe_add (x y : ) :
              ↑(x + y) = x + y
              @[simp]
              theorem Real.Angle.coe_neg (x : ) :
              ↑(-x) = -x
              @[simp]
              theorem Real.Angle.coe_sub (x y : ) :
              ↑(x - y) = x - y
              theorem Real.Angle.coe_nsmul (n : ) (x : ) :
              ↑(n x) = n x
              theorem Real.Angle.coe_zsmul (z : ) (x : ) :
              ↑(z x) = z x
              theorem Real.Angle.coe_eq_zero_iff {x : } :
              x = 0 ∃ (n : ), n (2 * Real.pi) = x
              @[simp]
              theorem Real.Angle.natCast_mul_eq_nsmul (x : ) (n : ) :
              ↑(n * x) = n x
              @[simp]
              theorem Real.Angle.intCast_mul_eq_zsmul (x : ) (n : ) :
              ↑(n * x) = n x
              theorem Real.Angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : } :
              θ = ψ ∃ (k : ), θ - ψ = 2 * Real.pi * k
              @[simp]
              theorem Real.Angle.coe_two_pi :
              ↑(2 * Real.pi) = 0
              @[simp]
              theorem Real.Angle.two_nsmul_coe_div_two (θ : ) :
              2 ↑(θ / 2) = θ
              @[simp]
              theorem Real.Angle.two_zsmul_coe_div_two (θ : ) :
              2 ↑(θ / 2) = θ
              theorem Real.Angle.zsmul_eq_iff {ψ θ : Angle} {z : } (hz : z 0) :
              z ψ = z θ ∃ (k : Fin z.natAbs), ψ = θ + k ↑(2 * Real.pi / z)
              theorem Real.Angle.nsmul_eq_iff {ψ θ : Angle} {n : } (hz : n 0) :
              n ψ = n θ ∃ (k : Fin n), ψ = θ + k ↑(2 * Real.pi / n)
              theorem Real.Angle.two_zsmul_eq_iff {ψ θ : Angle} :
              2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
              theorem Real.Angle.two_nsmul_eq_iff {ψ θ : Angle} :
              2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
              theorem Real.Angle.two_nsmul_eq_zero_iff {θ : Angle} :
              2 θ = 0 θ = 0 θ = Real.pi
              theorem Real.Angle.two_zsmul_eq_zero_iff {θ : Angle} :
              2 θ = 0 θ = 0 θ = Real.pi
              theorem Real.Angle.eq_neg_self_iff {θ : Angle} :
              θ = -θ θ = 0 θ = Real.pi
              theorem Real.Angle.ne_neg_self_iff {θ : Angle} :
              θ -θ θ 0 θ Real.pi
              theorem Real.Angle.neg_eq_self_iff {θ : Angle} :
              -θ = θ θ = 0 θ = Real.pi
              theorem Real.Angle.neg_ne_self_iff {θ : Angle} :
              -θ θ θ 0 θ Real.pi
              theorem Real.Angle.two_nsmul_eq_pi_iff {θ : Angle} :
              2 θ = Real.pi θ = ↑(Real.pi / 2) θ = ↑(-Real.pi / 2)
              theorem Real.Angle.two_zsmul_eq_pi_iff {θ : Angle} :
              2 θ = Real.pi θ = ↑(Real.pi / 2) θ = ↑(-Real.pi / 2)
              theorem Real.Angle.cos_eq_iff_coe_eq_or_eq_neg {θ ψ : } :
              Real.cos θ = Real.cos ψ θ = ψ θ = -ψ
              theorem Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ ψ : } :
              Real.sin θ = Real.sin ψ θ = ψ θ + ψ = Real.pi
              theorem Real.Angle.cos_sin_inj {θ ψ : } (Hcos : Real.cos θ = Real.cos ψ) (Hsin : Real.sin θ = Real.sin ψ) :
              θ = ψ

              The sine of a Real.Angle.

              Equations
                Instances For
                  @[simp]
                  theorem Real.Angle.sin_coe (x : ) :
                  (↑x).sin = Real.sin x

                  The cosine of a Real.Angle.

                  Equations
                    Instances For
                      @[simp]
                      theorem Real.Angle.cos_coe (x : ) :
                      (↑x).cos = Real.cos x
                      theorem Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : Angle} {ψ : } :
                      θ.cos = Real.cos ψ θ = ψ θ = -ψ
                      theorem Real.Angle.cos_eq_iff_eq_or_eq_neg {θ ψ : Angle} :
                      θ.cos = ψ.cos θ = ψ θ = -ψ
                      theorem Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : Angle} {ψ : } :
                      θ.sin = Real.sin ψ θ = ψ θ + ψ = Real.pi
                      theorem Real.Angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : Angle} :
                      θ.sin = ψ.sin θ = ψ θ + ψ = Real.pi
                      @[simp]
                      theorem Real.Angle.sin_eq_zero_iff {θ : Angle} :
                      θ.sin = 0 θ = 0 θ = Real.pi
                      @[simp]
                      theorem Real.Angle.sin_neg (θ : Angle) :
                      (-θ).sin = -θ.sin
                      @[simp]
                      theorem Real.Angle.sin_add_pi (θ : Angle) :
                      (θ + Real.pi).sin = -θ.sin
                      @[simp]
                      theorem Real.Angle.sin_sub_pi (θ : Angle) :
                      (θ - Real.pi).sin = -θ.sin
                      @[simp]
                      @[simp]
                      theorem Real.Angle.cos_neg (θ : Angle) :
                      (-θ).cos = θ.cos
                      @[simp]
                      theorem Real.Angle.cos_add_pi (θ : Angle) :
                      (θ + Real.pi).cos = -θ.cos
                      @[simp]
                      theorem Real.Angle.cos_sub_pi (θ : Angle) :
                      (θ - Real.pi).cos = -θ.cos
                      theorem Real.Angle.cos_eq_zero_iff {θ : Angle} :
                      θ.cos = 0 θ = ↑(Real.pi / 2) θ = ↑(-Real.pi / 2)
                      theorem Real.Angle.sin_add (θ₁ θ₂ : Angle) :
                      (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
                      theorem Real.Angle.cos_add (θ₁ θ₂ : Angle) :
                      (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
                      @[simp]
                      theorem Real.Angle.cos_sq_add_sin_sq (θ : Angle) :
                      θ.cos ^ 2 + θ.sin ^ 2 = 1
                      theorem Real.Angle.sin_add_pi_div_two (θ : Angle) :
                      (θ + ↑(Real.pi / 2)).sin = θ.cos
                      theorem Real.Angle.sin_sub_pi_div_two (θ : Angle) :
                      (θ - ↑(Real.pi / 2)).sin = -θ.cos
                      theorem Real.Angle.sin_pi_div_two_sub (θ : Angle) :
                      (↑(Real.pi / 2) - θ).sin = θ.cos
                      theorem Real.Angle.cos_add_pi_div_two (θ : Angle) :
                      (θ + ↑(Real.pi / 2)).cos = -θ.sin
                      theorem Real.Angle.cos_sub_pi_div_two (θ : Angle) :
                      (θ - ↑(Real.pi / 2)).cos = θ.sin
                      theorem Real.Angle.cos_pi_div_two_sub (θ : Angle) :
                      (↑(Real.pi / 2) - θ).cos = θ.sin
                      theorem Real.Angle.abs_sin_eq_of_two_nsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                      |θ.sin| = |ψ.sin|
                      theorem Real.Angle.abs_sin_eq_of_two_zsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                      |θ.sin| = |ψ.sin|
                      theorem Real.Angle.abs_cos_eq_of_two_nsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                      |θ.cos| = |ψ.cos|
                      theorem Real.Angle.abs_cos_eq_of_two_zsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                      |θ.cos| = |ψ.cos|
                      @[simp]
                      theorem Real.Angle.coe_toIcoMod (θ ψ : ) :
                      (toIcoMod two_pi_pos ψ θ) = θ
                      @[simp]
                      theorem Real.Angle.coe_toIocMod (θ ψ : ) :
                      (toIocMod two_pi_pos ψ θ) = θ

                      Convert a Real.Angle to a real number in the interval Ioc (-π) π.

                      Equations
                        Instances For
                          @[simp]
                          theorem Real.Angle.toReal_inj {θ ψ : Angle} :
                          θ.toReal = ψ.toReal θ = ψ
                          @[simp]
                          theorem Real.Angle.coe_toReal (θ : Angle) :
                          θ.toReal = θ
                          @[simp]
                          theorem Real.Angle.toReal_eq_zero_iff {θ : Angle} :
                          θ.toReal = 0 θ = 0
                          theorem Real.Angle.nsmul_toReal_eq_mul {n : } (h : n 0) {θ : Angle} :
                          (n θ).toReal = n * θ.toReal θ.toReal Set.Ioc (-Real.pi / n) (Real.pi / n)
                          theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : } {k : } :
                          (↑θ).toReal = θ - 2 * k * Real.pi θ Set.Ioc ((2 * k - 1) * Real.pi) ((2 * k + 1) * Real.pi)
                          @[simp]
                          @[simp]

                          The tangent of a Real.Angle.

                          Equations
                            Instances For
                              @[simp]
                              theorem Real.Angle.tan_coe (x : ) :
                              (↑x).tan = Real.tan x
                              @[simp]
                              @[simp]
                              theorem Real.Angle.tan_add_pi (θ : Angle) :
                              (θ + Real.pi).tan = θ.tan
                              @[simp]
                              theorem Real.Angle.tan_sub_pi (θ : Angle) :
                              (θ - Real.pi).tan = θ.tan
                              @[simp]
                              theorem Real.Angle.tan_eq_of_two_nsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                              θ.tan = ψ.tan
                              theorem Real.Angle.tan_eq_of_two_zsmul_eq {θ ψ : Angle} (h : 2 θ = 2 ψ) :
                              θ.tan = ψ.tan

                              The sign of a Real.Angle is 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π and -1 is the angle is strictly between and 0. It is defined as the sign of the sine of the angle.

                              Equations
                                Instances For
                                  @[simp]
                                  @[simp]
                                  @[simp]
                                  theorem Real.Angle.sign_neg (θ : Angle) :
                                  (-θ).sign = -θ.sign
                                  @[simp]
                                  theorem Real.Angle.sign_add_pi (θ : Angle) :
                                  (θ + Real.pi).sign = -θ.sign
                                  @[simp]
                                  theorem Real.Angle.sign_pi_add (θ : Angle) :
                                  (Real.pi + θ).sign = -θ.sign
                                  @[simp]
                                  theorem Real.Angle.sign_sub_pi (θ : Angle) :
                                  (θ - Real.pi).sign = -θ.sign
                                  @[simp]
                                  theorem Real.Angle.sign_pi_sub (θ : Angle) :
                                  (Real.pi - θ).sign = θ.sign
                                  theorem Real.Angle.sign_eq_zero_iff {θ : Angle} :
                                  θ.sign = 0 θ = 0 θ = Real.pi
                                  @[simp]
                                  theorem Real.Angle.sign_toReal {θ : Angle} (h : θ Real.pi) :
                                  theorem Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : θ Real.pi) :
                                  0 (↑θ).sign
                                  theorem Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : θ Real.pi) :
                                  (-θ).sign 0
                                  theorem Real.Angle.continuousAt_sign {θ : Angle} (h0 : θ 0) (hpi : θ Real.pi) :
                                  theorem ContinuousOn.angle_sign_comp {α : Type u_1} [TopologicalSpace α] {f : αReal.Angle} {s : Set α} (hf : ContinuousOn f s) (hs : zs, f z 0 f z Real.pi) :
                                  theorem Real.Angle.sign_eq_of_continuousOn {α : Type u_1} [TopologicalSpace α] {f : αAngle} {s : Set α} {x y : α} (hc : IsConnected s) (hf : ContinuousOn f s) (hs : zs, f z 0 f z Real.pi) (hx : x s) (hy : y s) :
                                  (f y).sign = (f x).sign

                                  Suppose a function to angles is continuous on a connected set and never takes the values 0 or π on that set. Then the values of the function on that set all have the same sign.