Documentation

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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_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_atTop_of_base_gt_one (b : ) (hb : 1 < b) :
Filter.Tendsto (fun (x : ) => b ^ x) Filter.atBot (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)
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.

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

Alias of tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero.


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 : α) => Complex.abs (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 = 0g x = 0) :
(fun (x : α) => f x ^ g x) =Θ[l] fun (x : α) => Complex.abs (f x) ^ (g x).re
theorem Complex.isTheta_cpow_const_rpow {α : Type u_1} {l : Filter α} {f : α} {b : } (hl : b.re = 0b 0∀ᶠ (x : α) in l, f x 0) :
(fun (x : α) => f x ^ b) =Θ[l] fun (x : α) => Complex.abs (f x) ^ b.re
theorem Asymptotics.IsBigOWith.rpow {α : Type u_1} {r : } {c : } {l : Filter α} {f : α} {g : α} (h : Asymptotics.IsBigOWith c l f g) (hc : 0 c) (hr : 0 r) (hg : 0 ≤ᶠ[l] g) :
Asymptotics.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 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_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_nhds_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_nhds_zero {r : } (hr : r < 0) :
Real.log =o[nhdsWithin 0 (Set.Ioi 0)] fun (x : ) => x ^ r
theorem tendsto_log_div_rpow_nhds_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_nhds_zero {r : } (hr : 0 < r) :
Filter.Tendsto (fun (x : ) => Real.log x * x ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)