# 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 Complex.exp_sub_sum_range_isBigO_pow (n : ) :
(fun (x : ) => - i, x ^ i / i.factorial) =O[nhds 0] fun (x : ) => x ^ n
theorem Complex.exp_sub_sum_range_succ_isLittleO_pow (n : ) :
(fun (x : ) => - iFinset.range (n + 1), x ^ i / i.factorial) =o[nhds 0] fun (x : ) => x ^ n
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 Real.exp_sub_sum_range_isBigO_pow (n : ) :
(fun (x : ) => - i, x ^ i / i.factorial) =O[nhds 0] fun (x : ) => x ^ n
theorem Real.exp_sub_sum_range_succ_isLittleO_pow (n : ) :
(fun (x : ) => - iFinset.range (n + 1), x ^ i / i.factorial) =o[nhds 0] fun (x : ) => x ^ n
theorem Filter.Tendsto.rexp {α : 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.rexp {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h : ) :
ContinuousWithinAt (fun (y : α) => Real.exp (f y)) s x
@[deprecated ContinuousWithinAt.rexp]
theorem ContinuousWithinAt.exp {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h : ) :
ContinuousWithinAt (fun (y : α) => Real.exp (f y)) s x

Alias of ContinuousWithinAt.rexp.

theorem ContinuousAt.rexp {α : Type u_1} [] {f : α} {x : α} (h : ) :
ContinuousAt (fun (y : α) => Real.exp (f y)) x
@[deprecated ContinuousAt.rexp]
theorem ContinuousAt.exp {α : Type u_1} [] {f : α} {x : α} (h : ) :
ContinuousAt (fun (y : α) => Real.exp (f y)) x

Alias of ContinuousAt.rexp.

theorem ContinuousOn.rexp {α : Type u_1} [] {f : α} {s : Set α} (h : ) :
ContinuousOn (fun (y : α) => Real.exp (f y)) s
@[deprecated ContinuousOn.rexp]
theorem ContinuousOn.exp {α : Type u_1} [] {f : α} {s : Set α} (h : ) :
ContinuousOn (fun (y : α) => Real.exp (f y)) s

Alias of ContinuousOn.rexp.

theorem Continuous.rexp {α : Type u_1} [] {f : α} (h : ) :
Continuous fun (y : α) => Real.exp (f y)
@[deprecated Continuous.rexp]
theorem Continuous.exp {α : Type u_1} [] {f : α} (h : ) :
Continuous fun (y : α) => Real.exp (f y)

Alias of Continuous.rexp.

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_zero :
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 +∞

@[deprecated Real.tendsto_exp_neg_atTop_nhds_zero]
theorem Real.tendsto_exp_neg_atTop_nhds_0 :
Filter.Tendsto (fun (x : ) => Real.exp (-x)) Filter.atTop (nhds 0)

Alias of Real.tendsto_exp_neg_atTop_nhds_zero.

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.

@[deprecated Real.tendsto_exp_nhds_zero_nhds_one]

Alias of Real.tendsto_exp_nhds_zero_nhds_one.

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_zero (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.

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

Alias of Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero.

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, +∞).

Equations
Instances For
@[simp]
theorem Real.coe_expOrderIso_apply (x : ) :
(Real.expOrderIso 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 Real.summable_exp_nat_mul_iff {a : } :
(Summable fun (n : ) => Real.exp (n * a)) a < 0
theorem Real.summable_pow_mul_exp_neg_nat_mul (k : ) {r : } (hr : 0 < r) :
Summable fun (n : ) => n ^ k * Real.exp (-r * n)
theorem HasSum.rexp {ι : Type u_1} {f : ι} {a : } (h : HasSum f a) :
HasProd () ()

If f has sum a, then exp ∘ f has product exp a.

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 → ∞.

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

theorem HasSum.cexp {ι : Type u_1} {f : ι} {a : } (h : HasSum f a) :
HasProd () ()

If f has sum a, then exp ∘ f has product exp a.