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

theorem Complex.continuous_exp : Continuous Complex.exp

theorem Complex.continuousOn_exp {s : Set ℂ} : ContinuousOn Complex.exp s

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 Real.continuous_exp : Continuous Real.exp

theorem Real.continuousOn_exp {s : Set ℝ} : ContinuousOn Real.exp s

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)

theorem Real.exp_half (x : ℝ) : Real.exp (x / 2) = Real.sqrt (Real.exp x)

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

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.

theorem Real.tendsto_exp_atBot : Filter.Tendsto Real.exp Filter.atBot (nhds 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

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 * Real.exp x + 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 * Real.exp x + 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.

def Real.expOrderIso : ℝ ≃o ↑(Set.Ioi 0)

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

Equations

• Real.expOrderIso = StrictMono.orderIsoOfSurjective (Set.codRestrict Real.exp (Real.lt 0) Real.exp_pos) Real.expOrderIso.proof_1 Real.expOrderIso.proof_2

@[simp]

theorem Real.coe_expOrderIso_apply (x : ℝ) : ↑(↑Real.expOrderIso x) = Real.exp x

@[simp]

theorem Real.coe_comp_expOrderIso : Subtype.val ∘ ↑Real.expOrderIso = Real.exp

@[simp]

theorem Real.range_exp : Set.range Real.exp = Set.Ioi 0

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

theorem Real.map_exp_atBot : Filter.map Real.exp Filter.atBot = nhdsWithin 0 (Set.Ioi 0)

@[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.comap_exp_nhds_zero : Filter.comap Real.exp (nhds 0) = Filter.atBot

@[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.openEmbedding_exp : OpenEmbedding Real.exp

theorem Real.map_exp_nhds (x : ℝ) : Filter.map Real.exp (nhds x) = nhds (Real.exp x)

theorem Real.comap_exp_nhds_exp (x : ℝ) : Filter.comap Real.exp (nhds (Real.exp x)) = nhds x

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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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.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}ᶜ)