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)
:
‖Complex.exp (x + z) - Complex.exp x - z • Complex.exp x‖ ≤ ‖Complex.exp x‖ * ‖z‖ ^ 2
theorem
Filter.Tendsto.cexp
{α : Type u_1}
{l : Filter α}
{f : α → ℂ}
{z : ℂ}
(hf : Filter.Tendsto f l (nhds z))
:
Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds (Complex.exp z))
theorem
ContinuousWithinAt.cexp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{s : Set α}
{x : α}
(h : ContinuousWithinAt f s x)
:
ContinuousWithinAt (fun y => Complex.exp (f y)) s x
theorem
ContinuousAt.cexp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{x : α}
(h : ContinuousAt f x)
:
ContinuousAt (fun y => Complex.exp (f y)) x
theorem
ContinuousOn.cexp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun y => Complex.exp (f y)) s
theorem
Continuous.cexp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
(h : Continuous f)
:
Continuous fun y => Complex.exp (f y)
theorem
Filter.Tendsto.exp
{α : Type u_1}
{l : Filter α}
{f : α → ℝ}
{z : ℝ}
(hf : Filter.Tendsto f l (nhds z))
:
Filter.Tendsto (fun x => Real.exp (f x)) l (nhds (Real.exp z))
theorem
ContinuousWithinAt.exp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℝ}
{s : Set α}
{x : α}
(h : ContinuousWithinAt f s x)
:
ContinuousWithinAt (fun y => Real.exp (f y)) s x
theorem
ContinuousAt.exp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℝ}
{x : α}
(h : ContinuousAt f x)
:
ContinuousAt (fun y => Real.exp (f y)) x
theorem
ContinuousOn.exp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℝ}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun y => Real.exp (f y)) s
theorem
Continuous.exp
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℝ}
(h : Continuous f)
:
Continuous fun y => Real.exp (f y)
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
.
theorem
Real.tendsto_exp_atBot_nhdsWithin :
Filter.Tendsto Real.exp Filter.atBot (nhdsWithin 0 (Set.Ioi 0))
@[simp]
theorem
Real.isBoundedUnder_ge_exp_comp
{α : Type u_1}
(l : Filter α)
(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 : Filter α}
{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 => Real.exp x / x ^ n) Filter.atTop Filter.atTop
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
.
@[simp]
theorem
Real.tendsto_exp_comp_atTop
{α : Type u_1}
{l : Filter α}
{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 : Filter α}
{f : ℝ → α}
:
Filter.Tendsto (fun x => f (Real.exp x)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
@[simp]
@[simp]
theorem
Real.comap_exp_nhdsWithin_Ioi_zero :
Filter.comap Real.exp (nhdsWithin 0 (Set.Ioi 0)) = Filter.atBot
theorem
Real.tendsto_comp_exp_atBot
{α : Type u_1}
{l : Filter α}
{f : ℝ → α}
:
Filter.Tendsto (fun x => f (Real.exp x)) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) l
@[simp]
theorem
Real.tendsto_exp_comp_nhds_zero
{α : Type u_1}
{l : Filter α}
{f : α → ℝ}
:
Filter.Tendsto (fun x => Real.exp (f x)) l (nhds 0) ↔ Filter.Tendsto f l Filter.atBot
theorem
Real.isLittleO_one_exp_comp
{α : Type u_1}
{l : Filter α}
{f : α → ℝ}
:
((fun x => 1) =o[l] fun x => Real.exp (f x)) ↔ Filter.Tendsto f l Filter.atTop
@[simp]
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.comap_exp_comap_abs_atTop :
Filter.comap Complex.exp (Filter.comap (↑Complex.abs) Filter.atTop) = Filter.comap Complex.re Filter.atTop
theorem
Complex.comap_exp_nhds_zero :
Filter.comap Complex.exp (nhds 0) = Filter.comap Complex.re Filter.atBot
theorem
Complex.comap_exp_nhdsWithin_zero :
Filter.comap Complex.exp (nhdsWithin 0 {0}ᶜ) = Filter.comap Complex.re Filter.atBot
theorem
Complex.tendsto_exp_nhds_zero_iff
{α : Type u_1}
{l : Filter α}
{f : α → ℂ}
:
Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds 0) ↔ Filter.Tendsto (fun x => (f x).re) l Filter.atBot
theorem
Complex.tendsto_exp_comap_re_atTop :
Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atTop) (Filter.comap (↑Complex.abs) Filter.atTop)
Complex.abs (Complex.exp z) → ∞
as Complex.re z → ∞
. TODO: use Bornology.cobounded
.
theorem
Complex.tendsto_exp_comap_re_atBot :
Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (nhds 0)
Complex.exp z → 0
as Complex.re z → -∞
.
theorem
Complex.tendsto_exp_comap_re_atBot_nhdsWithin :
Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (nhdsWithin 0 {0}ᶜ)