mathlib3 documentation

analysis.special_functions.pow.asymptotics

Limits and asymptotics of power functions at +∞ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_at_top {y : } (hy : 0 < y) :

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

theorem tendsto_rpow_neg_at_top {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ), x ^ -y) filter.at_top (nhds 0)

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

theorem tendsto_rpow_div_mul_add (a b c : ) (hb : 0 b) :
filter.tendsto (λ (x : ), x ^ (a / (b * x + c))) filter.at_top (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 (λ (x : ), x ^ (1 / x)) filter.at_top (nhds 1)

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

theorem tendsto_rpow_neg_div  :
filter.tendsto (λ (x : ), x ^ ((-1) / x)) filter.at_top (nhds 1)

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

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

theorem tendsto_exp_mul_div_rpow_at_top (s b : ) (hb : 0 < b) :

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

theorem tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 (s b : ) (hb : 0 < b) :
filter.tendsto (λ (x : ), x ^ s * rexp (-b * x)) filter.at_top (nhds 0)

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

theorem ennreal.tendsto_rpow_at_top {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), x ^ y) (nhds ) (nhds )

Asymptotic results: is_O, is_o and is_Theta #

theorem complex.is_Theta_exp_arg_mul_im {α : Type u_1} {l : filter α} {f g : α } (hl : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) :
(λ (x : α), rexp ((f x).arg * (g x).im)) =Θ[l] λ (x : α), 1
theorem complex.is_O_cpow_rpow {α : Type u_1} {l : filter α} {f g : α } (hl : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) :
(λ (x : α), f x ^ g x) =O[l] λ (x : α), complex.abs (f x) ^ (g x).re
theorem complex.is_Theta_cpow_rpow {α : Type u_1} {l : filter α} {f g : α } (hl_im : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) (hl : ∀ᶠ (x : α) in l, f x = 0 (g x).re = 0 g x = 0) :
(λ (x : α), f x ^ g x) =Θ[l] λ (x : α), complex.abs (f x) ^ (g x).re
theorem complex.is_Theta_cpow_const_rpow {α : Type u_1} {l : filter α} {f : α } {b : } (hl : b.re = 0 b 0 (∀ᶠ (x : α) in l, f x 0)) :
(λ (x : α), f x ^ b) =Θ[l] λ (x : α), complex.abs (f x) ^ b.re
theorem asymptotics.is_O_with.rpow {α : Type u_1} {r c : } {l : filter α} {f g : α } (h : asymptotics.is_O_with c l f g) (hc : 0 c) (hr : 0 r) (hg : 0 ≤ᶠ[l] g) :
asymptotics.is_O_with (c ^ r) l (λ (x : α), f x ^ r) (λ (x : α), g x ^ r)
theorem asymptotics.is_O.rpow {α : Type u_1} {r : } {l : filter α} {f g : α } (hr : 0 r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) :
(λ (x : α), f x ^ r) =O[l] λ (x : α), g x ^ r
theorem asymptotics.is_o.rpow {α : Type u_1} {r : } {l : filter α} {f g : α } (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) :
(λ (x : α), f x ^ r) =o[l] λ (x : α), g x ^ r
theorem is_o_rpow_exp_pos_mul_at_top (s : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ s) =o[filter.at_top] λ (x : ), rexp (b * x)

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

theorem is_o_zpow_exp_pos_mul_at_top (k : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ k) =o[filter.at_top] λ (x : ), rexp (b * x)

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

theorem is_o_pow_exp_pos_mul_at_top (k : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ k) =o[filter.at_top] λ (x : ), rexp (b * x)

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

theorem is_o_rpow_exp_at_top (s : ) :
(λ (x : ), x ^ s) =o[filter.at_top] rexp

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

theorem is_o_exp_neg_mul_rpow_at_top {a : } (ha : 0 < a) (b : ) :
(λ (x : ), rexp (-a * x)) =o[filter.at_top] λ (x : ), x ^ b

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

theorem is_o_log_rpow_at_top {r : } (hr : 0 < r) :
theorem is_o_log_rpow_rpow_at_top {s : } (r : ) (hs : 0 < s) :
(λ (x : ), real.log x ^ r) =o[filter.at_top] λ (x : ), x ^ s
theorem is_o_abs_log_rpow_rpow_nhds_zero {s : } (r : ) (hs : s < 0) :
(λ (x : ), |real.log x| ^ r) =o[nhds_within 0 (set.Ioi 0)] λ (x : ), x ^ s
theorem is_o_log_rpow_nhds_zero {r : } (hr : r < 0) :
real.log =o[nhds_within 0 (set.Ioi 0)] λ (x : ), x ^ r
theorem tendsto_log_div_rpow_nhds_zero {r : } (hr : r < 0) :
filter.tendsto (λ (x : ), real.log x / x ^ r) (nhds_within 0 (set.Ioi 0)) (nhds 0)
theorem tendsto_log_mul_rpow_nhds_zero {r : } (hr : 0 < r) :
filter.tendsto (λ (x : ), real.log x * x ^ r) (nhds_within 0 (set.Ioi 0)) (nhds 0)