Limits and asymptotics of power functions at +∞

This file contains results about the limiting behaviour of power functions at +∞. For convenience some results on asymptotics as x → 0 (those which are not just continuity statements) are also located here.

Limits at +∞

theorem tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun (x : ℝ) => x ^ y) Filter.atTop Filter.atTop

The function x ^ y tends to +∞ at +∞ for any positive real y.

theorem tendsto_rpow_neg_nhdsGT_zero {y : ℝ} (hr : y < 0) : Filter.Tendsto (fun (x : ℝ) => x ^ y) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

theorem tendsto_rpow_neg_atTop {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun (x : ℝ) => x ^ (-y)) Filter.atTop (nhds 0)

The function x ^ (-y) tends to 0 at +∞ for any positive real y.

theorem tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b < 1) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atTop (nhds 0)

theorem tendsto_rpow_atBot_of_base_lt_one (b : ℝ) (hb₀ : 0 < b) (hb₁ : b < 1) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot Filter.atTop

theorem tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds 0)

@[deprecated tendsto_rpow_atBot_of_base_gt_one (since := "2025-08-24")]

theorem tendsto_rpow_atTop_of_base_gt_one (b : ℝ) (hb : 1 < b) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds 0)

Alias of tendsto_rpow_atBot_of_base_gt_one.

theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) : Filter.Tendsto (fun (x : ℝ) => x ^ (a / (b * x + c))) Filter.atTop (nhds 1)

The function x ^ (a / (b * x + c)) tends to 1 at +∞, for any real numbers a, b, and c such that b is nonzero.

theorem tendsto_rpow_div : Filter.Tendsto (fun (x : ℝ) => x ^ (1 / x)) Filter.atTop (nhds 1)

The function x ^ (1 / x) tends to 1 at +∞.

theorem tendsto_rpow_neg_div : Filter.Tendsto (fun (x : ℝ) => x ^ (-1 / x)) Filter.atTop (nhds 1)

The function x ^ (-1 / x) tends to 1 at +∞.

theorem tendsto_exp_div_rpow_atTop (s : ℝ) : Filter.Tendsto (fun (x : ℝ) => Real.exp x / x ^ s) Filter.atTop Filter.atTop

The function exp(x) / x ^ s tends to +∞ at +∞, for any real number s.

theorem tendsto_exp_mul_div_rpow_atTop (s b : ℝ) (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => Real.exp (b * x) / x ^ s) Filter.atTop Filter.atTop

The function exp (b * x) / x ^ s tends to +∞ at +∞, for any real s and b > 0.

theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s b : ℝ) (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => x ^ s * Real.exp (-b * x)) Filter.atTop (nhds 0)

The function x ^ s * exp (-b * x) tends to 0 at +∞, for any real s and b > 0.

theorem NNReal.tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun (x : NNReal) => x ^ y) Filter.atTop Filter.atTop

theorem ENNReal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun (x : ENNReal) => x ^ y) (nhds ⊤) (nhds ⊤)

Asymptotic results: IsBigO, IsLittleO and IsTheta

theorem Complex.isTheta_exp_arg_mul_im {α : Type u_1} {l : Filter α} {f g : α → ℂ} (hl : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => |(g x).im|) : (fun (x : α) => Real.exp ((f x).arg * (g x).im)) =Θ[l] fun (x : α) => 1

theorem Complex.isBigO_cpow_rpow {α : Type u_1} {l : Filter α} {f g : α → ℂ} (hl : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => |(g x).im|) : (fun (x : α) => f x ^ g x) =O[l] fun (x : α) => ‖f x‖ ^ (g x).re

theorem Complex.isTheta_cpow_rpow {α : Type u_1} {l : Filter α} {f g : α → ℂ} (hl_im : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => |(g x).im|) (hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0) : (fun (x : α) => f x ^ g x) =Θ[l] fun (x : α) => ‖f x‖ ^ (g x).re

theorem Complex.isTheta_cpow_const_rpow {α : Type u_1} {l : Filter α} {f : α → ℂ} {b : ℂ} (hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0) : (fun (x : α) => f x ^ b) =Θ[l] fun (x : α) => ‖f x‖ ^ b.re

theorem Asymptotics.IsBigOWith.rpow {α : Type u_1} {r c : ℝ} {l : Filter α} {f g : α → ℝ} (h : IsBigOWith c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) : IsBigOWith (c ^ r) l (fun (x : α) => f x ^ r) fun (x : α) => g x ^ r

theorem Asymptotics.IsBigO.rpow {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) : (fun (x : α) => f x ^ r) =O[l] fun (x : α) => g x ^ r

theorem Asymptotics.IsTheta.rpow {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hr : 0 ≤ r) (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) : (fun (x : α) => f x ^ r) =Θ[l] fun (x : α) => g x ^ r

theorem Asymptotics.IsLittleO.rpow {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) : (fun (x : α) => f x ^ r) =o[l] fun (x : α) => g x ^ r

theorem Asymptotics.IsBigO.sqrt {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =O[l] g) (hg : 0 ≤ᶠ[l] g) : (fun (x : α) => √(f x)) =O[l] fun (x : α) => √(g x)

theorem Asymptotics.IsLittleO.sqrt {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =o[l] g) (hg : 0 ≤ᶠ[l] g) : (fun (x : α) => √(f x)) =o[l] fun (x : α) => √(g x)

