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 +∞ #

source
theorem tendsto_rpow_atTop {y : Real} (hy : LT.lt 0 y) :
Filter.Tendsto (fun (x : Real) => HPow.hPow x y) Filter.atTop Filter.atTop

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

source
theorem tendsto_rpow_neg_atTop {y : Real} (hy : LT.lt 0 y) :
Filter.Tendsto (fun (x : Real) => HPow.hPow x (Neg.neg y)) Filter.atTop (nhds 0)

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

source
theorem tendsto_rpow_atTop_of_base_lt_one (b : Real) (hb₀ : LT.lt (-1) b) (hb₁ : LT.lt b 1) :
Filter.Tendsto (fun (x : Real) => HPow.hPow b x) Filter.atTop (nhds 0)
source
theorem tendsto_rpow_atTop_of_base_gt_one (b : Real) (hb : LT.lt 1 b) :
Filter.Tendsto (fun (x : Real) => HPow.hPow b x) Filter.atBot (nhds 0)
source
theorem tendsto_rpow_atBot_of_base_lt_one (b : Real) (hb₀ : LT.lt 0 b) (hb₁ : LT.lt b 1) :
Filter.Tendsto (fun (x : Real) => HPow.hPow b x) Filter.atBot Filter.atTop
source
theorem tendsto_rpow_atBot_of_base_gt_one (b : Real) (hb : LT.lt 1 b) :
Filter.Tendsto (fun (x : Real) => HPow.hPow b x) Filter.atBot (nhds 0)
source
theorem tendsto_rpow_div_mul_add (a b c : Real) (hb : Ne 0 b) :
Filter.Tendsto (fun (x : Real) => HPow.hPow x (HDiv.hDiv a (HAdd.hAdd (HMul.hMul 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.

source
theorem tendsto_rpow_div :
Filter.Tendsto (fun (x : Real) => HPow.hPow x (HDiv.hDiv 1 x)) Filter.atTop (nhds 1)

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

source
theorem tendsto_rpow_neg_div :
Filter.Tendsto (fun (x : Real) => HPow.hPow x (HDiv.hDiv (-1) x)) Filter.atTop (nhds 1)

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

source
theorem tendsto_exp_div_rpow_atTop (s : Real) :
Filter.Tendsto (fun (x : Real) => HDiv.hDiv (Real.exp x) (HPow.hPow x s)) Filter.atTop Filter.atTop

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

source
theorem tendsto_exp_mul_div_rpow_atTop (s b : Real) (hb : LT.lt 0 b) :
Filter.Tendsto (fun (x : Real) => HDiv.hDiv (Real.exp (HMul.hMul b x)) (HPow.hPow x s)) Filter.atTop Filter.atTop

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

source
theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s b : Real) (hb : LT.lt 0 b) :
Filter.Tendsto (fun (x : Real) => HMul.hMul (HPow.hPow x s) (Real.exp (HMul.hMul (Neg.neg b) x))) Filter.atTop (nhds 0)

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

source
theorem NNReal.tendsto_rpow_atTop {y : Real} (hy : LT.lt 0 y) :
Filter.Tendsto (fun (x : NNReal) => HPow.hPow x y) Filter.atTop Filter.atTop
source
theorem ENNReal.tendsto_rpow_at_top {y : Real} (hy : LT.lt 0 y) :
Filter.Tendsto (fun (x : ENNReal) => HPow.hPow x y) (nhds Top.top) (nhds Top.top)

Asymptotic results: IsBigO, IsLittleO and IsTheta #

source
theorem Complex.isTheta_exp_arg_mul_im {α : Type u_1} {l : Filter α} {f g : α → Complex} (hl : Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l fun (x : α) => abs (g x).im) :
Asymptotics.IsTheta l (fun (x : α) => Real.exp (HMul.hMul (f x).arg (g x).im)) fun (x : α) => 1
source
theorem Complex.isBigO_cpow_rpow {α : Type u_1} {l : Filter α} {f g : α → Complex} (hl : Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l fun (x : α) => abs (g x).im) :
Asymptotics.IsBigO l (fun (x : α) => HPow.hPow (f x) (g x)) fun (x : α) => HPow.hPow (Norm.norm (f x)) (g x).re
source
theorem Complex.isTheta_cpow_rpow {α : Type u_1} {l : Filter α} {f g : α → Complex} (hl_im : Filter.IsBoundedUnder (fun (x1 x2 : Real) => LE.le x1 x2) l fun (x : α) => abs (g x).im) (hl : Filter.Eventually (fun (x : α) => Eq (f x) 0 → Eq (g x).re 0 → Eq (g x) 0) l) :
Asymptotics.IsTheta l (fun (x : α) => HPow.hPow (f x) (g x)) fun (x : α) => HPow.hPow (Norm.norm (f x)) (g x).re
source
theorem Complex.isTheta_cpow_const_rpow {α : Type u_1} {l : Filter α} {f : α → Complex} {b : Complex} (hl : Eq b.re 0 → Ne b 0 → Filter.Eventually (fun (x : α) => Ne (f x) 0) l) :
Asymptotics.IsTheta l (fun (x : α) => HPow.hPow (f x) b) fun (x : α) => HPow.hPow (Norm.norm (f x)) b.re
source
theorem Asymptotics.IsBigOWith.rpow {α : Type u_1} {r c : Real} {l : Filter α} {f g : α → Real} (h : IsBigOWith c l f g) (hc : LE.le 0 c) (hr : LE.le 0 r) (hg : l.EventuallyLE 0 g) :
IsBigOWith (HPow.hPow c r) l (fun (x : α) => HPow.hPow (f x) r) fun (x : α) => HPow.hPow (g x) r
source
theorem Asymptotics.IsBigO.rpow {α : Type u_1} {r : Real} {l : Filter α} {f g : α → Real} (hr : LE.le 0 r) (hg : l.EventuallyLE 0 g) (h : IsBigO l f g) :
IsBigO l (fun (x : α) => HPow.hPow (f x) r) fun (x : α) => HPow.hPow (g x) r
source
theorem Asymptotics.IsTheta.rpow {α : Type u_1} {r : Real} {l : Filter α} {f g : α → Real} (hr : LE.le 0 r) (hf : l.EventuallyLE 0 f) (hg : l.EventuallyLE 0 g) (h : IsTheta l f g) :
IsTheta l (fun (x : α) => HPow.hPow (f x) r) fun (x : α) => HPow.hPow (g x) r
source
theorem Asymptotics.IsLittleO.rpow {α : Type u_1} {r : Real} {l : Filter α} {f g : α → Real} (hr : LT.lt 0 r) (hg : l.EventuallyLE 0 g) (h : IsLittleO l f g) :
IsLittleO l (fun (x : α) => HPow.hPow (f x) r) fun (x : α) => HPow.hPow (g x) r
source
theorem Asymptotics.IsBigO.sqrt {α : Type u_1} {l : Filter α} {f g : α → Real} (hfg : IsBigO l f g) (hg : l.EventuallyLE 0 g) :
IsBigO l (fun (x : α) => (f x).sqrt) fun (x : α) => (g x).sqrt
source
theorem Asymptotics.IsLittleO.sqrt {α : Type u_1} {l : Filter α} {f g : α → Real} (hfg : IsLittleO l f g) (hg : l.EventuallyLE 0 g) :
IsLittleO l (fun (x : α) => (f x).sqrt) fun (x : α) => (g x).sqrt
source
theorem Asymptotics.IsTheta.sqrt {α : Type u_1} {l : Filter α} {f g : α → Real} (hfg : IsTheta l f g) (hf : l.EventuallyLE 0 f) (hg : l.EventuallyLE 0 g) :
IsTheta l (fun (x : α) => (f x).sqrt) fun (x : α) => (g x).sqrt
source
theorem Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow {𝕜 : Type u_2} [RCLike 𝕜] {g : Nat → 𝕜} {a : 𝕜} {r : Real} (hlim : Filter.Tendsto (fun (n : Nat) => HDiv.hDiv (g n) (RCLike.ofReal (HPow.hPow n.cast r))) Filter.atTop (nhds a)) :
IsBigO Filter.atTop g fun (n : Nat) => HPow.hPow n.cast r
source
theorem Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow {E : Type u_2} [SeminormedRing E] (a b c : Real) {f g : Real → E} (hf : IsBigO Filter.atTop f fun (t : Real) => HPow.hPow t a) (hg : IsBigO Filter.atTop g fun (t : Real) => HPow.hPow t b) (h : LE.le (HAdd.hAdd a b) c) :
IsBigO Filter.atTop (HMul.hMul f g) fun (t : Real) => HPow.hPow t c
source
theorem Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow {E : Type u_2} [SeminormedRing E] (a b c : Real) {f g : Nat → E} (hf : IsBigO Filter.atTop f fun (n : Nat) => HPow.hPow n.cast a) (hg : IsBigO Filter.atTop g fun (n : Nat) => HPow.hPow n.cast b) (h : LE.le (HAdd.hAdd a b) c) :
IsBigO Filter.atTop (HMul.hMul f g) fun (n : Nat) => HPow.hPow n.cast c
source
theorem isLittleO_rpow_exp_pos_mul_atTop (s : Real) {b : Real} (hb : LT.lt 0 b) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow x s) fun (x : Real) => Real.exp (HMul.hMul b x)

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

source
theorem isLittleO_zpow_exp_pos_mul_atTop (k : Int) {b : Real} (hb : LT.lt 0 b) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow x k) fun (x : Real) => Real.exp (HMul.hMul b x)

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

source
theorem isLittleO_pow_exp_pos_mul_atTop (k : Nat) {b : Real} (hb : LT.lt 0 b) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow x k) fun (x : Real) => Real.exp (HMul.hMul b x)

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

