analysis.special_functions.exp

source

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

source

theorem complex.locally_lipschitz_exp {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_le : r ≤ 1) (x y : ℂ) (hyx : ‖y - x‖ < r) :

‖complex.exp y - complex.exp x‖ ≤ (1 + r) * ‖complex.exp x‖ * ‖y - x‖

source

@[continuity]

theorem complex.continuous_exp :

continuous complex.exp

source

theorem complex.continuous_on_exp {s : set ℂ} :

continuous_on complex.exp s

source

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))

source

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

source

theorem continuous_at.cexp {α : Type u_1} [topological_space α] {f : α → ℂ} {x : α} (h : continuous_at f x) :

continuous_at (λ (y : α), complex.exp (f y)) x

source

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

source

theorem continuous.cexp {α : Type u_1} [topological_space α] {f : α → ℂ} (h : continuous f) :

continuous (λ (y : α), complex.exp (f y))

source

@[continuity]

theorem real.continuous_exp :

continuous real.exp

source

theorem real.continuous_on_exp {s : set ℝ} :

continuous_on real.exp s

source

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))

source

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

source

theorem continuous_at.exp {α : Type u_1} [topological_space α] {f : α → ℝ} {x : α} (h : continuous_at f x) :

continuous_at (λ (y : α), real.exp (f y)) x

source

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

source

theorem continuous.exp {α : Type u_1} [topological_space α] {f : α → ℝ} (h : continuous f) :

continuous (λ (y : α), real.exp (f y))

source

theorem real.exp_half (x : ℝ) :

real.exp (x / 2) = real.sqrt (real.exp x)

source

theorem real.tendsto_exp_at_top :

filter.tendsto real.exp filter.at_top filter.at_top

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

source

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

source

theorem real.tendsto_exp_nhds_0_nhds_1 :

filter.tendsto real.exp (nhds 0) (nhds 1)

The real exponential function tends to 1 at 0.

source

theorem real.tendsto_exp_at_bot :

filter.tendsto real.exp filter.at_bot (nhds 0)

source

theorem real.tendsto_exp_at_bot_nhds_within :

filter.tendsto real.exp filter.at_bot (nhds_within 0 (set.Ioi 0))

source

@[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))

source

@[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

source

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

source

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.

source

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.

source

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.

source

noncomputable def real.exp_order_iso :

ℝ ≃o ↥(set.Ioi 0)

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

source

@[simp]

theorem real.coe_exp_order_iso_apply (x : ℝ) :

↑(⇑real.exp_order_iso x) = real.exp x

source

@[simp]

theorem real.coe_comp_exp_order_iso :

coe ∘ ⇑real.exp_order_iso = real.exp

source

@[simp]

theorem real.range_exp :

set.range real.exp = set.Ioi 0

source

@[simp]

theorem real.map_exp_at_top :

filter.map real.exp filter.at_top = filter.at_top

source

@[simp]

theorem real.comap_exp_at_top :

filter.comap real.exp filter.at_top = filter.at_top

source

@[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

source

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

source

@[simp]

theorem real.map_exp_at_bot :

filter.map real.exp filter.at_bot = nhds_within 0 (set.Ioi 0)

source

@[simp]

theorem real.comap_exp_nhds_within_Ioi_zero :

filter.comap real.exp (nhds_within 0 (set.Ioi 0)) = filter.at_bot

source

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

source

@[simp]

theorem real.comap_exp_nhds_zero :

filter.comap real.exp (nhds 0) = filter.at_bot

source

@[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

source

theorem real.is_o_pow_exp_at_top {n : ℕ} :

(λ (x : ℝ), x ^ n) =o[filter.at_top ] real.exp

source

@[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.is_bounded_under has_le.le l (f - g)

source

@[simp]

theorem real.is_Theta_exp_comp_exp_comp {α : Type u_1} {l : filter α} {f g : α → ℝ} :

((λ (x : α), real.exp (f x)) =Θ[l] λ (x : α), real.exp (g x)) ↔ filter.is_bounded_under has_le.le l (λ (x : α), |f x - g x|)

source

@[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

source

@[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

source

@[simp]

theorem real.is_O_one_exp_comp {α : Type u_1} {l : filter α} {f : α → ℝ} :

((λ (x : α), 1) =O[l] λ (x : α), real.exp (f x)) ↔ filter.is_bounded_under ge 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.

source

theorem real.is_O_exp_comp_one {α : Type u_1} {l : filter α} {f : α → ℝ} :

((λ (x : α), real.exp (f x)) =O[l] λ (x : α), 1) ↔ filter.is_bounded_under has_le.le 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.

source

@[simp]

theorem real.is_Theta_exp_comp_one {α : Type u_1} {l : filter α} {f : α → ℝ} :

((λ (x : α), real.exp (f x)) =Θ[l] λ (x : α), 1) ↔ filter.is_bounded_under has_le.le l (λ (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.

source

theorem complex.comap_exp_comap_abs_at_top :

filter.comap complex.exp (filter.comap ⇑complex.abs filter.at_top) = filter.comap complex.re filter.at_top

source

theorem complex.comap_exp_nhds_zero :

filter.comap complex.exp (nhds 0) = filter.comap complex.re filter.at_bot

source

theorem complex.comap_exp_nhds_within_zero :

filter.comap complex.exp (nhds_within 0 {0}ᶜ) = filter.comap complex.re filter.at_bot

source

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

source

theorem complex.tendsto_exp_comap_re_at_top :

filter.tendsto complex.exp (filter.comap complex.re filter.at_top) (filter.comap ⇑complex.abs filter.at_top)

complex.abs (complex.exp z) → ∞ as complex.re z → ∞. TODO: use bornology.cobounded.

source

theorem complex.tendsto_exp_comap_re_at_bot :

filter.tendsto complex.exp (filter.comap complex.re filter.at_bot) (nhds 0)

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

source

theorem complex.tendsto_exp_comap_re_at_bot_nhds_within :

filter.tendsto complex.exp (filter.comap complex.re filter.at_bot) (nhds_within 0 {0}ᶜ)

mathlib3 documentation

Complex and real exponential #

Tags #