theorem Asymptotics.IsTheta.sqrt {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =Θ[l] g) (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) : (fun (x : α) => √(f x)) =Θ[l] fun (x : α) => √(g x)

theorem Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow {𝕜 : Type u_2} [RCLike 𝕜] {g : ℕ → 𝕜} {a : 𝕜} {r : ℝ} (hlim : Filter.Tendsto (fun (n : ℕ) => g n / ↑(↑n ^ r)) Filter.atTop (nhds a)) : g =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r

theorem Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow {E : Type u_2} [SeminormedRing E] (a b c : ℝ) {f g : ℝ → E} (hf : f =O[Filter.atTop] fun (t : ℝ) => t ^ a) (hg : g =O[Filter.atTop] fun (t : ℝ) => t ^ b) (h : a + b ≤ c) : (f * g) =O[Filter.atTop] fun (t : ℝ) => t ^ c

theorem Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow {E : Type u_2} [SeminormedRing E] (a b c : ℝ) {f g : ℕ → E} (hf : f =O[Filter.atTop] fun (n : ℕ) => ↑n ^ a) (hg : g =O[Filter.atTop] fun (n : ℕ) => ↑n ^ b) (h : a + b ≤ c) : (f * g) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ c

theorem Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp {a b : ℝ} (h : a ≤ b) (himp : b = 0 → a = 0) : (fun (x : ℝ) => x ^ b) =O[nhdsWithin 0 (Set.Ici 0)] fun (x : ℝ) => x ^ a

If a ≤ b, then x^b = O(x^a) as x → 0, x ≥ 0, unless b = 0 and a ≠ 0.

theorem Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le {a b : ℝ} (h : a ≤ b) (hb : b ≠ 0) : (fun (x : ℝ) => x ^ b) =O[nhdsWithin 0 (Set.Ici 0)] fun (x : ℝ) => x ^ a

If a ≤ b, b ≠ 0, then x^b = O(x^a) as x → 0, x ≥ 0.

theorem Asymptotics.IsBigO.id_rpow_of_le_one {a : ℝ} (ha : a ≤ 1) : id =O[nhdsWithin 0 (Set.Ici 0)] fun (x : ℝ) => x ^ a

If a ≤ 1, then x = O(x ^ a) as x → 0, x ≥ 0.

theorem isLittleO_rpow_exp_pos_mul_atTop (s : ℝ) {b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => x ^ s) =o[Filter.atTop] fun (x : ℝ) => Real.exp (b * x)

x ^ s = o(exp(b * x)) as x → ∞ for any real s and positive b.

theorem isLittleO_zpow_exp_pos_mul_atTop (k : ℤ) {b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => x ^ k) =o[Filter.atTop] fun (x : ℝ) => Real.exp (b * x)

x ^ k = o(exp(b * x)) as x → ∞ for any integer k and positive b.

theorem isLittleO_pow_exp_pos_mul_atTop (k : ℕ) {b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => x ^ k) =o[Filter.atTop] fun (x : ℝ) => Real.exp (b * x)

x ^ k = o(exp(b * x)) as x → ∞ for any natural k and positive b.

theorem isLittleO_rpow_exp_atTop (s : ℝ) : (fun (x : ℝ) => x ^ s) =o[Filter.atTop] Real.exp

x ^ s = o(exp x) as x → ∞ for any real s.

theorem isLittleO_exp_neg_mul_rpow_atTop {a : ℝ} (ha : 0 < a) (b : ℝ) : (fun (x : ℝ) => Real.exp (-a * x)) =o[Filter.atTop] fun (x : ℝ) => x ^ b

exp (-a * x) = o(x ^ s) as x → ∞, for any positive a and real s.

theorem isLittleO_exp_mul_rpow_of_lt (k : ℝ) {a b : ℝ} (ha' : a < b) : (fun (t : ℝ) => Real.exp (a * t) * t ^ k) =o[Filter.atTop] fun (t : ℝ) => Real.exp (b * t)

theorem isLittleO_log_rpow_atTop {r : ℝ} (hr : 0 < r) : Real.log =o[Filter.atTop] fun (x : ℝ) => x ^ r

theorem isLittleO_log_rpow_rpow_atTop {s : ℝ} (r : ℝ) (hs : 0 < s) : (fun (x : ℝ) => Real.log x ^ r) =o[Filter.atTop] fun (x : ℝ) => x ^ s

theorem isLittleO_abs_log_rpow_rpow_nhdsGT_zero {s : ℝ} (r : ℝ) (hs : s < 0) : (fun (x : ℝ) => |Real.log x| ^ r) =o[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ s

theorem isLittleO_log_rpow_nhdsGT_zero {r : ℝ} (hr : r < 0) : Real.log =o[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ r

theorem tendsto_log_div_rpow_nhdsGT_zero {r : ℝ} (hr : r < 0) : Filter.Tendsto (fun (x : ℝ) => Real.log x / x ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem tendsto_log_mul_rpow_nhdsGT_zero {r : ℝ} (hr : 0 < r) : Filter.Tendsto (fun (x : ℝ) => Real.log x * x ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem tendsto_log_mul_self_nhdsLT_zero : Filter.Tendsto (fun (x : ℝ) => Real.log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)