# mathlib3documentation

analysis.special_functions.exp

# Complex and real exponential #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
@[continuity]
theorem filter.tendsto.cexp {α : Type u_1} {l : filter α} {f : α } {z : } (hf : (nhds z)) :
filter.tendsto (λ (x : α), cexp (f x)) l (nhds (cexp z))
theorem continuous_within_at.cexp {α : Type u_1} {f : α } {s : set α} {x : α} (h : x) :
continuous_within_at (λ (y : α), cexp (f y)) s x
theorem continuous_at.cexp {α : Type u_1} {f : α } {x : α} (h : x) :
continuous_at (λ (y : α), cexp (f y)) x
theorem continuous_on.cexp {α : Type u_1} {f : α } {s : set α} (h : s) :
continuous_on (λ (y : α), cexp (f y)) s
theorem continuous.cexp {α : Type u_1} {f : α } (h : continuous f) :
continuous (λ (y : α), cexp (f y))
@[continuity]
theorem real.continuous_exp  :
theorem filter.tendsto.exp {α : Type u_1} {l : filter α} {f : α } {z : } (hf : (nhds z)) :
filter.tendsto (λ (x : α), rexp (f x)) l (nhds (rexp z))
theorem continuous_within_at.exp {α : Type u_1} {f : α } {s : set α} {x : α} (h : x) :
continuous_within_at (λ (y : α), rexp (f y)) s x
theorem continuous_at.exp {α : Type u_1} {f : α } {x : α} (h : x) :
continuous_at (λ (y : α), rexp (f y)) x
theorem continuous_on.exp {α : Type u_1} {f : α } {s : set α} (h : s) :
continuous_on (λ (y : α), rexp (f y)) s
theorem continuous.exp {α : Type u_1} {f : α } (h : continuous f) :
continuous (λ (y : α), rexp (f y))
theorem real.exp_half (x : ) :
rexp (x / 2) = (rexp x)

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 : α), rexp (f x))
@[simp]
theorem real.is_bounded_under_le_exp_comp {α : Type u_1} {l : filter α} {f : α } :
(λ (x : α), rexp (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 * rexp x + 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 : α), rexp (f x)) l filter.at_top
theorem real.tendsto_comp_exp_at_top {α : Type u_1} {l : filter α} {f : α} :
filter.tendsto (λ (x : ), f (rexp x)) filter.at_top l
@[simp]
theorem real.map_exp_at_bot  :
theorem real.tendsto_comp_exp_at_bot {α : Type u_1} {l : filter α} {f : α} :
filter.tendsto (λ (x : ), f (rexp 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 : α), rexp (f x)) l (nhds 0)
theorem real.is_o_pow_exp_at_top {n : } :
(λ (x : ), x ^ n) =o[filter.at_top] rexp
@[simp]
theorem real.is_O_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α } :
((λ (x : α), rexp (f x)) =O[l] λ (x : α), rexp (g x)) (f - g)
@[simp]
theorem real.is_Theta_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α } :
((λ (x : α), rexp (f x)) =Θ[l] λ (x : α), rexp (g x)) (λ (x : α), |f x - g x|)
@[simp]
theorem real.is_o_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α } :
((λ (x : α), rexp (f x)) =o[l] λ (x : α), rexp (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 : α), rexp (f x))
@[simp]
theorem real.is_O_one_exp_comp {α : Type u_1} {l : filter α} {f : α } :
((λ (x : α), 1) =O[l] λ (x : α), rexp (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 : α), rexp (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 : α), rexp (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 : α), cexp (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 → -∞.