# 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 : (𝓝 z)) :
filter.tendsto (λ (x : α), complex.exp (f x)) l (𝓝 (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 : (𝓝 z)) :
filter.tendsto (λ (x : α), real.exp (f x)) l (𝓝 (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))

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.

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) (hn : 1 n) :

The function (b * exp x + c) / (x ^ n) tends to +∞ at +∞, for any positive 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) (hn : 1 n) :
filter.tendsto (λ (x : ), x ^ n / (b * + c)) filter.at_top (𝓝 0)

The function (x ^ n) / (b * exp x + c) tends to 0 at +∞, for any positive 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  :
theorem real.tendsto_comp_exp_at_bot {α : Type u_1} {l : filter α} {f : → α} :