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
    • r = r
    Instances For

      Coercion ℝ → Angle as an additive homomorphism.

      Equations
      Instances For
        theorem Real.Angle.induction_on {p : Real.AngleProp} (θ : Real.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
        @[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
        @[deprecated Real.Angle.natCast_mul_eq_nsmul]
        theorem Real.Angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
        (n * x) = n x

        Alias of Real.Angle.natCast_mul_eq_nsmul.

        @[deprecated Real.Angle.intCast_mul_eq_zsmul]
        theorem Real.Angle.coe_int_mul_eq_zsmul (x : ) (n : ) :
        (n * x) = n x

        Alias of Real.Angle.intCast_mul_eq_zsmul.

        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 {ψ : Real.Angle} {θ : Real.Angle} {z : } (hz : z 0) :
        z ψ = z θ ∃ (k : Fin z.natAbs), ψ = θ + k (2 * Real.pi / z)
        theorem Real.Angle.nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} {n : } (hz : n 0) :
        n ψ = n θ ∃ (k : Fin n), ψ = θ + k (2 * Real.pi / n)
        theorem Real.Angle.two_zsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
        2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
        theorem Real.Angle.two_nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
        2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
        theorem Real.Angle.eq_neg_self_iff {θ : Real.Angle} :
        θ = -θ θ = 0 θ = Real.pi
        theorem Real.Angle.neg_eq_self_iff {θ : Real.Angle} :
        -θ = θ θ = 0 θ = Real.pi
        theorem Real.Angle.two_nsmul_eq_pi_iff {θ : Real.Angle} :
        2 θ = Real.pi θ = (Real.pi / 2) θ = (-Real.pi / 2)
        theorem Real.Angle.two_zsmul_eq_pi_iff {θ : Real.Angle} :
        2 θ = Real.pi θ = (Real.pi / 2) θ = (-Real.pi / 2)
        theorem Real.Angle.cos_eq_iff_coe_eq_or_eq_neg {θ : } {ψ : } :
        θ.cos = ψ.cos θ = ψ θ = -ψ
        theorem Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ : } {ψ : } :
        θ.sin = ψ.sin θ = ψ θ + ψ = Real.pi
        theorem Real.Angle.cos_sin_inj {θ : } {ψ : } (Hcos : θ.cos = ψ.cos) (Hsin : θ.sin = ψ.sin) :
        θ = ψ

        The sine of a Real.Angle.

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

          The cosine of a Real.Angle.

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

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

            Equations
            Instances For
              theorem Real.Angle.toReal_coe_eq_self_iff {θ : } :
              (θ).toReal = θ -Real.pi < θ θ Real.pi
              @[simp]
              theorem Real.Angle.toReal_inj {θ : Real.Angle} {ψ : Real.Angle} :
              θ.toReal = ψ.toReal θ = ψ
              @[simp]
              theorem Real.Angle.coe_toReal (θ : Real.Angle) :
              θ.toReal = θ
              @[simp]
              @[simp]
              theorem Real.Angle.toReal_eq_zero_iff {θ : Real.Angle} :
              θ.toReal = 0 θ = 0
              @[simp]
              theorem Real.Angle.toReal_pi :
              (Real.pi).toReal = Real.pi
              @[simp]
              theorem Real.Angle.toReal_eq_pi_iff {θ : Real.Angle} :
              θ.toReal = Real.pi θ = Real.pi
              @[simp]
              theorem Real.Angle.toReal_pi_div_two :
              ((Real.pi / 2)).toReal = Real.pi / 2
              @[simp]
              theorem Real.Angle.toReal_eq_pi_div_two_iff {θ : Real.Angle} :
              θ.toReal = Real.pi / 2 θ = (Real.pi / 2)
              @[simp]
              @[simp]
              theorem Real.Angle.abs_toReal_coe_eq_self_iff {θ : } :
              |(θ).toReal| = θ 0 θ θ Real.pi
              theorem Real.Angle.abs_toReal_neg_coe_eq_self_iff {θ : } :
              |(-θ).toReal| = θ 0 θ θ Real.pi
              theorem Real.Angle.abs_toReal_eq_pi_div_two_iff {θ : Real.Angle} :
              |θ.toReal| = Real.pi / 2 θ = (Real.pi / 2) θ = (-Real.pi / 2)
              theorem Real.Angle.nsmul_toReal_eq_mul {n : } (h : n 0) {θ : Real.Angle} :
              (n θ).toReal = n * θ.toReal θ.toReal Set.Ioc (-Real.pi / n) (Real.pi / n)
              theorem Real.Angle.two_nsmul_toReal_eq_two_mul {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal θ.toReal Set.Ioc (-Real.pi / 2) (Real.pi / 2)
              theorem Real.Angle.two_zsmul_toReal_eq_two_mul {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal θ.toReal Set.Ioc (-Real.pi / 2) (Real.pi / 2)
              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)
              theorem Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal - 2 * Real.pi Real.pi / 2 < θ.toReal
              theorem Real.Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal - 2 * Real.pi Real.pi / 2 < θ.toReal
              theorem Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal + 2 * Real.pi θ.toReal -Real.pi / 2
              theorem Real.Angle.two_zsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} :
              (2 θ).toReal = 2 * θ.toReal + 2 * Real.pi θ.toReal -Real.pi / 2
              @[simp]
              theorem Real.Angle.sin_toReal (θ : Real.Angle) :
              θ.toReal.sin = θ.sin
              @[simp]
              theorem Real.Angle.cos_toReal (θ : Real.Angle) :
              θ.toReal.cos = θ.cos

              The tangent of a Real.Angle.

              Equations
              • θ.tan = θ.sin / θ.cos
              Instances For
                theorem Real.Angle.tan_eq_sin_div_cos (θ : Real.Angle) :
                θ.tan = θ.sin / θ.cos
                @[simp]
                theorem Real.Angle.tan_coe (x : ) :
                (x).tan = x.tan
                @[simp]
                theorem Real.Angle.tan_add_pi (θ : Real.Angle) :
                (θ + Real.pi).tan = θ.tan
                @[simp]
                theorem Real.Angle.tan_sub_pi (θ : Real.Angle) :
                (θ - Real.pi).tan = θ.tan
                @[simp]
                theorem Real.Angle.tan_toReal (θ : Real.Angle) :
                θ.toReal.tan = θ.tan
                theorem Real.Angle.tan_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
                θ.tan = ψ.tan
                theorem Real.Angle.tan_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.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
                • θ.sign = SignType.sign θ.sin
                Instances For
                  @[simp]
                  theorem Real.Angle.sign_coe_pi :
                  (Real.pi).sign = 0
                  @[simp]
                  theorem Real.Angle.sign_neg (θ : Real.Angle) :
                  (-θ).sign = -θ.sign
                  @[simp]
                  theorem Real.Angle.sign_add_pi (θ : Real.Angle) :
                  (θ + Real.pi).sign = -θ.sign
                  @[simp]
                  theorem Real.Angle.sign_pi_add (θ : Real.Angle) :
                  (Real.pi + θ).sign = -θ.sign
                  @[simp]
                  theorem Real.Angle.sign_sub_pi (θ : Real.Angle) :
                  (θ - Real.pi).sign = -θ.sign
                  @[simp]
                  theorem Real.Angle.sign_pi_sub (θ : Real.Angle) :
                  (Real.pi - θ).sign = θ.sign
                  theorem Real.Angle.sign_eq_zero_iff {θ : Real.Angle} :
                  θ.sign = 0 θ = 0 θ = Real.pi
                  theorem Real.Angle.sign_ne_zero_iff {θ : Real.Angle} :
                  θ.sign 0 θ 0 θ Real.pi
                  theorem Real.Angle.toReal_neg_iff_sign_neg {θ : Real.Angle} :
                  θ.toReal < 0 θ.sign = -1
                  @[simp]
                  theorem Real.Angle.sign_toReal {θ : Real.Angle} (h : θ Real.pi) :
                  SignType.sign θ.toReal = θ.sign
                  theorem Real.Angle.coe_abs_toReal_of_sign_nonneg {θ : Real.Angle} (h : 0 θ.sign) :
                  |θ.toReal| = θ
                  theorem Real.Angle.neg_coe_abs_toReal_of_sign_nonpos {θ : Real.Angle} (h : θ.sign 0) :
                  -|θ.toReal| = θ
                  theorem Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq {θ : Real.Angle} {ψ : Real.Angle} :
                  θ = ψ θ.sign = ψ.sign |θ.toReal| = |ψ.toReal|
                  theorem Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq {θ : Real.Angle} {ψ : Real.Angle} (h : θ.sign = ψ.sign) :
                  θ = ψ |θ.toReal| = |ψ.toReal|
                  @[simp]
                  theorem Real.Angle.sign_coe_pi_div_two :
                  ((Real.pi / 2)).sign = 1
                  @[simp]
                  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.sign_two_nsmul_eq_sign_iff {θ : Real.Angle} :
                  (2 θ).sign = θ.sign θ = Real.pi |θ.toReal| < Real.pi / 2
                  theorem Real.Angle.sign_two_zsmul_eq_sign_iff {θ : Real.Angle} :
                  (2 θ).sign = θ.sign θ = Real.pi |θ.toReal| < Real.pi / 2
                  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 : αReal.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.