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

source

theorem tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :

filter.tendsto (λ (x : ℝ), x ^ y) filter.at_top filter.at_top

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

source

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.

source

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.

source

theorem tendsto_rpow_div :

filter.tendsto (λ (x : ℝ), x ^ (1 / x)) filter.at_top (nhds 1)

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

source

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

source

theorem tendsto_exp_div_rpow_at_top (s : ℝ) :

filter.tendsto (λ (x : ℝ), rexp x / x ^ s) filter.at_top filter.at_top

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

source

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

filter.tendsto (λ (x : ℝ), rexp (b * x) / x ^ s) filter.at_top filter.at_top

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_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.

source

theorem nnreal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :

filter.tendsto (λ (x : nnreal), x ^ y) filter.at_top filter.at_top

source

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` #

source

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

source

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

source

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

source

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

source

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)

source