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) : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2

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

theorem Complex.continuous_exp : Continuous exp

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

theorem Complex.exp_sub_sum_range_isBigO_pow (n : ℕ) : (fun (x : ℂ) => exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun (x : ℂ) => x ^ n

theorem Complex.exp_sub_sum_range_succ_isLittleO_pow (n : ℕ) : (fun (x : ℂ) => exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun (x : ℂ) => x ^ n

theorem Filter.Tendsto.cexp {α : Type u_1} {l : Filter α} {f : α → ℂ} {z : ℂ} (hf : Tendsto f l (nhds z)) : 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 UniformContinuousOn.cexp (a : ℝ) : UniformContinuousOn Complex.exp {x : ℂ | x.re ≤ a}

The complex exponential function is uniformly continuous on left half planes.

@[deprecated UniformContinuousOn.cexp (since := "2025-02-11")]

theorem UniformlyContinuousOn.cexp (a : ℝ) : UniformContinuousOn Complex.exp {x : ℂ | x.re ≤ a}

Alias of UniformContinuousOn.cexp.

---

The complex exponential function is uniformly continuous on left half planes.

theorem Real.continuous_exp : Continuous exp

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

theorem Real.exp_sub_sum_range_isBigO_pow (n : ℕ) : (fun (x : ℝ) => exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun (x : ℝ) => x ^ n

theorem Real.exp_sub_sum_range_succ_isLittleO_pow (n : ℕ) : (fun (x : ℝ) => exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun (x : ℝ) => x ^ n

theorem Filter.Tendsto.rexp {α : Type u_1} {l : Filter α} {f : α → ℝ} {z : ℝ} (hf : Tendsto f l (nhds z)) : Tendsto (fun (x : α) => Real.exp (f x)) l (nhds (Real.exp z))

theorem ContinuousWithinAt.rexp {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (y : α) => Real.exp (f y)) s x

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

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

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

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

theorem Real.tendsto_exp_atTop : Filter.Tendsto exp Filter.atTop Filter.atTop

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

theorem Real.tendsto_exp_neg_atTop_nhds_zero : Filter.Tendsto (fun (x : ℝ) => 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_zero_nhds_one : Filter.Tendsto exp (nhds 0) (nhds 1)

The real exponential function tends to 1 at 0.

theorem Real.tendsto_exp_atBot : Filter.Tendsto exp Filter.atBot (nhds 0)

theorem Real.tendsto_exp_atBot_nhdsGT : Filter.Tendsto exp Filter.atBot (nhdsWithin 0 (Set.Ioi 0))

@[deprecated Real.tendsto_exp_atBot_nhdsGT (since := "2024-12-22")]

theorem Real.tendsto_exp_atBot_nhdsWithin : Filter.Tendsto exp Filter.atBot (nhdsWithin 0 (Set.Ioi 0))

Alias of Real.tendsto_exp_atBot_nhdsGT.

@[simp]

theorem Real.isBoundedUnder_ge_exp_comp {α : Type u_1} (l : Filter α) (f : α → ℝ) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) l fun (x : α) => exp (f x)

@[simp]

theorem Real.isBoundedUnder_le_exp_comp {α : Type u_1} {l : Filter α} {f : α → ℝ} : (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => exp (f x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l f

theorem Real.tendsto_exp_div_pow_atTop (n : ℕ) : Filter.Tendsto (fun (x : ℝ) => 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_zero (n : ℕ) : Filter.Tendsto (fun (x : ℝ) => x ^ n * 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 * 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 * 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_3 Real.expOrderIso._proof_4

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.map_exp_atTop : Filter.map exp Filter.atTop = Filter.atTop

@[simp]

theorem Real.comap_exp_atTop : Filter.comap exp Filter.atTop = Filter.atTop

@[simp]

theorem Real.tendsto_exp_comp_atTop {α : Type u_1} {l : Filter α} {f : α → ℝ} : Filter.Tendsto (fun (x : α) => 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 (exp x)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l

@[simp]

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

@[simp]

theorem Real.comap_exp_nhdsGT_zero : Filter.comap exp (nhdsWithin 0 (Set.Ioi 0)) = Filter.atBot

@[deprecated Real.comap_exp_nhdsGT_zero (since := "2024-12-22")]

theorem Real.comap_exp_nhdsWithin_Ioi_zero : Filter.comap exp (nhdsWithin 0 (Set.Ioi 0)) = Filter.atBot

Alias of Real.comap_exp_nhdsGT_zero.

theorem Real.tendsto_comp_exp_atBot {α : Type u_1} {l : Filter α} {f : ℝ → α} : Filter.Tendsto (fun (x : ℝ) => f (exp x)) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) l

@[simp]

theorem Real.comap_exp_nhds_zero : Filter.comap exp (nhds 0) = Filter.atBot

@[simp]

theorem Real.tendsto_exp_comp_nhds_zero {α : Type u_1} {l : Filter α} {f : α → ℝ} : Filter.Tendsto (fun (x : α) => exp (f x)) l (nhds 0) ↔ Filter.Tendsto f l Filter.atBot

theorem Real.isOpenEmbedding_exp : Topology.IsOpenEmbedding exp

@[simp]

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

@[simp]

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

theorem Real.isLittleO_pow_exp_atTop {n : ℕ} : (fun (x : ℝ) => x ^ n) =o[Filter.atTop] exp

@[simp]

theorem Real.isBigO_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → ℝ} : ((fun (x : α) => exp (f x)) =O[l] fun (x : α) => exp (g x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (f - g)

@[simp]

theorem Real.isTheta_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → ℝ} : ((fun (x : α) => exp (f x)) =Θ[l] fun (x : α) => exp (g x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => |f x - g x|

@[simp]

theorem Real.isLittleO_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → ℝ} : ((fun (x : α) => exp (f x)) =o[l] fun (x : α) => 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 : α) => 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 : α) => exp (f x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) 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 : α) => exp (f x)) =O[l] fun (x : α) => 1) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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 : α) => exp (f x)) =Θ[l] fun (x : α) => 1) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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 : ℕ) => exp (↑n * a)) ↔ a < 0

