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 : Complex) (hz : LE.le (Norm.norm z) 1) : LE.le (Norm.norm (HSub.hSub (HSub.hSub (exp (HAdd.hAdd x z)) (exp x)) (HSMul.hSMul z (exp x)))) (HMul.hMul (Norm.norm (exp x)) (HPow.hPow (Norm.norm z) 2))

theorem Complex.locally_lipschitz_exp {r : Real} (hr_nonneg : LE.le 0 r) (hr_le : LE.le r 1) (x y : Complex) (hyx : LT.lt (Norm.norm (HSub.hSub y x)) r) : LE.le (Norm.norm (HSub.hSub (exp y) (exp x))) (HMul.hMul (HMul.hMul (HAdd.hAdd 1 r) (Norm.norm (exp x))) (Norm.norm (HSub.hSub y x)))

theorem Complex.continuous_exp : Continuous exp

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

theorem Complex.exp_sub_sum_range_isBigO_pow (n : Nat) : Asymptotics.IsBigO (nhds 0) (fun (x : Complex) => HSub.hSub (exp x) ((Finset.range n).sum fun (i : Nat) => HDiv.hDiv (HPow.hPow x i) i.factorial.cast)) fun (x : Complex) => HPow.hPow x n

theorem Complex.exp_sub_sum_range_succ_isLittleO_pow (n : Nat) : Asymptotics.IsLittleO (nhds 0) (fun (x : Complex) => HSub.hSub (exp x) ((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) => HDiv.hDiv (HPow.hPow x i) i.factorial.cast)) fun (x : Complex) => HPow.hPow x n

theorem Filter.Tendsto.cexp {α : Type u_1} {l : Filter α} {f : α → Complex} {z : Complex} (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 : α → Complex} {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 : α → Complex} {x : α} (h : ContinuousAt f x) : ContinuousAt (fun (y : α) => Complex.exp (f y)) x

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

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

theorem UniformContinuousOn.cexp (a : Real) : UniformContinuousOn Complex.exp (setOf fun (x : Complex) => LE.le 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 : Real) : UniformContinuousOn Complex.exp (setOf fun (x : Complex) => LE.le 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 Real} : ContinuousOn exp s

theorem Real.exp_sub_sum_range_isBigO_pow (n : Nat) : Asymptotics.IsBigO (nhds 0) (fun (x : Real) => HSub.hSub (exp x) ((Finset.range n).sum fun (i : Nat) => HDiv.hDiv (HPow.hPow x i) i.factorial.cast)) fun (x : Real) => HPow.hPow x n

theorem Real.exp_sub_sum_range_succ_isLittleO_pow (n : Nat) : Asymptotics.IsLittleO (nhds 0) (fun (x : Real) => HSub.hSub (exp x) ((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) => HDiv.hDiv (HPow.hPow x i) i.factorial.cast)) fun (x : Real) => HPow.hPow x n

theorem Filter.Tendsto.rexp {α : Type u_1} {l : Filter α} {f : α → Real} {z : Real} (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 : α → Real} {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 : α → Real} {x : α} (h : ContinuousAt f x) : ContinuousAt (fun (y : α) => Real.exp (f y)) x

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

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

