Documentation

Mathlib.Data.Complex.Exponential

Exponential, trigonometric and hyperbolic trigonometric functions #

This file contains the definitions of the real and complex exponential, sine, cosine, tangent, hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.

theorem Complex.isCauSeq_abs_exp (z : ) :
IsCauSeq abs fun (n : ) => mFinset.range n, Complex.abs (z ^ m / m.factorial)
theorem Complex.isCauSeq_exp (z : ) :
IsCauSeq Complex.abs fun (n : ) => mFinset.range n, z ^ m / m.factorial

The Cauchy sequence consisting of partial sums of the Taylor series of the complex exponential function

Equations
Instances For
    def Complex.exp (z : ) :

    The complex exponential function, defined via its Taylor series

    Equations
    • z.exp = z.exp'.lim
    Instances For
      def Complex.sin (z : ) :

      The complex sine function, defined via exp

      Equations
      Instances For
        def Complex.cos (z : ) :

        The complex cosine function, defined via exp

        Equations
        Instances For
          def Complex.tan (z : ) :

          The complex tangent function, defined as sin z / cos z

          Equations
          • z.tan = z.sin / z.cos
          Instances For
            def Complex.cot (z : ) :

            The complex cotangent function, defined as cos z / sin z

            Equations
            • z.cot = z.cos / z.sin
            Instances For
              def Complex.sinh (z : ) :

              The complex hyperbolic sine function, defined via exp

              Equations
              • z.sinh = (z.exp - (-z).exp) / 2
              Instances For
                def Complex.cosh (z : ) :

                The complex hyperbolic cosine function, defined via exp

                Equations
                • z.cosh = (z.exp + (-z).exp) / 2
                Instances For
                  def Complex.tanh (z : ) :

                  The complex hyperbolic tangent function, defined as sinh z / cosh z

                  Equations
                  • z.tanh = z.sinh / z.cosh
                  Instances For

                    scoped notation for the complex exponential function

                    Equations
                    Instances For
                      def Real.exp (x : ) :

                      The real exponential function, defined as the real part of the complex exponential

                      Equations
                      • x.exp = (x).exp.re
                      Instances For
                        def Real.sin (x : ) :

                        The real sine function, defined as the real part of the complex sine

                        Equations
                        • x.sin = (x).sin.re
                        Instances For
                          def Real.cos (x : ) :

                          The real cosine function, defined as the real part of the complex cosine

                          Equations
                          • x.cos = (x).cos.re
                          Instances For
                            def Real.tan (x : ) :

                            The real tangent function, defined as the real part of the complex tangent

                            Equations
                            • x.tan = (x).tan.re
                            Instances For
                              def Real.cot (x : ) :

                              The real cotangent function, defined as the real part of the complex cotangent

                              Equations
                              • x.cot = (x).cot.re
                              Instances For
                                def Real.sinh (x : ) :

                                The real hypebolic sine function, defined as the real part of the complex hyperbolic sine

                                Equations
                                • x.sinh = (x).sinh.re
                                Instances For
                                  def Real.cosh (x : ) :

                                  The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine

                                  Equations
                                  • x.cosh = (x).cosh.re
                                  Instances For
                                    def Real.tanh (x : ) :

                                    The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent

                                    Equations
                                    • x.tanh = (x).tanh.re
                                    Instances For

                                      scoped notation for the real exponential function

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Complex.exp_add (x : ) (y : ) :
                                        (x + y).exp = x.exp * y.exp

                                        the exponential function as a monoid hom from Multiplicative to

                                        Equations
                                        Instances For
                                          theorem Complex.exp_list_sum (l : List ) :
                                          l.sum.exp = (List.map Complex.exp l).prod
                                          theorem Complex.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                          (xs, f x).exp = xs, (f x).exp
                                          theorem Complex.exp_nsmul (x : ) (n : ) :
                                          (n x).exp = x.exp ^ n
                                          theorem Complex.exp_nat_mul (x : ) (n : ) :
                                          (n * x).exp = x.exp ^ n
                                          theorem Complex.exp_ne_zero (x : ) :
                                          x.exp 0
                                          theorem Complex.exp_neg (x : ) :
                                          (-x).exp = x.exp⁻¹
                                          theorem Complex.exp_sub (x : ) (y : ) :
                                          (x - y).exp = x.exp / y.exp
                                          theorem Complex.exp_int_mul (z : ) (n : ) :
                                          (n * z).exp = z.exp ^ n
                                          @[simp]
                                          theorem Complex.exp_conj (x : ) :
                                          ((starRingEnd ) x).exp = (starRingEnd ) x.exp
                                          @[simp]
                                          theorem Complex.ofReal_exp_ofReal_re (x : ) :
                                          (x).exp.re = (x).exp
                                          @[simp]
                                          theorem Complex.ofReal_exp (x : ) :
                                          x.exp = (x).exp
                                          @[simp]
                                          theorem Complex.exp_ofReal_im (x : ) :
                                          (x).exp.im = 0
                                          theorem Complex.exp_ofReal_re (x : ) :
                                          (x).exp.re = x.exp
                                          theorem Complex.two_sinh (x : ) :
                                          2 * x.sinh = x.exp - (-x).exp
                                          theorem Complex.two_cosh (x : ) :
                                          2 * x.cosh = x.exp + (-x).exp
                                          @[simp]
                                          theorem Complex.sinh_neg (x : ) :
                                          (-x).sinh = -x.sinh
                                          theorem Complex.sinh_add (x : ) (y : ) :
                                          (x + y).sinh = x.sinh * y.cosh + x.cosh * y.sinh
                                          @[simp]
                                          theorem Complex.cosh_neg (x : ) :
                                          (-x).cosh = x.cosh
                                          theorem Complex.cosh_add (x : ) (y : ) :
                                          (x + y).cosh = x.cosh * y.cosh + x.sinh * y.sinh
                                          theorem Complex.sinh_sub (x : ) (y : ) :
                                          (x - y).sinh = x.sinh * y.cosh - x.cosh * y.sinh
                                          theorem Complex.cosh_sub (x : ) (y : ) :
                                          (x - y).cosh = x.cosh * y.cosh - x.sinh * y.sinh
                                          theorem Complex.sinh_conj (x : ) :
                                          ((starRingEnd ) x).sinh = (starRingEnd ) x.sinh
                                          @[simp]
                                          theorem Complex.ofReal_sinh_ofReal_re (x : ) :
                                          (x).sinh.re = (x).sinh
                                          @[simp]
                                          theorem Complex.ofReal_sinh (x : ) :
                                          x.sinh = (x).sinh
                                          @[simp]
                                          theorem Complex.sinh_ofReal_im (x : ) :
                                          (x).sinh.im = 0
                                          theorem Complex.sinh_ofReal_re (x : ) :
                                          (x).sinh.re = x.sinh
                                          theorem Complex.cosh_conj (x : ) :
                                          ((starRingEnd ) x).cosh = (starRingEnd ) x.cosh
                                          theorem Complex.ofReal_cosh_ofReal_re (x : ) :
                                          (x).cosh.re = (x).cosh
                                          @[simp]
                                          theorem Complex.ofReal_cosh (x : ) :
                                          x.cosh = (x).cosh
                                          @[simp]
                                          theorem Complex.cosh_ofReal_im (x : ) :
                                          (x).cosh.im = 0
                                          @[simp]
                                          theorem Complex.cosh_ofReal_re (x : ) :
                                          (x).cosh.re = x.cosh
                                          theorem Complex.tanh_eq_sinh_div_cosh (x : ) :
                                          x.tanh = x.sinh / x.cosh
                                          @[simp]
                                          theorem Complex.tanh_neg (x : ) :
                                          (-x).tanh = -x.tanh
                                          theorem Complex.tanh_conj (x : ) :
                                          ((starRingEnd ) x).tanh = (starRingEnd ) x.tanh
                                          @[simp]
                                          theorem Complex.ofReal_tanh_ofReal_re (x : ) :
                                          (x).tanh.re = (x).tanh
                                          @[simp]
                                          theorem Complex.ofReal_tanh (x : ) :
                                          x.tanh = (x).tanh
                                          @[simp]
                                          theorem Complex.tanh_ofReal_im (x : ) :
                                          (x).tanh.im = 0
                                          theorem Complex.tanh_ofReal_re (x : ) :
                                          (x).tanh.re = x.tanh
                                          @[simp]
                                          theorem Complex.cosh_add_sinh (x : ) :
                                          x.cosh + x.sinh = x.exp
                                          @[simp]
                                          theorem Complex.sinh_add_cosh (x : ) :
                                          x.sinh + x.cosh = x.exp
                                          @[simp]
                                          theorem Complex.exp_sub_cosh (x : ) :
                                          x.exp - x.cosh = x.sinh
                                          @[simp]
                                          theorem Complex.exp_sub_sinh (x : ) :
                                          x.exp - x.sinh = x.cosh
                                          @[simp]
                                          theorem Complex.cosh_sub_sinh (x : ) :
                                          x.cosh - x.sinh = (-x).exp
                                          @[simp]
                                          theorem Complex.sinh_sub_cosh (x : ) :
                                          x.sinh - x.cosh = -(-x).exp
                                          @[simp]
                                          theorem Complex.cosh_sq_sub_sinh_sq (x : ) :
                                          x.cosh ^ 2 - x.sinh ^ 2 = 1
                                          theorem Complex.cosh_sq (x : ) :
                                          x.cosh ^ 2 = x.sinh ^ 2 + 1
                                          theorem Complex.sinh_sq (x : ) :
                                          x.sinh ^ 2 = x.cosh ^ 2 - 1
                                          theorem Complex.cosh_two_mul (x : ) :
                                          (2 * x).cosh = x.cosh ^ 2 + x.sinh ^ 2
                                          theorem Complex.sinh_two_mul (x : ) :
                                          (2 * x).sinh = 2 * x.sinh * x.cosh
                                          theorem Complex.cosh_three_mul (x : ) :
                                          (3 * x).cosh = 4 * x.cosh ^ 3 - 3 * x.cosh
                                          theorem Complex.sinh_three_mul (x : ) :
                                          (3 * x).sinh = 4 * x.sinh ^ 3 + 3 * x.sinh
                                          @[simp]
                                          @[simp]
                                          theorem Complex.sin_neg (x : ) :
                                          (-x).sin = -x.sin
                                          theorem Complex.two_sin (x : ) :
                                          2 * x.sin = ((-x * Complex.I).exp - (x * Complex.I).exp) * Complex.I
                                          theorem Complex.two_cos (x : ) :
                                          2 * x.cos = (x * Complex.I).exp + (-x * Complex.I).exp
                                          theorem Complex.sinh_mul_I (x : ) :
                                          (x * Complex.I).sinh = x.sin * Complex.I
                                          theorem Complex.cosh_mul_I (x : ) :
                                          (x * Complex.I).cosh = x.cos
                                          theorem Complex.tanh_mul_I (x : ) :
                                          (x * Complex.I).tanh = x.tan * Complex.I
                                          theorem Complex.cos_mul_I (x : ) :
                                          (x * Complex.I).cos = x.cosh
                                          theorem Complex.sin_mul_I (x : ) :
                                          (x * Complex.I).sin = x.sinh * Complex.I
                                          theorem Complex.tan_mul_I (x : ) :
                                          (x * Complex.I).tan = x.tanh * Complex.I
                                          theorem Complex.sin_add (x : ) (y : ) :
                                          (x + y).sin = x.sin * y.cos + x.cos * y.sin
                                          @[simp]
                                          @[simp]
                                          theorem Complex.cos_neg (x : ) :
                                          (-x).cos = x.cos
                                          theorem Complex.cos_add (x : ) (y : ) :
                                          (x + y).cos = x.cos * y.cos - x.sin * y.sin
                                          theorem Complex.sin_sub (x : ) (y : ) :
                                          (x - y).sin = x.sin * y.cos - x.cos * y.sin
                                          theorem Complex.cos_sub (x : ) (y : ) :
                                          (x - y).cos = x.cos * y.cos + x.sin * y.sin
                                          theorem Complex.sin_add_mul_I (x : ) (y : ) :
                                          (x + y * Complex.I).sin = x.sin * y.cosh + x.cos * y.sinh * Complex.I
                                          theorem Complex.sin_eq (z : ) :
                                          z.sin = (z.re).sin * (z.im).cosh + (z.re).cos * (z.im).sinh * Complex.I
                                          theorem Complex.cos_add_mul_I (x : ) (y : ) :
                                          (x + y * Complex.I).cos = x.cos * y.cosh - x.sin * y.sinh * Complex.I
                                          theorem Complex.cos_eq (z : ) :
                                          z.cos = (z.re).cos * (z.im).cosh - (z.re).sin * (z.im).sinh * Complex.I
                                          theorem Complex.sin_sub_sin (x : ) (y : ) :
                                          x.sin - y.sin = 2 * ((x - y) / 2).sin * ((x + y) / 2).cos
                                          theorem Complex.cos_sub_cos (x : ) (y : ) :
                                          x.cos - y.cos = -2 * ((x + y) / 2).sin * ((x - y) / 2).sin
                                          theorem Complex.sin_add_sin (x : ) (y : ) :
                                          x.sin + y.sin = 2 * ((x + y) / 2).sin * ((x - y) / 2).cos
                                          theorem Complex.cos_add_cos (x : ) (y : ) :
                                          x.cos + y.cos = 2 * ((x + y) / 2).cos * ((x - y) / 2).cos
                                          theorem Complex.sin_conj (x : ) :
                                          ((starRingEnd ) x).sin = (starRingEnd ) x.sin
                                          @[simp]
                                          theorem Complex.ofReal_sin_ofReal_re (x : ) :
                                          (x).sin.re = (x).sin
                                          @[simp]
                                          theorem Complex.ofReal_sin (x : ) :
                                          x.sin = (x).sin
                                          @[simp]
                                          theorem Complex.sin_ofReal_im (x : ) :
                                          (x).sin.im = 0
                                          theorem Complex.sin_ofReal_re (x : ) :
                                          (x).sin.re = x.sin
                                          theorem Complex.cos_conj (x : ) :
                                          ((starRingEnd ) x).cos = (starRingEnd ) x.cos
                                          @[simp]
                                          theorem Complex.ofReal_cos_ofReal_re (x : ) :
                                          (x).cos.re = (x).cos
                                          @[simp]
                                          theorem Complex.ofReal_cos (x : ) :
                                          x.cos = (x).cos
                                          @[simp]
                                          theorem Complex.cos_ofReal_im (x : ) :
                                          (x).cos.im = 0
                                          theorem Complex.cos_ofReal_re (x : ) :
                                          (x).cos.re = x.cos
                                          @[simp]
                                          theorem Complex.tan_eq_sin_div_cos (x : ) :
                                          x.tan = x.sin / x.cos
                                          theorem Complex.tan_mul_cos {x : } (hx : x.cos 0) :
                                          x.tan * x.cos = x.sin
                                          @[simp]
                                          theorem Complex.tan_neg (x : ) :
                                          (-x).tan = -x.tan
                                          theorem Complex.tan_conj (x : ) :
                                          ((starRingEnd ) x).tan = (starRingEnd ) x.tan
                                          @[simp]
                                          theorem Complex.ofReal_tan_ofReal_re (x : ) :
                                          (x).tan.re = (x).tan
                                          @[simp]
                                          theorem Complex.ofReal_tan (x : ) :
                                          x.tan = (x).tan
                                          @[simp]
                                          theorem Complex.tan_ofReal_im (x : ) :
                                          (x).tan.im = 0
                                          theorem Complex.tan_ofReal_re (x : ) :
                                          (x).tan.re = x.tan
                                          theorem Complex.cos_add_sin_I (x : ) :
                                          x.cos + x.sin * Complex.I = (x * Complex.I).exp
                                          theorem Complex.cos_sub_sin_I (x : ) :
                                          x.cos - x.sin * Complex.I = (-x * Complex.I).exp
                                          @[simp]
                                          theorem Complex.sin_sq_add_cos_sq (x : ) :
                                          x.sin ^ 2 + x.cos ^ 2 = 1
                                          @[simp]
                                          theorem Complex.cos_sq_add_sin_sq (x : ) :
                                          x.cos ^ 2 + x.sin ^ 2 = 1
                                          theorem Complex.cos_two_mul' (x : ) :
                                          (2 * x).cos = x.cos ^ 2 - x.sin ^ 2
                                          theorem Complex.cos_two_mul (x : ) :
                                          (2 * x).cos = 2 * x.cos ^ 2 - 1
                                          theorem Complex.sin_two_mul (x : ) :
                                          (2 * x).sin = 2 * x.sin * x.cos
                                          theorem Complex.cos_sq (x : ) :
                                          x.cos ^ 2 = 1 / 2 + (2 * x).cos / 2
                                          theorem Complex.cos_sq' (x : ) :
                                          x.cos ^ 2 = 1 - x.sin ^ 2
                                          theorem Complex.sin_sq (x : ) :
                                          x.sin ^ 2 = 1 - x.cos ^ 2
                                          theorem Complex.inv_one_add_tan_sq {x : } (hx : x.cos 0) :
                                          (1 + x.tan ^ 2)⁻¹ = x.cos ^ 2
                                          theorem Complex.tan_sq_div_one_add_tan_sq {x : } (hx : x.cos 0) :
                                          x.tan ^ 2 / (1 + x.tan ^ 2) = x.sin ^ 2
                                          theorem Complex.cos_three_mul (x : ) :
                                          (3 * x).cos = 4 * x.cos ^ 3 - 3 * x.cos
                                          theorem Complex.sin_three_mul (x : ) :
                                          (3 * x).sin = 3 * x.sin - 4 * x.sin ^ 3
                                          theorem Complex.exp_mul_I (x : ) :
                                          (x * Complex.I).exp = x.cos + x.sin * Complex.I
                                          theorem Complex.exp_add_mul_I (x : ) (y : ) :
                                          (x + y * Complex.I).exp = x.exp * (y.cos + y.sin * Complex.I)
                                          theorem Complex.exp_eq_exp_re_mul_sin_add_cos (x : ) :
                                          x.exp = (x.re).exp * ((x.im).cos + (x.im).sin * Complex.I)
                                          theorem Complex.exp_re (x : ) :
                                          x.exp.re = x.re.exp * x.im.cos
                                          theorem Complex.exp_im (x : ) :
                                          x.exp.im = x.re.exp * x.im.sin
                                          @[simp]
                                          theorem Complex.exp_ofReal_mul_I_re (x : ) :
                                          (x * Complex.I).exp.re = x.cos
                                          @[simp]
                                          theorem Complex.exp_ofReal_mul_I_im (x : ) :
                                          (x * Complex.I).exp.im = x.sin
                                          theorem Complex.cos_add_sin_mul_I_pow (n : ) (z : ) :
                                          (z.cos + z.sin * Complex.I) ^ n = (n * z).cos + (n * z).sin * Complex.I

                                          De Moivre's formula

                                          @[simp]
                                          theorem Real.exp_zero :
                                          theorem Real.exp_add (x : ) (y : ) :
                                          (x + y).exp = x.exp * y.exp

                                          the exponential function as a monoid hom from Multiplicative to

                                          Equations
                                          Instances For
                                            theorem Real.exp_list_sum (l : List ) :
                                            l.sum.exp = (List.map Real.exp l).prod
                                            theorem Real.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                            (xs, f x).exp = xs, (f x).exp
                                            theorem Real.exp_nsmul (x : ) (n : ) :
                                            (n x).exp = x.exp ^ n
                                            theorem Real.exp_nat_mul (x : ) (n : ) :
                                            (n * x).exp = x.exp ^ n
                                            theorem Real.exp_ne_zero (x : ) :
                                            x.exp 0
                                            theorem Real.exp_neg (x : ) :
                                            (-x).exp = x.exp⁻¹
                                            theorem Real.exp_sub (x : ) (y : ) :
                                            (x - y).exp = x.exp / y.exp
                                            @[simp]
                                            theorem Real.sin_zero :
                                            @[simp]
                                            theorem Real.sin_neg (x : ) :
                                            (-x).sin = -x.sin
                                            theorem Real.sin_add (x : ) (y : ) :
                                            (x + y).sin = x.sin * y.cos + x.cos * y.sin
                                            @[simp]
                                            theorem Real.cos_zero :
                                            @[simp]
                                            theorem Real.cos_neg (x : ) :
                                            (-x).cos = x.cos
                                            @[simp]
                                            theorem Real.cos_abs (x : ) :
                                            |x|.cos = x.cos
                                            theorem Real.cos_add (x : ) (y : ) :
                                            (x + y).cos = x.cos * y.cos - x.sin * y.sin
                                            theorem Real.sin_sub (x : ) (y : ) :
                                            (x - y).sin = x.sin * y.cos - x.cos * y.sin
                                            theorem Real.cos_sub (x : ) (y : ) :
                                            (x - y).cos = x.cos * y.cos + x.sin * y.sin
                                            theorem Real.sin_sub_sin (x : ) (y : ) :
                                            x.sin - y.sin = 2 * ((x - y) / 2).sin * ((x + y) / 2).cos
                                            theorem Real.cos_sub_cos (x : ) (y : ) :
                                            x.cos - y.cos = -2 * ((x + y) / 2).sin * ((x - y) / 2).sin
                                            theorem Real.cos_add_cos (x : ) (y : ) :
                                            x.cos + y.cos = 2 * ((x + y) / 2).cos * ((x - y) / 2).cos
                                            theorem Real.tan_eq_sin_div_cos (x : ) :
                                            x.tan = x.sin / x.cos
                                            theorem Real.tan_mul_cos {x : } (hx : x.cos 0) :
                                            x.tan * x.cos = x.sin
                                            @[simp]
                                            theorem Real.tan_zero :
                                            @[simp]
                                            theorem Real.tan_neg (x : ) :
                                            (-x).tan = -x.tan
                                            @[simp]
                                            theorem Real.sin_sq_add_cos_sq (x : ) :
                                            x.sin ^ 2 + x.cos ^ 2 = 1
                                            @[simp]
                                            theorem Real.cos_sq_add_sin_sq (x : ) :
                                            x.cos ^ 2 + x.sin ^ 2 = 1
                                            theorem Real.sin_sq_le_one (x : ) :
                                            x.sin ^ 2 1
                                            theorem Real.cos_sq_le_one (x : ) :
                                            x.cos ^ 2 1
                                            theorem Real.abs_sin_le_one (x : ) :
                                            |x.sin| 1
                                            theorem Real.abs_cos_le_one (x : ) :
                                            |x.cos| 1
                                            theorem Real.sin_le_one (x : ) :
                                            x.sin 1
                                            theorem Real.cos_le_one (x : ) :
                                            x.cos 1
                                            theorem Real.neg_one_le_sin (x : ) :
                                            -1 x.sin
                                            theorem Real.neg_one_le_cos (x : ) :
                                            -1 x.cos
                                            theorem Real.cos_two_mul (x : ) :
                                            (2 * x).cos = 2 * x.cos ^ 2 - 1
                                            theorem Real.cos_two_mul' (x : ) :
                                            (2 * x).cos = x.cos ^ 2 - x.sin ^ 2
                                            theorem Real.sin_two_mul (x : ) :
                                            (2 * x).sin = 2 * x.sin * x.cos
                                            theorem Real.cos_sq (x : ) :
                                            x.cos ^ 2 = 1 / 2 + (2 * x).cos / 2
                                            theorem Real.cos_sq' (x : ) :
                                            x.cos ^ 2 = 1 - x.sin ^ 2
                                            theorem Real.sin_sq (x : ) :
                                            x.sin ^ 2 = 1 - x.cos ^ 2
                                            theorem Real.sin_sq_eq_half_sub (x : ) :
                                            x.sin ^ 2 = 1 / 2 - (2 * x).cos / 2
                                            theorem Real.abs_sin_eq_sqrt_one_sub_cos_sq (x : ) :
                                            |x.sin| = (1 - x.cos ^ 2)
                                            theorem Real.abs_cos_eq_sqrt_one_sub_sin_sq (x : ) :
                                            |x.cos| = (1 - x.sin ^ 2)
                                            theorem Real.inv_one_add_tan_sq {x : } (hx : x.cos 0) :
                                            (1 + x.tan ^ 2)⁻¹ = x.cos ^ 2
                                            theorem Real.tan_sq_div_one_add_tan_sq {x : } (hx : x.cos 0) :
                                            x.tan ^ 2 / (1 + x.tan ^ 2) = x.sin ^ 2
                                            theorem Real.inv_sqrt_one_add_tan_sq {x : } (hx : 0 < x.cos) :
                                            ((1 + x.tan ^ 2))⁻¹ = x.cos
                                            theorem Real.tan_div_sqrt_one_add_tan_sq {x : } (hx : 0 < x.cos) :
                                            x.tan / (1 + x.tan ^ 2) = x.sin
                                            theorem Real.cos_three_mul (x : ) :
                                            (3 * x).cos = 4 * x.cos ^ 3 - 3 * x.cos
                                            theorem Real.sin_three_mul (x : ) :
                                            (3 * x).sin = 3 * x.sin - 4 * x.sin ^ 3
                                            theorem Real.sinh_eq (x : ) :
                                            x.sinh = (x.exp - (-x).exp) / 2

                                            The definition of sinh in terms of exp.

                                            @[simp]
                                            @[simp]
                                            theorem Real.sinh_neg (x : ) :
                                            (-x).sinh = -x.sinh
                                            theorem Real.sinh_add (x : ) (y : ) :
                                            (x + y).sinh = x.sinh * y.cosh + x.cosh * y.sinh
                                            theorem Real.cosh_eq (x : ) :
                                            x.cosh = (x.exp + (-x).exp) / 2

                                            The definition of cosh in terms of exp.

                                            @[simp]
                                            @[simp]
                                            theorem Real.cosh_neg (x : ) :
                                            (-x).cosh = x.cosh
                                            @[simp]
                                            theorem Real.cosh_abs (x : ) :
                                            |x|.cosh = x.cosh
                                            theorem Real.cosh_add (x : ) (y : ) :
                                            (x + y).cosh = x.cosh * y.cosh + x.sinh * y.sinh
                                            theorem Real.sinh_sub (x : ) (y : ) :
                                            (x - y).sinh = x.sinh * y.cosh - x.cosh * y.sinh
                                            theorem Real.cosh_sub (x : ) (y : ) :
                                            (x - y).cosh = x.cosh * y.cosh - x.sinh * y.sinh
                                            theorem Real.tanh_eq_sinh_div_cosh (x : ) :
                                            x.tanh = x.sinh / x.cosh
                                            @[simp]
                                            @[simp]
                                            theorem Real.tanh_neg (x : ) :
                                            (-x).tanh = -x.tanh
                                            @[simp]
                                            theorem Real.cosh_add_sinh (x : ) :
                                            x.cosh + x.sinh = x.exp
                                            @[simp]
                                            theorem Real.sinh_add_cosh (x : ) :
                                            x.sinh + x.cosh = x.exp
                                            @[simp]
                                            theorem Real.exp_sub_cosh (x : ) :
                                            x.exp - x.cosh = x.sinh
                                            @[simp]
                                            theorem Real.exp_sub_sinh (x : ) :
                                            x.exp - x.sinh = x.cosh
                                            @[simp]
                                            theorem Real.cosh_sub_sinh (x : ) :
                                            x.cosh - x.sinh = (-x).exp
                                            @[simp]
                                            theorem Real.sinh_sub_cosh (x : ) :
                                            x.sinh - x.cosh = -(-x).exp
                                            @[simp]
                                            theorem Real.cosh_sq_sub_sinh_sq (x : ) :
                                            x.cosh ^ 2 - x.sinh ^ 2 = 1
                                            theorem Real.cosh_sq (x : ) :
                                            x.cosh ^ 2 = x.sinh ^ 2 + 1
                                            theorem Real.cosh_sq' (x : ) :
                                            x.cosh ^ 2 = 1 + x.sinh ^ 2
                                            theorem Real.sinh_sq (x : ) :
                                            x.sinh ^ 2 = x.cosh ^ 2 - 1
                                            theorem Real.cosh_two_mul (x : ) :
                                            (2 * x).cosh = x.cosh ^ 2 + x.sinh ^ 2
                                            theorem Real.sinh_two_mul (x : ) :
                                            (2 * x).sinh = 2 * x.sinh * x.cosh
                                            theorem Real.cosh_three_mul (x : ) :
                                            (3 * x).cosh = 4 * x.cosh ^ 3 - 3 * x.cosh
                                            theorem Real.sinh_three_mul (x : ) :
                                            (3 * x).sinh = 4 * x.sinh ^ 3 + 3 * x.sinh
                                            theorem Real.sum_le_exp_of_nonneg {x : } (hx : 0 x) (n : ) :
                                            iFinset.range n, x ^ i / i.factorial x.exp
                                            theorem Real.pow_div_factorial_le_exp (x : ) (hx : 0 x) (n : ) :
                                            x ^ n / n.factorial x.exp
                                            theorem Real.quadratic_le_exp_of_nonneg {x : } (hx : 0 x) :
                                            1 + x + x ^ 2 / 2 x.exp
                                            theorem Real.one_le_exp {x : } (hx : 0 x) :
                                            1 x.exp
                                            theorem Real.exp_pos (x : ) :
                                            0 < x.exp
                                            theorem Real.exp_nonneg (x : ) :
                                            0 x.exp
                                            @[simp]
                                            theorem Real.abs_exp (x : ) :
                                            |x.exp| = x.exp
                                            theorem Real.exp_abs_le (x : ) :
                                            |x|.exp x.exp + (-x).exp
                                            theorem Real.exp_lt_exp_of_lt {x : } {y : } (h : x < y) :
                                            x.exp < y.exp
                                            theorem Real.exp_le_exp_of_le {x : } {y : } (h : x y) :
                                            x.exp y.exp
                                            @[simp]
                                            theorem Real.exp_lt_exp {x : } {y : } :
                                            x.exp < y.exp x < y
                                            @[simp]
                                            theorem Real.exp_le_exp {x : } {y : } :
                                            x.exp y.exp x y
                                            @[simp]
                                            theorem Real.exp_eq_exp {x : } {y : } :
                                            x.exp = y.exp x = y
                                            @[simp]
                                            theorem Real.exp_eq_one_iff (x : ) :
                                            x.exp = 1 x = 0
                                            @[simp]
                                            theorem Real.one_lt_exp_iff {x : } :
                                            1 < x.exp 0 < x
                                            @[simp]
                                            theorem Real.exp_lt_one_iff {x : } :
                                            x.exp < 1 x < 0
                                            @[simp]
                                            theorem Real.exp_le_one_iff {x : } :
                                            x.exp 1 x 0
                                            @[simp]
                                            theorem Real.one_le_exp_iff {x : } :
                                            1 x.exp 0 x
                                            theorem Real.cosh_pos (x : ) :
                                            0 < x.cosh

                                            Real.cosh is always positive

                                            theorem Real.sinh_lt_cosh (x : ) :
                                            x.sinh < x.cosh
                                            theorem Complex.sum_div_factorial_le {α : Type u_1} [LinearOrderedField α] (n : ) (j : ) (hn : 0 < n) :
                                            mFinset.filter (fun (k : ) => n k) (Finset.range j), 1 / m.factorial n.succ / (n.factorial * n)
                                            theorem Complex.exp_bound {x : } (hx : Complex.abs x 1) {n : } (hn : 0 < n) :
                                            Complex.abs (x.exp - mFinset.range n, x ^ m / m.factorial) Complex.abs x ^ n * (n.succ * (n.factorial * n)⁻¹)
                                            theorem Complex.exp_bound' {x : } {n : } (hx : Complex.abs x / n.succ 1 / 2) :
                                            Complex.abs (x.exp - mFinset.range n, x ^ m / m.factorial) Complex.abs x ^ n / n.factorial * 2
                                            theorem Complex.abs_exp_sub_one_le {x : } (hx : Complex.abs x 1) :
                                            Complex.abs (x.exp - 1) 2 * Complex.abs x
                                            theorem Complex.abs_exp_sub_one_sub_id_le {x : } (hx : Complex.abs x 1) :
                                            Complex.abs (x.exp - 1 - x) Complex.abs x ^ 2
                                            theorem Real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
                                            |x.exp - mFinset.range n, x ^ m / m.factorial| |x| ^ n * (n.succ / (n.factorial * n))
                                            theorem Real.exp_bound' {x : } (h1 : 0 x) (h2 : x 1) {n : } (hn : 0 < n) :
                                            x.exp mFinset.range n, x ^ m / m.factorial + x ^ n * (n + 1) / (n.factorial * n)
                                            theorem Real.abs_exp_sub_one_le {x : } (hx : |x| 1) :
                                            |x.exp - 1| 2 * |x|
                                            theorem Real.abs_exp_sub_one_sub_id_le {x : } (hx : |x| 1) :
                                            |x.exp - 1 - x| x ^ 2
                                            noncomputable def Real.expNear (n : ) (x : ) (r : ) :

                                            A finite initial segment of the exponential series, followed by an arbitrary tail. For fixed n this is just a linear map wrt r, and each map is a simple linear function of the previous (see expNear_succ), with expNear n x r ⟶ exp x as n ⟶ ∞, for any r.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Real.expNear_zero (x : ) (r : ) :
                                              Real.expNear 0 x r = r
                                              @[simp]
                                              theorem Real.expNear_succ (n : ) (x : ) (r : ) :
                                              Real.expNear (n + 1) x r = Real.expNear n x (1 + x / (n + 1) * r)
                                              theorem Real.expNear_sub (n : ) (x : ) (r₁ : ) (r₂ : ) :
                                              Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / n.factorial * (r₁ - r₂)
                                              theorem Real.exp_approx_end (n : ) (m : ) (x : ) (e₁ : n + 1 = m) (h : |x| 1) :
                                              |x.exp - Real.expNear m x 0| |x| ^ m / m.factorial * ((m + 1) / m)
                                              theorem Real.exp_approx_succ {n : } {x : } {a₁ : } {b₁ : } (m : ) (e₁ : n + 1 = m) (a₂ : ) (b₂ : ) (e : |1 + x / m * a₂ - a₁| b₁ - |x| / m * b₂) (h : |x.exp - Real.expNear m x a₂| |x| ^ m / m.factorial * b₂) :
                                              |x.exp - Real.expNear n x a₁| |x| ^ n / n.factorial * b₁
                                              theorem Real.exp_approx_end' {n : } {x : } {a : } {b : } (m : ) (e₁ : n + 1 = m) (rm : ) (er : m = rm) (h : |x| 1) (e : |1 - a| b - |x| / rm * ((rm + 1) / rm)) :
                                              |x.exp - Real.expNear n x a| |x| ^ n / n.factorial * b
                                              theorem Real.exp_1_approx_succ_eq {n : } {a₁ : } {b₁ : } {m : } (en : n + 1 = m) {rm : } (er : m = rm) (h : |Real.exp 1 - Real.expNear m 1 ((a₁ - 1) * rm)| |1| ^ m / m.factorial * (b₁ * rm)) :
                                              |Real.exp 1 - Real.expNear n 1 a₁| |1| ^ n / n.factorial * b₁
                                              theorem Real.exp_approx_start (x : ) (a : ) (b : ) (h : |x.exp - Real.expNear 0 x a| |x| ^ 0 / (Nat.factorial 0) * b) :
                                              |x.exp - a| b
                                              theorem Real.cos_bound {x : } (hx : |x| 1) :
                                              |x.cos - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
                                              theorem Real.sin_bound {x : } (hx : |x| 1) :
                                              |x.sin - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
                                              theorem Real.cos_pos_of_le_one {x : } (hx : |x| 1) :
                                              0 < x.cos
                                              theorem Real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
                                              0 < x.sin
                                              theorem Real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
                                              0 < x.sin
                                              theorem Real.exp_bound_div_one_sub_of_interval' {x : } (h1 : 0 < x) (h2 : x < 1) :
                                              x.exp < 1 / (1 - x)
                                              theorem Real.exp_bound_div_one_sub_of_interval {x : } (h1 : 0 x) (h2 : x < 1) :
                                              x.exp 1 / (1 - x)
                                              theorem Real.add_one_lt_exp {x : } (hx : x 0) :
                                              x + 1 < x.exp
                                              theorem Real.add_one_le_exp (x : ) :
                                              x + 1 x.exp
                                              theorem Real.one_sub_lt_exp_neg {x : } (hx : x 0) :
                                              1 - x < (-x).exp
                                              theorem Real.one_sub_le_exp_neg (x : ) :
                                              1 - x (-x).exp
                                              theorem Real.one_sub_div_pow_le_exp_neg {n : } {t : } (ht' : t n) :
                                              (1 - t / n) ^ n (-t).exp

                                              Extension for the positivity tactic: Real.exp is always positive.

                                              Instances For

                                                Extension for the positivity tactic: Real.cosh is always positive.

                                                Instances For
                                                  @[simp]
                                                  theorem Complex.abs_cos_add_sin_mul_I (x : ) :
                                                  Complex.abs ((x).cos + (x).sin * Complex.I) = 1
                                                  @[simp]
                                                  theorem Complex.abs_exp_ofReal (x : ) :
                                                  Complex.abs (x).exp = x.exp
                                                  @[simp]
                                                  theorem Complex.abs_exp_ofReal_mul_I (x : ) :
                                                  Complex.abs (x * Complex.I).exp = 1
                                                  theorem Complex.abs_exp (z : ) :
                                                  Complex.abs z.exp = z.re.exp
                                                  theorem Complex.abs_exp_eq_iff_re_eq {x : } {y : } :
                                                  Complex.abs x.exp = Complex.abs y.exp x.re = y.re