# 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} [] (f : α) {a : α} {m : } (ham : ∀ (n : ), n m|f n| a) (hnm : ∀ (n : ), n mf () f n) :
IsCauSeq abs f
theorem isCauSeq_of_mono_bounded {α : Type u_1} [] (f : α) {a : α} {m : } (ham : ∀ (n : ), n m|f n| a) (hnm : ∀ (n : ), n mf n f ()) :
IsCauSeq abs f
theorem isCauSeq_series_of_abv_le_of_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {f : β} {g : α} (n : ) :
(∀ (m : ), n mabv (f m) g m) → (IsCauSeq abs fun n => Finset.sum () fun i => g i) → IsCauSeq abv fun n => Finset.sum () fun i => f i
theorem isCauSeq_series_of_abv_isCauSeq {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {f : β} :
(IsCauSeq abs fun m => Finset.sum () fun n => abv (f n)) → IsCauSeq abv fun m => Finset.sum () fun n => f n
theorem isCauSeq_geo_series {α : Type u_1} [] {β : Type u_2} [Ring β] [] {abv : βα} [] (x : β) (hx1 : abv x < 1) :
IsCauSeq abv fun n => Finset.sum () fun m => x ^ m
theorem isCauSeq_geo_series_const {α : Type u_1} [] (a : α) {x : α} (hx1 : |x| < 1) :
IsCauSeq abs fun m => Finset.sum () fun n => a * x ^ n
theorem series_ratio_test {α : Type u_1} [] {β : Type u_2} [Ring β] {abv : βα} [] {f : β} (n : ) (r : α) (hr0 : 0 r) (hr1 : r < 1) (h : ∀ (m : ), n mabv (f ()) r * abv (f m)) :
IsCauSeq abv fun m => Finset.sum () fun n => f n
theorem sum_range_diag_flip {α : Type u_3} [] (n : ) (f : α) :
(Finset.sum () fun m => Finset.sum (Finset.range (m + 1)) fun k => f k (m - k)) = Finset.sum () 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} {abv : βα} [] [] {γ : Type u_3} (f : γβ) (s : ) :
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} {abv : βα} [Ring β] [] {a : β} {b : β} (ha : IsCauSeq abs fun m => Finset.sum () fun n => abv (a n)) (hb : IsCauSeq abv fun m => Finset.sum () fun n => b n) (ε : α) (ε0 : 0 < ε) :
i, ∀ (j : ), j iabv (((Finset.sum () fun k => a k) * Finset.sum () fun k => b k) - Finset.sum () 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 () fun m => Complex.abs (z ^ m / ↑())
theorem Complex.isCauSeq_exp (z : ) :
IsCauSeq fun n => Finset.sum () fun m => z ^ m / ↑()
def Complex.exp' (z : ) :

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

Instances For
def Complex.exp (z : ) :

The complex exponential function, defined via its Taylor series

Instances For
def Complex.sin (z : ) :

The complex sine function, defined via exp

Instances For
def Complex.cos (z : ) :

The complex cosine function, defined via exp

Instances For
def Complex.tan (z : ) :

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

Instances For
def Complex.sinh (z : ) :

The complex hyperbolic sine function, defined via exp

Instances For
def Complex.cosh (z : ) :

The complex hyperbolic cosine function, defined via exp

Instances For
def Complex.tanh (z : ) :

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

Instances For

scoped notation for the complex exponential function

Instances For
def Real.exp (x : ) :

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

Instances For
def Real.sin (x : ) :

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

Instances For
def Real.cos (x : ) :

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

Instances For
def Real.tan (x : ) :

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

Instances For
def Real.sinh (x : ) :

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

Instances For
def Real.cosh (x : ) :

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

Instances For
def Real.tanh (x : ) :

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

Instances For

scoped notation for the real exponential function

Instances For
@[simp]
theorem Complex.exp_zero :
= 1
theorem Complex.exp_add (x : ) (y : ) :
Complex.exp (x + y) =
noncomputable def Complex.expMonoidHom :

the exponential function as a monoid hom from Multiplicative ℂ to ℂ

Instances For
theorem Complex.exp_sum {α : Type u_1} (s : ) (f : α) :
Complex.exp (Finset.sum s fun x => f x) = Finset.prod s fun x => Complex.exp (f x)
theorem Complex.exp_nat_mul (x : ) (n : ) :
Complex.exp (n * x) = ^ n
theorem Complex.exp_sub (x : ) (y : ) :
Complex.exp (x - y) =
theorem Complex.exp_int_mul (z : ) (n : ) :
Complex.exp (n * z) = ^ n
@[simp]
theorem Complex.exp_conj (x : ) :
Complex.exp (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_exp_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_exp (x : ) :
↑() =
@[simp]
theorem Complex.exp_ofReal_im (x : ) :
().im = 0
theorem Complex.exp_ofReal_re (x : ) :
().re =
@[simp]
@[simp]
theorem Complex.sinh_neg (x : ) :
theorem Complex.sinh_add (x : ) (y : ) :
@[simp]
@[simp]
theorem Complex.cosh_neg (x : ) :
theorem Complex.cosh_add (x : ) (y : ) :
theorem Complex.sinh_sub (x : ) (y : ) :
theorem Complex.cosh_sub (x : ) (y : ) :
theorem Complex.sinh_conj (x : ) :
Complex.sinh (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_sinh_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_sinh (x : ) :
↑() =
@[simp]
theorem Complex.sinh_ofReal_im (x : ) :
().im = 0
theorem Complex.sinh_ofReal_re (x : ) :
().re =
theorem Complex.cosh_conj (x : ) :
Complex.cosh (↑() x) = ↑() ()
theorem Complex.ofReal_cosh_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_cosh (x : ) :
↑() =
@[simp]
theorem Complex.cosh_ofReal_im (x : ) :
().im = 0
@[simp]
theorem Complex.cosh_ofReal_re (x : ) :
().re =
@[simp]
@[simp]
theorem Complex.tanh_neg (x : ) :
theorem Complex.tanh_conj (x : ) :
Complex.tanh (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_tanh_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_tanh (x : ) :
↑() =
@[simp]
theorem Complex.tanh_ofReal_im (x : ) :
().im = 0
theorem Complex.tanh_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.cosh_add_sinh (x : ) :
@[simp]
theorem Complex.sinh_add_cosh (x : ) :
@[simp]
theorem Complex.exp_sub_cosh (x : ) :
@[simp]
theorem Complex.exp_sub_sinh (x : ) :
@[simp]
@[simp]
@[simp]
theorem Complex.cosh_sq (x : ) :
= + 1
theorem Complex.sinh_sq (x : ) :
= - 1
@[simp]
theorem Complex.sin_zero :
= 0
@[simp]
theorem Complex.sin_neg (x : ) :
theorem Complex.two_sin (x : ) :
2 * = ( - ) * Complex.I
theorem Complex.two_cos (x : ) :
2 * = +
theorem Complex.sin_add (x : ) (y : ) :
Complex.sin (x + y) = +
@[simp]
theorem Complex.cos_zero :
= 1
@[simp]
theorem Complex.cos_neg (x : ) :
theorem Complex.cos_add (x : ) (y : ) :
Complex.cos (x + y) = -
theorem Complex.sin_sub (x : ) (y : ) :
Complex.sin (x - y) = -
theorem Complex.cos_sub (x : ) (y : ) :
Complex.cos (x - y) = +
theorem Complex.sin_add_mul_I (x : ) (y : ) :
theorem Complex.sin_eq (z : ) :
= Complex.sin z.re * Complex.cosh z.im + Complex.cos z.re * Complex.sinh z.im * Complex.I
theorem Complex.cos_add_mul_I (x : ) (y : ) :
theorem Complex.cos_eq (z : ) :
= Complex.cos z.re * Complex.cosh z.im - Complex.sin z.re * Complex.sinh z.im * Complex.I
theorem Complex.sin_sub_sin (x : ) (y : ) :
= 2 * Complex.sin ((x - y) / 2) * Complex.cos ((x + y) / 2)
theorem Complex.cos_sub_cos (x : ) (y : ) :
= -2 * Complex.sin ((x + y) / 2) * Complex.sin ((x - y) / 2)
theorem Complex.cos_add_cos (x : ) (y : ) :
= 2 * Complex.cos ((x + y) / 2) * Complex.cos ((x - y) / 2)
theorem Complex.sin_conj (x : ) :
Complex.sin (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_sin_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_sin (x : ) :
↑() =
@[simp]
theorem Complex.sin_ofReal_im (x : ) :
().im = 0
theorem Complex.sin_ofReal_re (x : ) :
().re =
theorem Complex.cos_conj (x : ) :
Complex.cos (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_cos_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_cos (x : ) :
↑() =
@[simp]
theorem Complex.cos_ofReal_im (x : ) :
().im = 0
theorem Complex.cos_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.tan_zero :
= 0
theorem Complex.tan_mul_cos {x : } (hx : 0) :
@[simp]
theorem Complex.tan_neg (x : ) :
theorem Complex.tan_conj (x : ) :
Complex.tan (↑() x) = ↑() ()
@[simp]
theorem Complex.ofReal_tan_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.ofReal_tan (x : ) :
↑() =
@[simp]
theorem Complex.tan_ofReal_im (x : ) :
().im = 0
theorem Complex.tan_ofReal_re (x : ) :
().re =
@[simp]
theorem Complex.sin_sq_add_cos_sq (x : ) :
^ 2 + ^ 2 = 1
@[simp]
theorem Complex.cos_sq_add_sin_sq (x : ) :
^ 2 + ^ 2 = 1
theorem Complex.cos_two_mul' (x : ) :
Complex.cos (2 * x) = ^ 2 - ^ 2
theorem Complex.cos_two_mul (x : ) :
Complex.cos (2 * x) = 2 * ^ 2 - 1
theorem Complex.sin_two_mul (x : ) :
Complex.sin (2 * x) = 2 * *
theorem Complex.cos_sq (x : ) :
^ 2 = 1 / 2 + Complex.cos (2 * x) / 2
theorem Complex.cos_sq' (x : ) :
^ 2 = 1 - ^ 2
theorem Complex.sin_sq (x : ) :
^ 2 = 1 - ^ 2
theorem Complex.inv_one_add_tan_sq {x : } (hx : 0) :
(1 + ^ 2)⁻¹ = ^ 2
theorem Complex.tan_sq_div_one_add_tan_sq {x : } (hx : 0) :
^ 2 / (1 + ^ 2) = ^ 2
theorem Complex.cos_three_mul (x : ) :
Complex.cos (3 * x) = 4 * ^ 3 - 3 *
theorem Complex.sin_three_mul (x : ) :
Complex.sin (3 * x) = 3 * - 4 * ^ 3
theorem Complex.exp_mul_I (x : ) :
=
theorem Complex.exp_add_mul_I (x : ) (y : ) :
Complex.exp (x + ) = * ()
theorem Complex.exp_re (x : ) :
().re = Real.exp x.re * Real.cos x.im
theorem Complex.exp_im (x : ) :
().im = Real.exp x.re * Real.sin x.im
@[simp]
@[simp]
theorem Complex.cos_add_sin_mul_I_pow (n : ) (z : ) :
() ^ n = Complex.cos (n * z) + Complex.sin (n * z) * Complex.I

De Moivre's formula

@[simp]
theorem Real.exp_zero :
= 1
theorem Real.exp_add (x : ) (y : ) :
Real.exp (x + y) =
noncomputable def Real.expMonoidHom :

the exponential function as a monoid hom from Multiplicative ℝ to ℝ

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

The definition of sinh in terms of exp.

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

The definition of cosh in terms of exp.

@[simp]
theorem Real.cosh_zero :
= 1
@[simp]
theorem Real.cosh_neg (x : ) :
@[simp]
theorem Real.cosh_abs (x : ) :
theorem Real.cosh_add (x : ) (y : ) :
Real.cosh (x + y) = +
theorem Real.sinh_sub (x : ) (y : ) :
Real.sinh (x - y) = -
theorem Real.cosh_sub (x : ) (y : ) :
Real.cosh (x - y) = -
@[simp]
theorem Real.tanh_zero :
= 0
@[simp]
theorem Real.tanh_neg (x : ) :
@[simp]
theorem Real.cosh_add_sinh (x : ) :
=
@[simp]
theorem Real.sinh_add_cosh (x : ) :
=
@[simp]
theorem Real.exp_sub_cosh (x : ) :
=
@[simp]
theorem Real.exp_sub_sinh (x : ) :
=
@[simp]
theorem Real.cosh_sub_sinh (x : ) :
@[simp]
theorem Real.sinh_sub_cosh (x : ) :
@[simp]
theorem Real.cosh_sq_sub_sinh_sq (x : ) :
^ 2 - ^ 2 = 1
theorem Real.cosh_sq (x : ) :
^ 2 = ^ 2 + 1
theorem Real.cosh_sq' (x : ) :
^ 2 = 1 + ^ 2
theorem Real.sinh_sq (x : ) :
^ 2 = ^ 2 - 1
theorem Real.cosh_two_mul (x : ) :
Real.cosh (2 * x) = ^ 2 + ^ 2
theorem Real.sinh_two_mul (x : ) :
Real.sinh (2 * x) = 2 * *
theorem Real.cosh_three_mul (x : ) :
Real.cosh (3 * x) = 4 * ^ 3 - 3 *
theorem Real.sinh_three_mul (x : ) :
Real.sinh (3 * x) = 4 * ^ 3 + 3 *
theorem Real.sum_le_exp_of_nonneg {x : } (hx : 0 x) (n : ) :
(Finset.sum () fun i => x ^ i / ↑())
theorem Real.quadratic_le_exp_of_nonneg {x : } (hx : 0 x) :
1 + x + x ^ 2 / 2
theorem Real.add_one_lt_exp_of_pos {x : } (hx : 0 < x) :
x + 1 <
theorem Real.add_one_le_exp_of_nonneg {x : } (hx : 0 x) :
x + 1

This is an intermediate result that is later replaced by Real.add_one_le_exp; use that lemma instead.

theorem Real.one_le_exp {x : } (hx : 0 x) :
1
theorem Real.exp_pos (x : ) :
0 <
@[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 : } :
x < y
@[simp]
theorem Real.exp_le_exp {x : } {y : } :
x y
@[simp]
theorem Real.exp_eq_exp {x : } {y : } :
x = y
@[simp]
theorem Real.exp_eq_one_iff (x : ) :
= 1 x = 0
@[simp]
theorem Real.one_lt_exp_iff {x : } :
1 < 0 < x
@[simp]
theorem Real.exp_lt_one_iff {x : } :
< 1 x < 0
@[simp]
theorem Real.exp_le_one_iff {x : } :
1 x 0
@[simp]
theorem Real.one_le_exp_iff {x : } :
1 0 x
theorem Real.cosh_pos (x : ) :
0 <

Real.cosh is always positive

theorem Complex.sum_div_factorial_le {α : Type u_1} (n : ) (j : ) (hn : 0 < n) :
(Finset.sum (Finset.filter (fun k => n k) ()) fun m => 1 / ↑()) ↑() / (↑() * n)
theorem Complex.exp_bound {x : } (hx : 1) {n : } (hn : 0 < n) :
Complex.abs ( - Finset.sum () fun m => x ^ m / ↑()) ^ n * (↑() * (↑() * n)⁻¹)
theorem Complex.exp_bound' {x : } {n : } (hx : / ↑() 1 / 2) :
Complex.abs ( - Finset.sum () fun m => x ^ m / ↑()) ^ n / ↑() * 2
theorem Complex.abs_exp_sub_one_le {x : } (hx : 1) :
Complex.abs ( - 1) 2 *
theorem Complex.abs_exp_sub_one_sub_id_le {x : } (hx : 1) :
Complex.abs ( - 1 - x) ^ 2
theorem Real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
| - Finset.sum () fun m => x ^ m / ↑()| |x| ^ n * (↑() / (↑() * n))
theorem Real.exp_bound' {x : } (h1 : 0 x) (h2 : x 1) {n : } (hn : 0 < n) :
(Finset.sum () fun m => x ^ m / ↑()) + x ^ n * (n + 1) / (↑() * n)
theorem Real.abs_exp_sub_one_le {x : } (hx : |x| 1) :
| - 1| 2 * |x|
theorem Real.abs_exp_sub_one_sub_id_le {x : } (hx : |x| 1) :
| - 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.

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 / ↑() * (r₁ - r₂)
theorem Real.exp_approx_end (n : ) (m : ) (x : ) (e₁ : n + 1 = m) (h : |x| 1) :
| - Real.expNear m x 0| |x| ^ 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.expNear m x a₂| |x| ^ m / ↑() * b₂) :
| - Real.expNear n x a₁| |x| ^ 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.expNear n x a| |x| ^ n / ↑() * b
theorem Real.exp_1_approx_succ_eq {n : } {a₁ : } {b₁ : } {m : } (en : n + 1 = m) {rm : } (er : m = rm) (h : | - Real.expNear m 1 ((a₁ - 1) * rm)| |1| ^ m / ↑() * (b₁ * rm)) :
| - Real.expNear n 1 a₁| |1| ^ n / ↑() * b₁
theorem Real.exp_approx_start (x : ) (a : ) (b : ) (h : | - Real.expNear 0 x a| |x| ^ 0 / ↑() * b) :
| - a| b
theorem Real.cos_bound {x : } (hx : |x| 1) :
| - (1 - x ^ 2 / 2)| |x| ^ 4 * (5 / 96)
theorem Real.sin_bound {x : } (hx : |x| 1) :
| - (x - x ^ 3 / 6)| |x| ^ 4 * (5 / 96)
theorem Real.cos_pos_of_le_one {x : } (hx : |x| 1) :
0 <
theorem Real.sin_pos_of_pos_of_le_one {x : } (hx0 : 0 < x) (hx : x 1) :
0 <
theorem Real.sin_pos_of_pos_of_le_two {x : } (hx0 : 0 < x) (hx : x 2) :
0 <
theorem Real.exp_bound_div_one_sub_of_interval' {x : } (h1 : 0 < x) (h2 : x < 1) :
< 1 / (1 - x)
theorem Real.exp_bound_div_one_sub_of_interval {x : } (h1 : 0 x) (h2 : x < 1) :
1 / (1 - x)
theorem Real.one_sub_lt_exp_minus_of_pos {y : } (h : 0 < y) :
1 - y < Real.exp (-y)
theorem Real.add_one_lt_exp_of_neg {x : } (h : x < 0) :
x + 1 <
theorem Real.add_one_lt_exp_of_nonzero {x : } (hx : x 0) :
x + 1 <
theorem Real.add_one_le_exp (x : ) :
x + 1
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
@[simp]
@[simp]
theorem Complex.abs_exp_ofReal (x : ) :
Complex.abs () =
theorem Complex.abs_exp (z : ) :
= Real.exp z.re
theorem Complex.abs_exp_eq_iff_re_eq {x : } {y : } :
= x.re = y.re