# Documentation

Mathlib.Analysis.SpecialFunctions.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
theorem Filter.Tendsto.cexp {α : Type u_1} {l : } {f : α} {z : } (hf : Filter.Tendsto f l (nhds z)) :
Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds ())
theorem ContinuousWithinAt.cexp {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h : ) :
ContinuousWithinAt (fun y => Complex.exp (f y)) s x
theorem ContinuousAt.cexp {α : Type u_1} [] {f : α} {x : α} (h : ) :
ContinuousAt (fun y => Complex.exp (f y)) x
theorem ContinuousOn.cexp {α : Type u_1} [] {f : α} {s : Set α} (h : ) :
ContinuousOn (fun y => Complex.exp (f y)) s
theorem Continuous.cexp {α : Type u_1} [] {f : α} (h : ) :
Continuous fun y => Complex.exp (f y)
theorem Filter.Tendsto.exp {α : Type u_1} {l : } {f : α} {z : } (hf : Filter.Tendsto f l (nhds z)) :
Filter.Tendsto (fun x => Real.exp (f x)) l (nhds ())
theorem ContinuousWithinAt.exp {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h : ) :
ContinuousWithinAt (fun y => Real.exp (f y)) s x
theorem ContinuousAt.exp {α : Type u_1} [] {f : α} {x : α} (h : ) :
ContinuousAt (fun y => Real.exp (f y)) x
theorem ContinuousOn.exp {α : Type u_1} [] {f : α} {s : Set α} (h : ) :
ContinuousOn (fun y => Real.exp (f y)) s
theorem Continuous.exp {α : Type u_1} [] {f : α} (h : ) :
Continuous fun y => Real.exp (f y)
theorem Real.exp_half (x : ) :
Real.exp (x / 2) =
theorem Real.tendsto_exp_atTop :
Filter.Tendsto Real.exp Filter.atTop Filter.atTop

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

theorem Real.tendsto_exp_neg_atTop_nhds_0 :
Filter.Tendsto (fun x => Real.exp (-x)) Filter.atTop (nhds 0)

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.isBoundedUnder_ge_exp_comp {α : Type u_1} (l : ) (f : α) :
Filter.IsBoundedUnder (fun x x_1 => x x_1) l fun x => Real.exp (f x)
@[simp]
theorem Real.isBoundedUnder_le_exp_comp {α : Type u_1} {l : } {f : α} :
(Filter.IsBoundedUnder (fun x x_1 => x x_1) l fun x => Real.exp (f x)) Filter.IsBoundedUnder (fun x x_1 => x x_1) l f
theorem Real.tendsto_exp_div_pow_atTop (n : ) :
Filter.Tendsto (fun x => / x ^ n) Filter.atTop Filter.atTop

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

theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_0 (n : ) :
Filter.Tendsto (fun x => x ^ n * Real.exp (-x)) Filter.atTop (nhds 0)

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

theorem Real.tendsto_mul_exp_add_div_pow_atTop (b : ) (c : ) (n : ) (hb : 0 < b) :
Filter.Tendsto (fun x => (b * + c) / x ^ n) Filter.atTop Filter.atTop

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_atTop (b : ) (c : ) (n : ) (hb : 0 b) :
Filter.Tendsto (fun x => x ^ n / (b * + c)) Filter.atTop (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.

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

Instances For
@[simp]
theorem Real.coe_expOrderIso_apply (x : ) :
↑() =
@[simp]
@[simp]
theorem Real.range_exp :
@[simp]
theorem Real.map_exp_atTop :
Filter.map Real.exp Filter.atTop = Filter.atTop
@[simp]
theorem Real.comap_exp_atTop :
Filter.comap Real.exp Filter.atTop = Filter.atTop
@[simp]
theorem Real.tendsto_exp_comp_atTop {α : Type u_1} {l : } {f : α} :
Filter.Tendsto (fun x => Real.exp (f x)) l Filter.atTop Filter.Tendsto f l Filter.atTop
theorem Real.tendsto_comp_exp_atTop {α : Type u_1} {l : } {f : α} :
Filter.Tendsto (fun x => f ()) Filter.atTop l Filter.Tendsto f Filter.atTop l
@[simp]
@[simp]
theorem Real.comap_exp_nhdsWithin_Ioi_zero :
= Filter.atBot
theorem Real.tendsto_comp_exp_atBot {α : Type u_1} {l : } {f : α} :
Filter.Tendsto (fun x => f ()) Filter.atBot l Filter.Tendsto f (nhdsWithin 0 ()) l
@[simp]
theorem Real.comap_exp_nhds_zero :
= Filter.atBot
@[simp]
theorem Real.tendsto_exp_comp_nhds_zero {α : Type u_1} {l : } {f : α} :
Filter.Tendsto (fun x => Real.exp (f x)) l (nhds 0) Filter.Tendsto f l Filter.atBot
theorem Real.map_exp_nhds (x : ) :
= nhds ()
theorem Real.isLittleO_pow_exp_atTop {n : } :
(fun x => x ^ n) =o[Filter.atTop] Real.exp
@[simp]
theorem Real.isBigO_exp_comp_exp_comp {α : Type u_1} {l : } {f : α} {g : α} :
((fun x => Real.exp (f x)) =O[l] fun x => Real.exp (g x)) Filter.IsBoundedUnder (fun x x_1 => x x_1) l (f - g)
@[simp]
theorem Real.isTheta_exp_comp_exp_comp {α : Type u_1} {l : } {f : α} {g : α} :
((fun x => Real.exp (f x)) =Θ[l] fun x => Real.exp (g x)) Filter.IsBoundedUnder (fun x x_1 => x x_1) l fun x => |f x - g x|
@[simp]
theorem Real.isLittleO_exp_comp_exp_comp {α : Type u_1} {l : } {f : α} {g : α} :
((fun x => Real.exp (f x)) =o[l] fun x => Real.exp (g x)) Filter.Tendsto (fun x => g x - f x) l Filter.atTop
theorem Real.isLittleO_one_exp_comp {α : Type u_1} {l : } {f : α} :
((fun x => 1) =o[l] fun x => Real.exp (f x)) Filter.Tendsto f l Filter.atTop
@[simp]
theorem Real.isBigO_one_exp_comp {α : Type u_1} {l : } {f : α} :
((fun x => 1) =O[l] fun x => Real.exp (f x)) Filter.IsBoundedUnder (fun x x_1 => x x_1) l f

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.isBigO_exp_comp_one {α : Type u_1} {l : } {f : α} :
((fun x => Real.exp (f x)) =O[l] fun x => 1) Filter.IsBoundedUnder (fun x x_1 => x x_1) l f

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.isTheta_exp_comp_one {α : Type u_1} {l : } {f : α} :
((fun x => Real.exp (f x)) =Θ[l] fun x => 1) Filter.IsBoundedUnder (fun x x_1 => x x_1) l fun 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 : } {f : α} :
Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds 0) Filter.Tendsto (fun x => (f x).re) l Filter.atBot

Complex.abs (Complex.exp z) → ∞ as Complex.re z → ∞. TODO: use Bornology.cobounded.

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