theorem Real.summable_exp_neg_nat : Summable fun (n : ℕ) => exp (-↑n)

theorem Real.summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) : Summable fun (n : ℕ) => ↑n ^ k * exp (-r * ↑n)

theorem HasSum.rexp {ι : Type u_1} {f : ι → ℝ} {a : ℝ} (h : HasSum f a) : HasProd (Real.exp ∘ f) (Real.exp a)

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

@[simp]

theorem Complex.comap_exp_cobounded : Filter.comap exp (Bornology.cobounded ℂ) = Filter.comap re Filter.atTop

@[simp]

theorem Complex.comap_exp_nhds_zero : Filter.comap exp (nhds 0) = Filter.comap re Filter.atBot

theorem Complex.comap_exp_nhdsNE : Filter.comap exp (nhdsWithin 0 {0}ᶜ) = Filter.comap re Filter.atBot

@[deprecated Complex.comap_exp_nhdsNE (since := "2024-12-22")]

theorem Complex.comap_exp_nhdsWithin_zero : Filter.comap exp (nhdsWithin 0 {0}ᶜ) = Filter.comap re Filter.atBot

Alias of Complex.comap_exp_nhdsNE.

theorem Complex.tendsto_exp_nhds_zero_iff {α : Type u_1} {l : Filter α} {f : α → ℂ} : Filter.Tendsto (fun (x : α) => 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 exp (Filter.comap re Filter.atTop) (Bornology.cobounded ℂ)

‖Complex.exp z‖ → ∞ as Complex.re z → ∞.

theorem Complex.tendsto_exp_comap_re_atBot : Filter.Tendsto exp (Filter.comap re Filter.atBot) (nhds 0)

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

theorem Complex.tendsto_exp_comap_re_atBot_nhdsNE : Filter.Tendsto exp (Filter.comap re Filter.atBot) (nhdsWithin 0 {0}ᶜ)

@[deprecated Complex.tendsto_exp_comap_re_atBot_nhdsNE (since := "2024-12-22")]

theorem Complex.tendsto_exp_comap_re_atBot_nhdsWithin : Filter.Tendsto exp (Filter.comap re Filter.atBot) (nhdsWithin 0 {0}ᶜ)

Alias of Complex.tendsto_exp_comap_re_atBot_nhdsNE.

theorem HasSum.cexp {ι : Type u_1} {f : ι → ℂ} {a : ℂ} (h : HasSum f a) : HasProd (Complex.exp ∘ f) (Complex.exp a)

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