theorem Real.exp_half (x : Real) : Eq (exp (HDiv.hDiv x 2)) (exp x).sqrt

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 : Real) => exp (Neg.neg 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.

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

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

theorem Real.tendsto_exp_div_pow_atTop (n : Nat) : Filter.Tendsto (fun (x : Real) => HDiv.hDiv (exp x) (HPow.hPow 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 : Nat) : Filter.Tendsto (fun (x : Real) => HMul.hMul (HPow.hPow x n) (exp (Neg.neg 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 : Real) (n : Nat) (hb : LT.lt 0 b) : Filter.Tendsto (fun (x : Real) => HDiv.hDiv (HAdd.hAdd (HMul.hMul b (exp x)) c) (HPow.hPow 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 : Real) (n : Nat) (hb : Ne 0 b) : Filter.Tendsto (fun (x : Real) => HDiv.hDiv (HPow.hPow x n) (HAdd.hAdd (HMul.hMul 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 : OrderIso Real (Set.Ioi 0).Elem

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

Equations

• Eq Real.expOrderIso (StrictMono.orderIsoOfSurjective (Set.codRestrict Real.exp (Real.lt✝ 0) Real.exp_pos) Real.expOrderIso._proof_5 Real.expOrderIso._proof_6)

theorem Real.coe_expOrderIso_apply (x : Real) : Eq (DFunLike.coe expOrderIso x).val (exp x)

theorem Real.coe_comp_expOrderIso : Eq (Function.comp Subtype.val (DFunLike.coe expOrderIso)) exp

theorem Real.range_exp : Eq (Set.range exp) (Set.Ioi 0)

theorem Real.map_exp_atTop : Eq (Filter.map exp Filter.atTop) Filter.atTop

theorem Real.comap_exp_atTop : Eq (Filter.comap exp Filter.atTop) Filter.atTop

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

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

theorem Real.comap_exp_nhdsGT_zero : Eq (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 : Eq (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 : Real → α} : Iff (Filter.Tendsto (fun (x : Real) => f (exp x)) Filter.atBot l) (Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) l)

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

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

theorem Real.isOpenEmbedding_exp : Topology.IsOpenEmbedding exp

@[deprecated Real.isOpenEmbedding_exp (since := "2024-10-18")]

theorem Real.openEmbedding_exp : Topology.IsOpenEmbedding exp

Alias of Real.isOpenEmbedding_exp.

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

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

theorem Real.isLittleO_pow_exp_atTop {n : Nat} : Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow x n) exp

theorem Real.isBigO_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → Real} : Iff (Asymptotics.IsBigO l (fun (x : α) => exp (f x)) fun (x : α) => exp (g x)) (Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l (HSub.hSub f g))

theorem Real.isTheta_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → Real} : Iff (Asymptotics.IsTheta l (fun (x : α) => exp (f x)) fun (x : α) => exp (g x)) (Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l fun (x : α) => abs (HSub.hSub (f x) (g x)))

theorem Real.isLittleO_exp_comp_exp_comp {α : Type u_1} {l : Filter α} {f g : α → Real} : Iff (Asymptotics.IsLittleO l (fun (x : α) => exp (f x)) fun (x : α) => exp (g x)) (Filter.Tendsto (fun (x : α) => HSub.hSub (g x) (f x)) l Filter.atTop)

theorem Real.isLittleO_one_exp_comp {α : Type u_1} {l : Filter α} {f : α → Real} : Iff (Asymptotics.IsLittleO l (fun (x : α) => 1) fun (x : α) => exp (f x)) (Filter.Tendsto f l Filter.atTop)

theorem Real.isBigO_one_exp_comp {α : Type u_1} {l : Filter α} {f : α → Real} : Iff (Asymptotics.IsBigO l (fun (x : α) => 1) fun (x : α) => exp (f x)) (Filter.IsBoundedUnder (fun (x1 x2 : Real) => GE.ge 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 : α → Real} : Iff (Asymptotics.IsBigO l (fun (x : α) => exp (f x)) fun (x : α) => 1) (Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le 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.isTheta_exp_comp_one {α : Type u_1} {l : Filter α} {f : α → Real} : Iff (Asymptotics.IsTheta l (fun (x : α) => exp (f x)) fun (x : α) => 1) (Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l fun (x : α) => abs (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 : Real} : Iff (Summable fun (n : Nat) => exp (HMul.hMul n.cast a)) (LT.lt a 0)

theorem Real.summable_exp_neg_nat : Summable fun (n : Nat) => exp (Neg.neg n.cast)

theorem Real.summable_pow_mul_exp_neg_nat_mul (k : Nat) {r : Real} (hr : LT.lt 0 r) : Summable fun (n : Nat) => HMul.hMul (HPow.hPow n.cast k) (exp (HMul.hMul (Neg.neg r) n.cast))

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

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

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

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

theorem Complex.comap_exp_nhdsNE : Eq (Filter.comap exp (nhdsWithin 0 (HasCompl.compl (Singleton.singleton 0)))) (Filter.comap re Filter.atBot)

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

theorem Complex.comap_exp_nhdsWithin_zero : Eq (Filter.comap exp (nhdsWithin 0 (HasCompl.compl (Singleton.singleton 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 : α → Complex} : Iff (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)

‖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 (HasCompl.compl (Singleton.singleton 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 (HasCompl.compl (Singleton.singleton 0)))

Alias of Complex.tendsto_exp_comap_re_atBot_nhdsNE.

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

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