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
    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
          Instances For
            def Complex.cot (z : ) :

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

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

              The complex hyperbolic sine function, defined via exp

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

                The complex hyperbolic cosine function, defined via exp

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

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

                  Equations
                  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
                      Instances For
                        def Real.sin (x : ) :

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

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

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

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

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

                            Equations
                            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
                                Instances For
                                  def Real.cosh (x : ) :

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

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

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

                                    Equations
                                    Instances For

                                      scoped notation for the real exponential function

                                      Equations
                                      Instances For
                                        @[simp]

                                        the exponential function as a monoid hom from Multiplicative to

                                        Equations
                                        Instances For
                                          theorem Complex.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                          Complex.exp (xs, f x) = xs, Complex.exp (f x)
                                          theorem Complex.exp_nsmul (x : ) (n : ) :
                                          theorem Complex.exp_nat_mul (x : ) (n : ) :
                                          Complex.exp (n * x) = Complex.exp x ^ n
                                          @[simp]
                                          theorem Complex.exp_int_mul (z : ) (n : ) :
                                          Complex.exp (n * z) = Complex.exp z ^ n
                                          @[simp]
                                          theorem Complex.ofReal_exp_ofReal_re (x : ) :
                                          (Complex.exp x).re = Complex.exp x
                                          @[simp]
                                          theorem Complex.ofReal_exp (x : ) :
                                          (Real.exp x) = Complex.exp x
                                          @[simp]
                                          theorem Complex.exp_ofReal_im (x : ) :
                                          (Complex.exp x).im = 0
                                          @[simp]
                                          @[simp]
                                          theorem Complex.ofReal_sinh (x : ) :
                                          @[simp]
                                          theorem Complex.sinh_ofReal_im (x : ) :
                                          (Complex.sinh x).im = 0
                                          @[simp]
                                          theorem Complex.ofReal_cosh (x : ) :
                                          @[simp]
                                          theorem Complex.cosh_ofReal_im (x : ) :
                                          (Complex.cosh x).im = 0
                                          @[simp]
                                          @[simp]
                                          @[simp]
                                          theorem Complex.ofReal_tanh (x : ) :
                                          @[simp]
                                          theorem Complex.tanh_ofReal_im (x : ) :
                                          (Complex.tanh x).im = 0
                                          @[simp]
                                          @[simp]
                                          @[simp]
                                          @[simp]
                                          theorem Complex.sin_sub_sin (x : ) (y : ) :
                                          Complex.sin x - Complex.sin y = 2 * Complex.sin ((x - y) / 2) * Complex.cos ((x + y) / 2)
                                          theorem Complex.cos_sub_cos (x : ) (y : ) :
                                          Complex.cos x - Complex.cos y = -2 * Complex.sin ((x + y) / 2) * Complex.sin ((x - y) / 2)
                                          theorem Complex.sin_add_sin (x : ) (y : ) :
                                          Complex.sin x + Complex.sin y = 2 * Complex.sin ((x + y) / 2) * Complex.cos ((x - y) / 2)
                                          theorem Complex.cos_add_cos (x : ) (y : ) :
                                          Complex.cos x + Complex.cos y = 2 * Complex.cos ((x + y) / 2) * Complex.cos ((x - y) / 2)
                                          @[simp]
                                          theorem Complex.ofReal_sin_ofReal_re (x : ) :
                                          (Complex.sin x).re = Complex.sin x
                                          @[simp]
                                          theorem Complex.ofReal_sin (x : ) :
                                          (Real.sin x) = Complex.sin x
                                          @[simp]
                                          theorem Complex.sin_ofReal_im (x : ) :
                                          (Complex.sin x).im = 0
                                          @[simp]
                                          theorem Complex.ofReal_cos_ofReal_re (x : ) :
                                          (Complex.cos x).re = Complex.cos x
                                          @[simp]
                                          theorem Complex.ofReal_cos (x : ) :
                                          (Real.cos x) = Complex.cos x
                                          @[simp]
                                          theorem Complex.cos_ofReal_im (x : ) :
                                          (Complex.cos x).im = 0
                                          @[simp]
                                          @[simp]
                                          @[simp]
                                          theorem Complex.ofReal_tan_ofReal_re (x : ) :
                                          (Complex.tan x).re = Complex.tan x
                                          @[simp]
                                          theorem Complex.ofReal_tan (x : ) :
                                          (Real.tan x) = Complex.tan x
                                          @[simp]
                                          theorem Complex.tan_ofReal_im (x : ) :
                                          (Complex.tan x).im = 0
                                          @[simp]
                                          @[simp]
                                          theorem Complex.cos_two_mul (x : ) :
                                          Complex.cos (2 * x) = 2 * Complex.cos x ^ 2 - 1
                                          theorem Complex.cos_sq (x : ) :
                                          Complex.cos x ^ 2 = 1 / 2 + Complex.cos (2 * x) / 2
                                          theorem Complex.exp_re (x : ) :
                                          (Complex.exp x).re = Real.exp x.re * Real.cos x.im
                                          theorem Complex.exp_im (x : ) :
                                          (Complex.exp x).im = Real.exp x.re * Real.sin x.im

                                          De Moivre's formula

                                          @[simp]
                                          theorem Real.exp_zero :
                                          theorem Real.exp_add (x : ) (y : ) :

                                          the exponential function as a monoid hom from Multiplicative to

                                          Equations
                                          Instances For
                                            theorem Real.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                            Real.exp (xs, f x) = xs, Real.exp (f x)
                                            theorem Real.exp_nsmul (x : ) (n : ) :
                                            Real.exp (n x) = Real.exp x ^ n
                                            theorem Real.exp_nat_mul (x : ) (n : ) :
                                            Real.exp (n * x) = Real.exp x ^ n
                                            @[simp]
                                            theorem Real.exp_ne_zero (x : ) :
                                            theorem Real.exp_sub (x : ) (y : ) :
                                            @[simp]
                                            theorem Real.sin_zero :
                                            @[simp]
                                            theorem Real.sin_neg (x : ) :
                                            theorem Real.sin_add (x : ) (y : ) :
                                            @[simp]
                                            theorem Real.cos_zero :
                                            @[simp]
                                            theorem Real.cos_neg (x : ) :
                                            @[simp]
                                            theorem Real.cos_abs (x : ) :
                                            theorem Real.cos_add (x : ) (y : ) :
                                            theorem Real.sin_sub (x : ) (y : ) :
                                            theorem Real.cos_sub (x : ) (y : ) :
                                            theorem Real.sin_sub_sin (x : ) (y : ) :
                                            Real.sin x - Real.sin y = 2 * Real.sin ((x - y) / 2) * Real.cos ((x + y) / 2)
                                            theorem Real.cos_sub_cos (x : ) (y : ) :
                                            Real.cos x - Real.cos y = -2 * Real.sin ((x + y) / 2) * Real.sin ((x - y) / 2)
                                            theorem Real.cos_add_cos (x : ) (y : ) :
                                            Real.cos x + Real.cos y = 2 * Real.cos ((x + y) / 2) * Real.cos ((x - y) / 2)
                                            @[simp]
                                            theorem Real.tan_zero :
                                            @[simp]
                                            theorem Real.tan_neg (x : ) :
                                            @[simp]
                                            theorem Real.sin_sq_add_cos_sq (x : ) :
                                            Real.sin x ^ 2 + Real.cos x ^ 2 = 1
                                            @[simp]
                                            theorem Real.cos_sq_add_sin_sq (x : ) :
                                            Real.cos x ^ 2 + Real.sin x ^ 2 = 1
                                            theorem Real.cos_two_mul (x : ) :
                                            Real.cos (2 * x) = 2 * Real.cos x ^ 2 - 1
                                            theorem Real.cos_two_mul' (x : ) :
                                            Real.cos (2 * x) = Real.cos x ^ 2 - Real.sin x ^ 2
                                            theorem Real.cos_sq (x : ) :
                                            Real.cos x ^ 2 = 1 / 2 + Real.cos (2 * x) / 2
                                            theorem Real.cos_sq' (x : ) :
                                            Real.cos x ^ 2 = 1 - Real.sin x ^ 2
                                            theorem Real.sin_sq (x : ) :
                                            Real.sin x ^ 2 = 1 - Real.cos x ^ 2
                                            theorem Real.sin_sq_eq_half_sub (x : ) :
                                            Real.sin x ^ 2 = 1 / 2 - Real.cos (2 * x) / 2
                                            theorem Real.inv_one_add_tan_sq {x : } (hx : Real.cos x 0) :
                                            (1 + Real.tan x ^ 2)⁻¹ = Real.cos x ^ 2
                                            theorem Real.tan_sq_div_one_add_tan_sq {x : } (hx : Real.cos x 0) :
                                            Real.tan x ^ 2 / (1 + Real.tan x ^ 2) = Real.sin x ^ 2
                                            theorem Real.cos_three_mul (x : ) :
                                            Real.cos (3 * x) = 4 * Real.cos x ^ 3 - 3 * Real.cos x
                                            theorem Real.sin_three_mul (x : ) :
                                            Real.sin (3 * x) = 3 * Real.sin x - 4 * Real.sin x ^ 3
                                            theorem Real.sinh_eq (x : ) :

                                            The definition of sinh in terms of exp.

                                            @[simp]
                                            @[simp]
                                            theorem Real.sinh_neg (x : ) :
                                            theorem Real.cosh_eq (x : ) :

                                            The definition of cosh in terms of exp.

                                            @[simp]
                                            @[simp]
                                            theorem Real.cosh_neg (x : ) :
                                            @[simp]
                                            theorem Real.cosh_abs (x : ) :
                                            @[simp]
                                            @[simp]
                                            theorem Real.tanh_neg (x : ) :
                                            @[simp]
                                            theorem Real.cosh_sq (x : ) :
                                            Real.cosh x ^ 2 = Real.sinh x ^ 2 + 1
                                            theorem Real.cosh_sq' (x : ) :
                                            Real.cosh x ^ 2 = 1 + Real.sinh x ^ 2
                                            theorem Real.sinh_sq (x : ) :
                                            Real.sinh x ^ 2 = Real.cosh x ^ 2 - 1
                                            theorem Real.cosh_three_mul (x : ) :
                                            Real.cosh (3 * x) = 4 * Real.cosh x ^ 3 - 3 * Real.cosh x
                                            theorem Real.sinh_three_mul (x : ) :
                                            Real.sinh (3 * x) = 4 * Real.sinh x ^ 3 + 3 * Real.sinh x
                                            theorem Real.sum_le_exp_of_nonneg {x : } (hx : 0 x) (n : ) :
                                            iFinset.range n, x ^ i / i.factorial Real.exp x
                                            theorem Real.pow_div_factorial_le_exp (x : ) (hx : 0 x) (n : ) :
                                            x ^ n / n.factorial Real.exp x
                                            theorem Real.quadratic_le_exp_of_nonneg {x : } (hx : 0 x) :
                                            1 + x + x ^ 2 / 2 Real.exp x
                                            theorem Real.one_le_exp {x : } (hx : 0 x) :
                                            theorem Real.exp_pos (x : ) :
                                            @[simp]
                                            theorem Real.abs_exp (x : ) :
                                            theorem Real.exp_lt_exp_of_lt {x : } {y : } (h : x < y) :
                                            theorem Real.exp_le_exp_of_le {x : } {y : } (h : x y) :
                                            @[simp]
                                            theorem Real.exp_lt_exp {x : } {y : } :
                                            @[simp]
                                            theorem Real.exp_le_exp {x : } {y : } :
                                            @[simp]
                                            theorem Real.exp_eq_exp {x : } {y : } :
                                            @[simp]
                                            theorem Real.exp_eq_one_iff (x : ) :
                                            Real.exp x = 1 x = 0
                                            @[simp]
                                            theorem Real.one_lt_exp_iff {x : } :
                                            1 < Real.exp x 0 < x
                                            @[simp]
                                            theorem Real.exp_lt_one_iff {x : } :
                                            Real.exp x < 1 x < 0
                                            @[simp]
                                            theorem Real.exp_le_one_iff {x : } :
                                            @[simp]
                                            theorem Real.one_le_exp_iff {x : } :
                                            theorem Real.cosh_pos (x : ) :

                                            Real.cosh is always positive

                                            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 (Complex.exp x - 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 (Complex.exp x - 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 (Complex.exp x - 1) 2 * Complex.abs x
                                            theorem Complex.abs_exp_sub_one_sub_id_le {x : } (hx : Complex.abs x 1) :
                                            Complex.abs (Complex.exp x - 1 - x) Complex.abs x ^ 2
                                            theorem Real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
                                            |Real.exp x - 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) :
                                            Real.exp x 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) :
                                            |Real.exp x - 1| 2 * |x|
                                            theorem Real.abs_exp_sub_one_sub_id_le {x : } (hx : |x| 1) :
                                            |Real.exp x - 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) :
                                              |Real.exp x - 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 : |Real.exp x - Real.expNear m x a₂| |x| ^ m / m.factorial * b₂) :
                                              |Real.exp x - 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)) :
                                              |Real.exp x - 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 : |Real.exp x - Real.expNear 0 x a| |x| ^ 0 / (Nat.factorial 0) * b) :
                                              |Real.exp x - a| b
                                              theorem Real.cos_bound {x : } (hx : |x| 1) :
                                              |Real.cos x - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
                                              theorem Real.sin_bound {x : } (hx : |x| 1) :
                                              |Real.sin x - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
                                              theorem Real.cos_pos_of_le_one {x : } (hx : |x| 1) :
                                              theorem Real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
                                              theorem Real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
                                              theorem Real.exp_bound_div_one_sub_of_interval' {x : } (h1 : 0 < x) (h2 : x < 1) :
                                              Real.exp x < 1 / (1 - x)
                                              theorem Real.exp_bound_div_one_sub_of_interval {x : } (h1 : 0 x) (h2 : x < 1) :
                                              Real.exp x 1 / (1 - x)
                                              theorem Real.add_one_lt_exp {x : } (hx : x 0) :
                                              x + 1 < Real.exp x
                                              theorem Real.one_sub_lt_exp_neg {x : } (hx : x 0) :
                                              1 - x < Real.exp (-x)
                                              theorem Real.one_sub_div_pow_le_exp_neg {n : } {t : } (ht' : t n) :
                                              (1 - t / n) ^ n Real.exp (-t)

                                              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 (Complex.cos x + Complex.sin x * Complex.I) = 1
                                                  @[simp]
                                                  theorem Complex.abs_exp_ofReal (x : ) :
                                                  Complex.abs (Complex.exp x) = Real.exp x
                                                  @[simp]
                                                  theorem Complex.abs_exp_ofReal_mul_I (x : ) :
                                                  Complex.abs (Complex.exp (x * Complex.I)) = 1
                                                  theorem Complex.abs_exp (z : ) :
                                                  Complex.abs (Complex.exp z) = Real.exp z.re
                                                  theorem Complex.abs_exp_eq_iff_re_eq {x : } {y : } :
                                                  Complex.abs (Complex.exp x) = Complex.abs (Complex.exp y) x.re = y.re