# mathlibdocumentation

analysis.special_functions.exp

# Complex and real exponential #

In this file we prove continuity of complex.exp and real.exp. We also prove a few facts about limits of real.exp at infinity.

## Tags #

exp

theorem complex.exp_bound_sq (x z : ) (hz : z 1) :
theorem complex.locally_lipschitz_exp {r : } (hr_nonneg : 0 r) (hr_le : r 1) (x y : ) (hyx : y - x < r) :
(1 + r) * * y - x
@[continuity]
theorem filter.tendsto.cexp {α : Type u_1} {l : filter α} {f : α → } {z : } (hf : (nhds z)) :
filter.tendsto (λ (x : α), complex.exp (f x)) l (nhds (complex.exp z))
theorem continuous_within_at.cexp {α : Type u_1} {f : α → } {s : set α} {x : α} (h : x) :
continuous_within_at (λ (y : α), complex.exp (f y)) s x
theorem continuous_at.cexp {α : Type u_1} {f : α → } {x : α} (h : x) :
continuous_at (λ (y : α), complex.exp (f y)) x
theorem continuous_on.cexp {α : Type u_1} {f : α → } {s : set α} (h : s) :
continuous_on (λ (y : α), complex.exp (f y)) s
theorem continuous.cexp {α : Type u_1} {f : α → } (h : continuous f) :
continuous (λ (y : α), complex.exp (f y))
@[continuity]
theorem filter.tendsto.exp {α : Type u_1} {l : filter α} {f : α → } {z : } (hf : (nhds z)) :
filter.tendsto (λ (x : α), real.exp (f x)) l (nhds (real.exp z))
theorem continuous_within_at.exp {α : Type u_1} {f : α → } {s : set α} {x : α} (h : x) :
continuous_within_at (λ (y : α), real.exp (f y)) s x
theorem continuous_at.exp {α : Type u_1} {f : α → } {x : α} (h : x) :
continuous_at (λ (y : α), real.exp (f y)) x
theorem continuous_on.exp {α : Type u_1} {f : α → } {s : set α} (h : s) :
continuous_on (λ (y : α), real.exp (f y)) s
theorem continuous.exp {α : Type u_1} {f : α → } (h : continuous f) :
continuous (λ (y : α), real.exp (f y))
theorem real.exp_half (x : ) :
real.exp (x / 2) =

The real exponential function tends to +∞ at +∞.

The real exponential function tends to 0 at -∞ or, equivalently, exp(-x) tends to 0 at +∞

The real exponential function tends to 1 at 0.

@[simp]
theorem real.is_bounded_under_ge_exp_comp {α : Type u_1} (l : filter α) (f : α → ) :
(λ (x : α), real.exp (f x))
@[simp]
theorem real.is_bounded_under_le_exp_comp {α : Type u_1} {l : filter α} {f : α → } :
(λ (x : α), real.exp (f x))

The function exp(x)/x^n tends to +∞ at +∞, for any natural number n

The function x^n * exp(-x) tends to 0 at +∞, for any natural number n.

theorem real.tendsto_mul_exp_add_div_pow_at_top (b c : ) (n : ) (hb : 0 < b) :

The function (b * exp x + c) / (x ^ n) tends to +∞ at +∞, for any natural number n and any real numbers b and c such that b is positive.

theorem real.tendsto_div_pow_mul_exp_add_at_top (b c : ) (n : ) (hb : 0 b) :
filter.tendsto (λ (x : ), x ^ n / (b * + c)) filter.at_top (nhds 0)

The function (x ^ n) / (b * exp x + c) tends to 0 at +∞, for any natural number n and any real numbers b and c such that b is nonzero.

noncomputable def real.exp_order_iso  :

real.exp as an order isomorphism between ℝ and (0, +∞).

Equations
@[simp]
@[simp]
@[simp]
theorem real.range_exp  :
@[simp]
@[simp]
@[simp]
theorem real.tendsto_exp_comp_at_top {α : Type u_1} {l : filter α} {f : α → } :
filter.tendsto (λ (x : α), real.exp (f x)) l filter.at_top
theorem real.tendsto_comp_exp_at_top {α : Type u_1} {l : filter α} {f : → α} :
@[simp]
theorem real.map_exp_at_bot  :
@[simp]
theorem real.tendsto_comp_exp_at_bot {α : Type u_1} {l : filter α} {f : → α} :
filter.tendsto (λ (x : ), f (real.exp x)) filter.at_bot l (set.Ioi 0)) l
@[simp]
@[simp]
theorem real.tendsto_exp_comp_nhds_zero {α : Type u_1} {l : filter α} {f : α → } :
filter.tendsto (λ (x : α), real.exp (f x)) l (nhds 0)
@[simp]
theorem real.is_O_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α → } :
((λ (x : α), real.exp (f x)) =O[l] λ (x : α), real.exp (g x)) (f - g)
@[simp]
theorem real.is_Theta_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α → } :
((λ (x : α), real.exp (f x)) =Θ[l] λ (x : α), real.exp (g x)) (λ (x : α), |f x - g x|)
@[simp]
theorem real.is_o_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α → } :
((λ (x : α), real.exp (f x)) =o[l] λ (x : α), real.exp (g x)) filter.tendsto (λ (x : α), g x - f x) l filter.at_top
@[simp]
theorem real.is_o_one_exp_comp {α : Type u_1} {l : filter α} {f : α → } :
((λ (x : α), 1) =o[l] λ (x : α), real.exp (f x))
@[simp]
theorem real.is_O_one_exp_comp {α : Type u_1} {l : filter α} {f : α → } :
((λ (x : α), 1) =O[l] λ (x : α), real.exp (f x))

real.exp (f x) is bounded away from zero along a filter if and only if this filter is bounded from below under f.

theorem real.is_O_exp_comp_one {α : Type u_1} {l : filter α} {f : α → } :
((λ (x : α), real.exp (f x)) =O[l] λ (x : α), 1)

real.exp (f x) is bounded away from zero along a filter if and only if this filter is bounded from below under f.

@[simp]
theorem real.is_Theta_exp_comp_one {α : Type u_1} {l : filter α} {f : α → } :
((λ (x : α), real.exp (f x)) =Θ[l] λ (x : α), 1) (λ (x : α), |f x|)

real.exp (f x) is bounded away from zero and infinity along a filter l if and only if |f x| is bounded from above along this filter.

theorem complex.tendsto_exp_nhds_zero_iff {α : Type u_1} {l : filter α} {f : α → } :
filter.tendsto (λ (x : α), complex.exp (f x)) l (nhds 0) filter.tendsto (λ (x : α), (f x).re) l filter.at_bot

complex.abs (complex.exp z) → ∞ as complex.re z → ∞. TODO: use bornology.cobounded.

complex.exp z → 0 as complex.re z → -∞.