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 (λ (x : α), complex.exp (f x)) l (nhds (complex.exp z))
theorem
continuous_within_at.cexp
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
{x : α}
(h : continuous_within_at f s x) :
continuous_within_at (λ (y : α), complex.exp (f y)) s x
theorem
continuous_at.cexp
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{x : α}
(h : continuous_at f x) :
continuous_at (λ (y : α), complex.exp (f y)) x
theorem
continuous_on.cexp
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
(h : continuous_on f s) :
continuous_on (λ (y : α), complex.exp (f y)) s
theorem
continuous.cexp
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
(h : continuous f) :
continuous (λ (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 (λ (x : α), real.exp (f x)) l (nhds (real.exp z))
theorem
continuous_within_at.exp
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{s : set α}
{x : α}
(h : continuous_within_at f s x) :
continuous_within_at (λ (y : α), real.exp (f y)) s x
theorem
continuous_at.exp
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{x : α}
(h : continuous_at f x) :
continuous_at (λ (y : α), real.exp (f y)) x
theorem
continuous_on.exp
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{s : set α}
(h : continuous_on f s) :
continuous_on (λ (y : α), real.exp (f y)) s
theorem
continuous.exp
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
(h : continuous f) :
continuous (λ (y : α), real.exp (f y))
The real exponential function tends to +∞ at +∞.
theorem
real.tendsto_exp_neg_at_top_nhds_0
:
filter.tendsto (λ (x : ℝ), real.exp (-x)) filter.at_top (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.is_bounded_under_ge_exp_comp
{α : Type u_1}
(l : filter α)
(f : α → ℝ) :
filter.is_bounded_under ge l (λ (x : α), real.exp (f x))
@[simp]
theorem
real.is_bounded_under_le_exp_comp
{α : Type u_1}
{l : filter α}
{f : α → ℝ} :
filter.is_bounded_under has_le.le l (λ (x : α), real.exp (f x)) ↔ filter.is_bounded_under has_le.le l f
theorem
real.tendsto_exp_div_pow_at_top
(n : ℕ) :
filter.tendsto (λ (x : ℝ), real.exp x / x ^ n) filter.at_top filter.at_top
The function exp(x)/x^n tends to +∞ at +∞, for any natural number n
theorem
real.tendsto_pow_mul_exp_neg_at_top_nhds_0
(n : ℕ) :
filter.tendsto (λ (x : ℝ), x ^ n * real.exp (-x)) filter.at_top (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_at_top
(b c : ℝ)
(n : ℕ)
(hb : 0 < b) :
filter.tendsto (λ (x : ℝ), (b * real.exp x + c) / x ^ n) filter.at_top filter.at_top
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 * real.exp 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.
real.exp as an order isomorphism between ℝ and (0, +∞).
Equations
- real.exp_order_iso = strict_mono.order_iso_of_surjective (set.cod_restrict real.exp (set.Ioi 0) real.exp_pos) real.exp_order_iso._proof_1 real.exp_order_iso._proof_2
@[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 ↔ filter.tendsto f l filter.at_top
theorem
real.tendsto_comp_exp_at_top
{α : Type u_1}
{l : filter α}
{f : ℝ → α} :
filter.tendsto (λ (x : ℝ), f (real.exp x)) filter.at_top l ↔ filter.tendsto f filter.at_top l
@[simp]
@[simp]
theorem
real.comap_exp_nhds_within_Ioi_zero
:
filter.comap real.exp (nhds_within 0 (set.Ioi 0)) = filter.at_bot
theorem
real.tendsto_comp_exp_at_bot
{α : Type u_1}
{l : filter α}
{f : ℝ → α} :
filter.tendsto (λ (x : ℝ), f (real.exp x)) filter.at_bot l ↔ filter.tendsto f (nhds_within 0 (set.Ioi 0)) l
@[simp]
theorem
real.tendsto_exp_comp_nhds_zero
{α : Type u_1}
{l : filter α}
{f : α → ℝ} :
filter.tendsto (λ (x : α), real.exp (f x)) l (nhds 0) ↔ filter.tendsto f l filter.at_bot
@[simp]
theorem
real.is_o_exp_comp_exp_comp
{α : Type u_1}
{l : filter α}
{f g : α → ℝ} :
((λ (x : α), real.exp (f x)) =o[l] λ (x : α), real.exp (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 : α), real.exp (f x)) ↔ filter.tendsto f l filter.at_top
@[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.tendsto_exp_nhds_zero_iff
{α : Type u_1}
{l : filter α}
{f : α → ℂ} :
filter.tendsto (λ (x : α), complex.exp (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 → -∞.