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 isCauSeq_of_decreasing_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : α) {a : α} {m : } (ham : nm, |f n| a) (hnm : nm, f (Nat.succ n) f n) :
IsCauSeq abs f
theorem isCauSeq_of_mono_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : α) {a : α} {m : } (ham : nm, |f n| a) (hnm : nm, f n f (Nat.succ n)) :
IsCauSeq abs f
theorem isCauSeq_series_of_abv_le_of_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] [LinearOrderedField α] {abv : βα} [IsAbsoluteValue abv] {f : β} {g : α} (n : ) :
(∀ (m : ), n mabv (f m) g m)(IsCauSeq abs fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => g i)IsCauSeq abv fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => f i
theorem isCauSeq_series_of_abv_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] [LinearOrderedField α] {abv : βα} [IsAbsoluteValue abv] {f : β} :
(IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => abv (f n))IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => f n
theorem isCauSeq_geo_series {α : Type u_1} [LinearOrderedField α] [Archimedean α] {β : Type u_2} [Ring β] [Nontrivial β] {abv : βα} [IsAbsoluteValue abv] (x : β) (hx1 : abv x < 1) :
IsCauSeq abv fun (n : ) => Finset.sum (Finset.range n) fun (m : ) => x ^ m
theorem isCauSeq_geo_series_const {α : Type u_1} [LinearOrderedField α] [Archimedean α] (a : α) {x : α} (hx1 : |x| < 1) :
IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => a * x ^ n
theorem series_ratio_test {α : Type u_1} [LinearOrderedField α] [Archimedean α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (n : ) (r : α) (hr0 : 0 r) (hr1 : r < 1) (h : ∀ (m : ), n mabv (f (Nat.succ m)) r * abv (f m)) :
IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => f n
theorem sum_range_diag_flip {α : Type u_3} [AddCommMonoid α] (n : ) (f : α) :
(Finset.sum (Finset.range n) fun (m : ) => Finset.sum (Finset.range (m + 1)) fun (k : ) => f k (m - k)) = Finset.sum (Finset.range n) fun (m : ) => Finset.sum (Finset.range (n - m)) fun (k : ) => f m k
theorem abv_sum_le_sum_abv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {abv : βα} [Semiring β] [IsAbsoluteValue abv] {γ : Type u_3} (f : γβ) (s : Finset γ) :
abv (Finset.sum s fun (k : γ) => f k) Finset.sum s fun (k : γ) => abv (f k)
theorem cauchy_product {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {abv : βα} [Ring β] [IsAbsoluteValue abv] {a : β} {b : β} (ha : IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => abv (a n)) (hb : IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => b n) (ε : α) (ε0 : 0 < ε) :
∃ (i : ), ji, abv (((Finset.sum (Finset.range j) fun (k : ) => a k) * Finset.sum (Finset.range j) fun (k : ) => b k) - Finset.sum (Finset.range j) fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (m : ) => a m * b (n - m)) < ε
theorem Complex.isCauSeq_abs_exp (z : ) :
IsCauSeq abs fun (n : ) => Finset.sum (Finset.range n) fun (m : ) => Complex.abs (z ^ m / (Nat.factorial m))
theorem Complex.isCauSeq_exp (z : ) :
IsCauSeq Complex.abs fun (n : ) => Finset.sum (Finset.range n) fun (m : ) => z ^ m / (Nat.factorial m)

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

Equations
  • One or more equations did not get rendered due to their size.
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.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.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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Complex.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                      Complex.exp (Finset.sum s fun (x : α) => f x) = Finset.prod s fun (x : α) => 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
                                      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.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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Real.exp_sum {α : Type u_1} (s : Finset α) (f : α) :
                                        Real.exp (Finset.sum s fun (x : α) => f x) = Finset.prod s fun (x : α) => 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
                                        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 : ) :
                                        (Finset.sum (Finset.range n) fun (i : ) => x ^ i / (Nat.factorial i)) Real.exp x
                                        theorem Real.pow_div_factorial_le_exp (x : ) (hx : 0 x) (n : ) :
                                        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) :
                                        (Finset.sum (Finset.filter (fun (k : ) => n k) (Finset.range j)) fun (m : ) => 1 / (Nat.factorial m)) (Nat.succ n) / ((Nat.factorial n) * n)
                                        theorem Complex.exp_bound {x : } (hx : Complex.abs x 1) {n : } (hn : 0 < n) :
                                        Complex.abs (Complex.exp x - Finset.sum (Finset.range n) fun (m : ) => x ^ m / (Nat.factorial m)) Complex.abs x ^ n * ((Nat.succ n) * ((Nat.factorial n) * n)⁻¹)
                                        theorem Complex.exp_bound' {x : } {n : } (hx : Complex.abs x / (Nat.succ n) 1 / 2) :
                                        theorem Real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
                                        |Real.exp x - Finset.sum (Finset.range n) fun (m : ) => x ^ m / (Nat.factorial m)| |x| ^ n * ((Nat.succ n) / ((Nat.factorial n) * n))
                                        theorem Real.exp_bound' {x : } (h1 : 0 x) (h2 : x 1) {n : } (hn : 0 < n) :
                                        Real.exp x (Finset.sum (Finset.range n) fun (m : ) => x ^ m / (Nat.factorial m)) + x ^ n * (n + 1) / ((Nat.factorial n) * 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 / (Nat.factorial n) * (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 / (Nat.factorial m) * ((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 / (Nat.factorial m) * b₂) :
                                          |Real.exp x - Real.expNear n x a₁| |x| ^ n / (Nat.factorial n) * 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 / (Nat.factorial n) * 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 / (Nat.factorial m) * (b₁ * rm)) :
                                          |Real.exp 1 - Real.expNear n 1 a₁| |1| ^ n / (Nat.factorial n) * 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.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

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

                                            Instances For