# 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 : ) => m, Complex.abs (z ^ m / m.factorial)
theorem Complex.isCauSeq_exp (z : ) :
IsCauSeq fun (n : ) => m, z ^ m / m.factorial
def Complex.exp' (z : ) :

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

Equations
• = fun (n : ) => m ∈ , z ^ m / m.factorial,
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
• z.cot =
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]
theorem Complex.exp_zero :
= 1
theorem Complex.exp_add (x : ) (y : ) :
Complex.exp (x + y) =
@[simp]
theorem Complex.expMonoidHom_apply (z : ) :
Complex.expMonoidHom z = Complex.exp (Multiplicative.toAdd z)
noncomputable def Complex.expMonoidHom :

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

Equations
Instances For
theorem Complex.exp_list_sum (l : ) :
Complex.exp l.sum = .prod
theorem Complex.exp_multiset_sum (s : ) :
Complex.exp s.sum = .prod
theorem Complex.exp_sum {α : Type u_1} (s : ) (f : α) :
Complex.exp (∑ xs, f x) = xs, Complex.exp (f x)
theorem Complex.exp_nsmul (x : ) (n : ) :
Complex.exp (n x) = ^ n
theorem Complex.exp_nat_mul (x : ) (n : ) :
Complex.exp (n * x) = ^ n
@[simp]
theorem Complex.exp_ne_zero (x : ) :
0
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 : ) :
@[simp]
theorem Complex.ofReal_exp_ofReal_re (x : ) :
(Complex.exp x).re =
@[simp]
theorem Complex.ofReal_exp (x : ) :
(Real.exp x) =
@[simp]
theorem Complex.exp_ofReal_im (x : ) :
(Complex.exp x).im = 0
theorem Complex.exp_ofReal_re (x : ) :
(Complex.exp 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 : ) :
@[simp]
theorem Complex.ofReal_sinh_ofReal_re (x : ) :
(Complex.sinh x).re =
@[simp]
theorem Complex.ofReal_sinh (x : ) :
(Real.sinh x) =
@[simp]
theorem Complex.sinh_ofReal_im (x : ) :
(Complex.sinh x).im = 0
@[simp]
theorem Complex.ofReal_cosh (x : ) :
(Real.cosh x) =
@[simp]
theorem Complex.cosh_ofReal_im (x : ) :
(Complex.cosh x).im = 0
@[simp]
theorem Complex.cosh_ofReal_re (x : ) :
(Complex.cosh x).re =
@[simp]
@[simp]
theorem Complex.tanh_neg (x : ) :
@[simp]
theorem Complex.ofReal_tanh_ofReal_re (x : ) :
(Complex.tanh x).re =
@[simp]
theorem Complex.ofReal_tanh (x : ) :
(Real.tanh x) =
@[simp]
theorem Complex.tanh_ofReal_im (x : ) :
(Complex.tanh x).im = 0
@[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.sin_add_sin (x : ) (y : ) :
= 2 * Complex.sin ((x + y) / 2) * Complex.cos ((x - y) / 2)
theorem Complex.cos_add_cos (x : ) (y : ) :
= 2 * Complex.cos ((x + y) / 2) * Complex.cos ((x - y) / 2)
@[simp]
theorem Complex.ofReal_sin_ofReal_re (x : ) :
(Complex.sin x).re =
@[simp]
theorem Complex.ofReal_sin (x : ) :
(Real.sin x) =
@[simp]
theorem Complex.sin_ofReal_im (x : ) :
(Complex.sin x).im = 0
theorem Complex.sin_ofReal_re (x : ) :
(Complex.sin x).re =
@[simp]
theorem Complex.ofReal_cos_ofReal_re (x : ) :
(Complex.cos x).re =
@[simp]
theorem Complex.ofReal_cos (x : ) :
(Real.cos x) =
@[simp]
theorem Complex.cos_ofReal_im (x : ) :
(Complex.cos x).im = 0
theorem Complex.cos_ofReal_re (x : ) :
(Complex.cos x).re =
@[simp]
theorem Complex.tan_zero :
= 0
theorem Complex.cot_eq_cos_div_sin (x : ) :
x.cot =
theorem Complex.tan_mul_cos {x : } (hx : 0) :
@[simp]
theorem Complex.tan_neg (x : ) :
theorem Complex.cot_conj (x : ) :
( x).cot = x.cot
@[simp]
theorem Complex.ofReal_tan_ofReal_re (x : ) :
(Complex.tan x).re =
@[simp]
theorem Complex.ofReal_cot_ofReal_re (x : ) :
(↑x).cot.re = (↑x).cot
@[simp]
theorem Complex.ofReal_tan (x : ) :
(Real.tan x) =
@[simp]
theorem Complex.ofReal_cot (x : ) :
x.cot = (↑x).cot
@[simp]
theorem Complex.tan_ofReal_im (x : ) :
(Complex.tan x).im = 0
theorem Complex.tan_ofReal_re (x : ) :
(Complex.tan 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 : ) :
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
@[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) =
@[simp]
theorem Real.expMonoidHom_apply (x : ) :
Real.expMonoidHom x = Real.exp (Multiplicative.toAdd x)
noncomputable def Real.expMonoidHom :

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

Equations
Instances For
theorem Real.exp_list_sum (l : ) :
Real.exp l.sum = .prod
theorem Real.exp_multiset_sum (s : ) :
Real.exp s.sum = .prod
theorem Real.exp_sum {α : Type u_1} (s : ) (f : α) :
Real.exp (∑ xs, f x) = xs, Real.exp (f x)
theorem Real.exp_nsmul (x : ) (n : ) :
Real.exp (n x) = ^ n
theorem Real.exp_nat_mul (x : ) (n : ) :
Real.exp (n * x) = ^ n
@[simp]
theorem Real.exp_ne_zero (x : ) :
0
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.cot_eq_cos_div_sin (x : ) :
x.cot =
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.neg_one_le_sin (x : ) :
-1
theorem Real.neg_one_le_cos (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.sin_sq_eq_half_sub (x : ) :
^ 2 = 1 / 2 - Real.cos (2 * x) / 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 < ) :
((1 + ^ 2))⁻¹ =
theorem Real.tan_div_sqrt_one_add_tan_sq {x : } (hx : 0 < ) :
/ (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 : ) :
i, x ^ i / i.factorial
theorem Real.pow_div_factorial_le_exp (x : ) (hx : 0 x) (n : ) :
x ^ n / n.factorial
theorem Real.quadratic_le_exp_of_nonneg {x : } (hx : 0 x) :
1 + x + x ^ 2 / 2
theorem Real.one_le_exp {x : } (hx : 0 x) :
1
theorem Real.exp_pos (x : ) :
0 <
theorem Real.exp_nonneg (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) :
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 ( - m, 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 ( - m, 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 ( - 1) 2 * Complex.abs x
theorem Complex.abs_exp_sub_one_sub_id_le {x : } (hx : Complex.abs x 1) :
Complex.abs ( - 1 - x) Complex.abs x ^ 2
theorem Real.exp_bound {x : } (hx : |x| 1) {n : } (hn : 0 < n) :
| - m, 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) :
m, x ^ m / m.factorial + x ^ n * (n + 1) / (n.factorial * 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.

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.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.expNear m x a₂| |x| ^ m / m.factorial * b₂) :
| - 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.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.expNear m 1 ((a₁ - 1) * rm)| |1| ^ m / m.factorial * (b₁ * rm)) :
| - Real.expNear n 1 a₁| |1| ^ n / n.factorial * 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.cos_one_le :
2 / 3
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.add_one_lt_exp {x : } (hx : x 0) :
x + 1 <
theorem Real.add_one_le_exp (x : ) :
x + 1
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 ( + ) = 1
@[simp]
theorem Complex.abs_exp_ofReal (x : ) :
Complex.abs (Complex.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