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 Complex.exp_sub_sum_range_isBigO_pow (n : ℕ) : (fun (x : ℂ) => Complex.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 : ℂ) => Complex.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 : 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 UniformlyContinuousOn.cexp (a : ℝ) : UniformContinuousOn Complex.exp {x : ℂ | x.re ≤ a}

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

theorem Real.continuous_exp : Continuous Real.exp

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

theorem Real.exp_sub_sum_range_isBigO_pow (n : ℕ) : (fun (x : ℝ) => Real.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 : ℝ) => Real.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 : Filter.Tendsto f l (nhds z)) : Filter.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

@[deprecated ContinuousWithinAt.rexp]

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

Alias of ContinuousWithinAt.rexp.

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

@[deprecated ContinuousAt.rexp]

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

Alias of ContinuousAt.rexp.

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

@[deprecated ContinuousOn.rexp]

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

Alias of ContinuousOn.rexp.

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

@[deprecated Continuous.rexp]

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

Alias of Continuous.rexp.

theorem Real.exp_half (x : ℝ) : Real.exp (x / 2) = √(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_zero : 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 +∞

@[deprecated Real.tendsto_exp_neg_atTop_nhds_zero]

theorem Real.tendsto_exp_neg_atTop_nhds_0 : Filter.Tendsto (fun (x : ℝ) => Real.exp (-x)) Filter.atTop (nhds 0)

Alias of Real.tendsto_exp_neg_atTop_nhds_zero.

---

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 Real.exp (nhds 0) (nhds 1)

The real exponential function tends to 1 at 0.

@[deprecated Real.tendsto_exp_nhds_zero_nhds_one]

theorem Real.tendsto_exp_nhds_0_nhds_1 : Filter.Tendsto Real.exp (nhds 0) (nhds 1)

Alias of Real.tendsto_exp_nhds_zero_nhds_one.

---

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 (x1 x2 : ℝ) => x1 ≥ x2) l fun (x : α) => Real.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 : α) => Real.exp (f x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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_zero (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.

@[deprecated Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero]

theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_0 (n : ℕ) : Filter.Tendsto (fun (x : ℝ) => x ^ n * Real.exp (-x)) Filter.atTop (nhds 0)

Alias of Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero.

---

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

@[simp]

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

@[simp]

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 (x1 x2 : ℝ) => x1 ≤ x2) 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 (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 : α) => 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 (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 : α) => Real.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 : α) => Real.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 : ℕ) => Real.exp (↑n * a)) ↔ a < 0

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

theorem Real.summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) : Summable fun (n : ℕ) => ↑n ^ k * Real.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 Complex.exp (Bornology.cobounded ℂ) = Filter.comap Complex.re Filter.atTop

@[simp]

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) (Bornology.cobounded ℂ)

Complex.abs (Complex.exp z) → ∞ as Complex.re z → ∞.

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

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.