source
theorem isLittleO_rpow_exp_atTop (s : Real) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow x s) Real.exp

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

source
theorem isLittleO_exp_neg_mul_rpow_atTop {a : Real} (ha : LT.lt 0 a) (b : Real) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => Real.exp (HMul.hMul (Neg.neg a) x)) fun (x : Real) => HPow.hPow x b

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

source
theorem isLittleO_log_rpow_atTop {r : Real} (hr : LT.lt 0 r) :
Asymptotics.IsLittleO Filter.atTop Real.log fun (x : Real) => HPow.hPow x r
source
theorem isLittleO_log_rpow_rpow_atTop {s : Real} (r : Real) (hs : LT.lt 0 s) :
Asymptotics.IsLittleO Filter.atTop (fun (x : Real) => HPow.hPow (Real.log x) r) fun (x : Real) => HPow.hPow x s
source
theorem isLittleO_abs_log_rpow_rpow_nhdsGT_zero {s : Real} (r : Real) (hs : LT.lt s 0) :
Asymptotics.IsLittleO (nhdsWithin 0 (Set.Ioi 0)) (fun (x : Real) => HPow.hPow (abs (Real.log x)) r) fun (x : Real) => HPow.hPow x s
source
@[deprecated isLittleO_abs_log_rpow_rpow_nhdsGT_zero (since := "2025-03-02")]
theorem isLittleO_abs_log_rpow_rpow_nhds_zero {s : Real} (r : Real) (hs : LT.lt s 0) :
Asymptotics.IsLittleO (nhdsWithin 0 (Set.Ioi 0)) (fun (x : Real) => HPow.hPow (abs (Real.log x)) r) fun (x : Real) => HPow.hPow x s

