Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Trigonometric functions #

Main definitions #

This file contains the definition of π.

See also Analysis.SpecialFunctions.Trigonometric.Inverse and Analysis.SpecialFunctions.Trigonometric.Arctan for the inverse trigonometric functions.

See also Analysis.SpecialFunctions.Complex.Arg and Analysis.SpecialFunctions.Complex.Log for the complex argument function and the complex logarithm.

Main statements #

Many basic inequalities on the real trigonometric functions are established.

The continuity of the usual trigonometric functions is proved.

Several facts about the real trigonometric functions have the proofs deferred to Analysis.SpecialFunctions.Trigonometric.Complex, as they are most easily proved by appealing to the corresponding fact for complex trigonometric functions.

See also Analysis.SpecialFunctions.Trigonometric.Chebyshev for the multiple angle formulas in terms of Chebyshev polynomials.

Tags #

sin, cos, tan, angle

noncomputable def Real.pi :

The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from which one can derive all its properties. For explicit bounds on π, see Data.Real.Pi.Bounds.

Equations
Instances For

    The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from which one can derive all its properties. For explicit bounds on π, see Data.Real.Pi.Bounds.

    Equations
    Instances For

      Extension for the positivity tactic: π is always positive.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def NNReal.pi :

        π considered as a nonnegative real.

        Equations
        Instances For
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          theorem Real.sin_nat_mul_pi (n : ) :
          Real.sin (n * Real.pi) = 0
          @[simp]
          theorem Real.sin_int_mul_pi (n : ) :
          Real.sin (n * Real.pi) = 0
          @[simp]
          theorem Real.sin_add_nat_mul_two_pi (x : ) (n : ) :
          Real.sin (x + n * (2 * Real.pi)) = Real.sin x
          @[simp]
          theorem Real.sin_add_int_mul_two_pi (x : ) (n : ) :
          Real.sin (x + n * (2 * Real.pi)) = Real.sin x
          @[simp]
          theorem Real.sin_sub_nat_mul_two_pi (x : ) (n : ) :
          Real.sin (x - n * (2 * Real.pi)) = Real.sin x
          @[simp]
          theorem Real.sin_sub_int_mul_two_pi (x : ) (n : ) :
          Real.sin (x - n * (2 * Real.pi)) = Real.sin x
          @[simp]
          theorem Real.sin_nat_mul_two_pi_sub (x : ) (n : ) :
          Real.sin (n * (2 * Real.pi) - x) = -Real.sin x
          @[simp]
          theorem Real.sin_int_mul_two_pi_sub (x : ) (n : ) :
          Real.sin (n * (2 * Real.pi) - x) = -Real.sin x
          theorem Real.sin_add_int_mul_pi (x : ) (n : ) :
          Real.sin (x + n * Real.pi) = (-1) ^ n * Real.sin x
          theorem Real.sin_add_nat_mul_pi (x : ) (n : ) :
          Real.sin (x + n * Real.pi) = (-1) ^ n * Real.sin x
          theorem Real.sin_sub_int_mul_pi (x : ) (n : ) :
          Real.sin (x - n * Real.pi) = (-1) ^ n * Real.sin x
          theorem Real.sin_sub_nat_mul_pi (x : ) (n : ) :
          Real.sin (x - n * Real.pi) = (-1) ^ n * Real.sin x
          theorem Real.sin_int_mul_pi_sub (x : ) (n : ) :
          Real.sin (n * Real.pi - x) = -((-1) ^ n * Real.sin x)
          theorem Real.sin_nat_mul_pi_sub (x : ) (n : ) :
          Real.sin (n * Real.pi - x) = -((-1) ^ n * Real.sin x)
          @[simp]
          theorem Real.abs_cos_int_mul_pi (k : ) :
          |Real.cos (k * Real.pi)| = 1
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          theorem Real.cos_nat_mul_two_pi (n : ) :
          Real.cos (n * (2 * Real.pi)) = 1
          @[simp]
          theorem Real.cos_int_mul_two_pi (n : ) :
          Real.cos (n * (2 * Real.pi)) = 1
          @[simp]
          theorem Real.cos_add_nat_mul_two_pi (x : ) (n : ) :
          Real.cos (x + n * (2 * Real.pi)) = Real.cos x
          @[simp]
          theorem Real.cos_add_int_mul_two_pi (x : ) (n : ) :
          Real.cos (x + n * (2 * Real.pi)) = Real.cos x
          @[simp]
          theorem Real.cos_sub_nat_mul_two_pi (x : ) (n : ) :
          Real.cos (x - n * (2 * Real.pi)) = Real.cos x
          @[simp]
          theorem Real.cos_sub_int_mul_two_pi (x : ) (n : ) :
          Real.cos (x - n * (2 * Real.pi)) = Real.cos x
          @[simp]
          theorem Real.cos_nat_mul_two_pi_sub (x : ) (n : ) :
          Real.cos (n * (2 * Real.pi) - x) = Real.cos x
          @[simp]
          theorem Real.cos_int_mul_two_pi_sub (x : ) (n : ) :
          Real.cos (n * (2 * Real.pi) - x) = Real.cos x
          theorem Real.cos_add_int_mul_pi (x : ) (n : ) :
          Real.cos (x + n * Real.pi) = (-1) ^ n * Real.cos x
          theorem Real.cos_add_nat_mul_pi (x : ) (n : ) :
          Real.cos (x + n * Real.pi) = (-1) ^ n * Real.cos x
          theorem Real.cos_sub_int_mul_pi (x : ) (n : ) :
          Real.cos (x - n * Real.pi) = (-1) ^ n * Real.cos x
          theorem Real.cos_sub_nat_mul_pi (x : ) (n : ) :
          Real.cos (x - n * Real.pi) = (-1) ^ n * Real.cos x
          theorem Real.cos_int_mul_pi_sub (x : ) (n : ) :
          Real.cos (n * Real.pi - x) = (-1) ^ n * Real.cos x
          theorem Real.cos_nat_mul_pi_sub (x : ) (n : ) :
          Real.cos (n * Real.pi - x) = (-1) ^ n * Real.cos x
          theorem Real.sin_pos_of_pos_of_lt_pi {x : } (h0x : 0 < x) (hxp : x < Real.pi) :
          theorem Real.sin_nonneg_of_nonneg_of_le_pi {x : } (h0x : 0 x) (hxp : x Real.pi) :
          theorem Real.sin_neg_of_neg_of_neg_pi_lt {x : } (hx0 : x < 0) (hpx : -Real.pi < x) :
          theorem Real.cos_pos_of_mem_Ioo {x : } (hx : x Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
          theorem Real.cos_neg_of_pi_div_two_lt_of_lt {x : } (hx₁ : Real.pi / 2 < x) (hx₂ : x < Real.pi + Real.pi / 2) :
          theorem Real.sin_eq_sqrt_one_sub_cos_sq {x : } (hl : 0 x) (hu : x Real.pi) :
          theorem Real.cos_eq_sqrt_one_sub_sin_sq {x : } (hl : -(Real.pi / 2) x) (hu : x Real.pi / 2) :
          theorem Real.cos_half {x : } (hl : -Real.pi x) (hr : x Real.pi) :
          Real.cos (x / 2) = ((1 + Real.cos x) / 2)
          theorem Real.abs_sin_half (x : ) :
          |Real.sin (x / 2)| = ((1 - Real.cos x) / 2)
          theorem Real.sin_half_eq_sqrt {x : } (hl : 0 x) (hr : x 2 * Real.pi) :
          Real.sin (x / 2) = ((1 - Real.cos x) / 2)
          theorem Real.sin_half_eq_neg_sqrt {x : } (hl : -(2 * Real.pi) x) (hr : x 0) :
          Real.sin (x / 2) = -((1 - Real.cos x) / 2)
          theorem Real.sin_eq_zero_iff_of_lt_of_lt {x : } (hx₁ : -Real.pi < x) (hx₂ : x < Real.pi) :
          Real.sin x = 0 x = 0
          theorem Real.sin_eq_zero_iff {x : } :
          Real.sin x = 0 ∃ (n : ), n * Real.pi = x
          theorem Real.sin_ne_zero_iff {x : } :
          Real.sin x 0 ∀ (n : ), n * Real.pi x
          theorem Real.cos_eq_one_iff (x : ) :
          Real.cos x = 1 ∃ (n : ), n * (2 * Real.pi) = x
          theorem Real.cos_eq_one_iff_of_lt_of_lt {x : } (hx₁ : -(2 * Real.pi) < x) (hx₂ : x < 2 * Real.pi) :
          Real.cos x = 1 x = 0
          theorem Real.sin_lt_sin_of_lt_of_le_pi_div_two {x : } {y : } (hx₁ : -(Real.pi / 2) x) (hy₂ : y Real.pi / 2) (hxy : x < y) :
          theorem Real.cos_lt_cos_of_nonneg_of_le_pi {x : } {y : } (hx₁ : 0 x) (hy₂ : y Real.pi) (hxy : x < y) :
          theorem Real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x : } {y : } (hx₁ : 0 x) (hy₂ : y Real.pi / 2) (hxy : x < y) :
          theorem Real.cos_le_cos_of_nonneg_of_le_pi {x : } {y : } (hx₁ : 0 x) (hy₂ : y Real.pi) (hxy : x y) :
          theorem Real.sin_le_sin_of_le_of_le_pi_div_two {x : } {y : } (hx₁ : -(Real.pi / 2) x) (hy₂ : y Real.pi / 2) (hxy : x y) :
          noncomputable def Real.sqrtTwoAddSeries (x : ) :

          the series sqrtTwoAddSeries x n is sqrt(2 + sqrt(2 + ... )) with n square roots, starting with x. We define it here because cos (pi / 2 ^ (n+1)) = sqrtTwoAddSeries 0 n / 2

          Equations
          • x.sqrtTwoAddSeries 0 = x
          • x.sqrtTwoAddSeries n.succ = (2 + x.sqrtTwoAddSeries n)
          Instances For
            theorem Real.sqrtTwoAddSeries_zero (x : ) :
            x.sqrtTwoAddSeries 0 = x
            theorem Real.sqrtTwoAddSeries_nonneg {x : } (h : 0 x) (n : ) :
            0 x.sqrtTwoAddSeries n
            theorem Real.sqrtTwoAddSeries_succ (x : ) (n : ) :
            x.sqrtTwoAddSeries (n + 1) = ((2 + x)).sqrtTwoAddSeries n
            theorem Real.sqrtTwoAddSeries_monotone_left {x : } {y : } (h : x y) (n : ) :
            x.sqrtTwoAddSeries n y.sqrtTwoAddSeries n
            @[simp]
            @[simp]
            @[simp]
            @[simp]
            @[simp]
            @[simp]
            @[simp]

            The cosine of π / 3 is 1 / 2.

            @[simp]

            The cosine of π / 6 is √3 / 2.

            The square of the cosine of π / 6 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

            @[simp]

            The sine of π / 6 is 1 / 2.

            The square of the sine of π / 3 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

            @[simp]

            The sine of π / 3 is √3 / 2.

            theorem Real.Polynomial.isRoot_cos_pi_div_five :
            (4 Polynomial.X ^ 2 - 2 Polynomial.X - Polynomial.C 1).IsRoot (Real.cos (Real.pi / 5))
            @[simp]

            The cosine of π / 5 is (1 + √5) / 4.

            def Real.sinOrderIso :
            (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) ≃o (Set.Icc (-1) 1)

            Real.sin as an OrderIso between [-(π / 2), π / 2] and [-1, 1].

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Real.coe_sinOrderIso_apply (x : (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :
              (Real.sinOrderIso x) = Real.sin x
              theorem Real.sinOrderIso_apply (x : (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) :
              Real.sinOrderIso x = Real.sin x,
              theorem Real.tan_pos_of_pos_of_lt_pi_div_two {x : } (h0x : 0 < x) (hxp : x < Real.pi / 2) :
              theorem Real.tan_neg_of_neg_of_pi_div_two_lt {x : } (hx0 : x < 0) (hpx : -(Real.pi / 2) < x) :
              theorem Real.tan_lt_tan_of_lt_of_lt_pi_div_two {x : } {y : } (hx₁ : -(Real.pi / 2) < x) (hy₂ : y < Real.pi / 2) (hxy : x < y) :
              theorem Real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x : } {y : } (hx₁ : 0 x) (hy₂ : y < Real.pi / 2) (hxy : x < y) :
              theorem Real.tan_inj_of_lt_of_lt_pi_div_two {x : } {y : } (hx₁ : -(Real.pi / 2) < x) (hx₂ : x < Real.pi / 2) (hy₁ : -(Real.pi / 2) < y) (hy₂ : y < Real.pi / 2) (hxy : Real.tan x = Real.tan y) :
              x = y
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              theorem Complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le {a : } {b : } (ha : a 0) {z : } (hz : |z.im| b) (hb : b Real.pi / 2) :
              Complex.abs (Complex.exp (a * (Complex.exp z + Complex.exp (-z)))) Real.exp (a * Real.cos b * Real.exp |z.re|)

              A supporting lemma for the Phragmen-Lindelöf principle in a horizontal strip. If z : ℂ belongs to a horizontal strip |Complex.im z| ≤ b, b ≤ π / 2, and a ≤ 0, then $$\left|exp^{a\left(e^{z}+e^{-z}\right)}\right| \le e^{a\cos b \exp^{|re z|}}.$$