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)
The function x ^ (1 / x)
tends to 1
at +∞
.
The function x ^ (-1 / x)
tends to 1
at +∞
.
The function exp(x) / x ^ s
tends to +∞
at +∞
, for any real number s
.
The function exp (b * x) / x ^ s
tends to +∞
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