Alias of isLittleO_abs_log_rpow_rpow_nhdsGT_zero.

source
theorem isLittleO_log_rpow_nhdsGT_zero {r : Real} (hr : LT.lt r 0) :
Asymptotics.IsLittleO (nhdsWithin 0 (Set.Ioi 0)) Real.log fun (x : Real) => HPow.hPow x r
source
@[deprecated isLittleO_log_rpow_nhdsGT_zero (since := "2025-03-02")]
theorem isLittleO_log_rpow_nhds_zero {r : Real} (hr : LT.lt r 0) :
Asymptotics.IsLittleO (nhdsWithin 0 (Set.Ioi 0)) Real.log fun (x : Real) => HPow.hPow x r

Alias of isLittleO_log_rpow_nhdsGT_zero.

source
theorem tendsto_log_div_rpow_nhdsGT_zero {r : Real} (hr : LT.lt r 0) :
Filter.Tendsto (fun (x : Real) => HDiv.hDiv (Real.log x) (HPow.hPow x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
source
@[deprecated tendsto_log_div_rpow_nhdsGT_zero (since := "2025-03-02")]
theorem tendsto_log_div_rpow_nhds_zero {r : Real} (hr : LT.lt r 0) :
Filter.Tendsto (fun (x : Real) => HDiv.hDiv (Real.log x) (HPow.hPow x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Alias of tendsto_log_div_rpow_nhdsGT_zero.

source
theorem tendsto_log_mul_rpow_nhdsGT_zero {r : Real} (hr : LT.lt 0 r) :
Filter.Tendsto (fun (x : Real) => HMul.hMul (Real.log x) (HPow.hPow x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
source
@[deprecated tendsto_log_mul_rpow_nhdsGT_zero (since := "2025-03-02")]
theorem tendsto_log_mul_rpow_nhds_zero {r : Real} (hr : LT.lt 0 r) :
Filter.Tendsto (fun (x : Real) => HMul.hMul (Real.log x) (HPow.hPow x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Alias of tendsto_log_mul_rpow_nhdsGT_zero.

source
theorem tendsto_log_mul_self_nhdsLT_zero :
Filter.Tendsto (fun (x : Real) => HMul.hMul (Real.log x) x) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)
source
@[deprecated tendsto_log_mul_self_nhdsLT_zero (since := "2025-03-02")]
theorem tendsto_log_mul_self_nhds_zero_left :
Filter.Tendsto (fun (x : Real) => HMul.hMul (Real.log x) x) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)

Alias of tendsto_log_mul_self_nhdsLT_zero.