ExponentAsymptotics.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Variable-exponent comparisons at a vanishing positive base

The affine-label construction uses exponent sequences rather than fixed exponents. These lemmas justify comparison when the limiting exponents have a strict gap, without replacing a variable power by the power of its limit.

theorem OAI.Problem326.tendsto_rpow_variable_zero line 23

Source documentation

A positive limiting exponent makes a power of a vanishing base vanish.

theorem tendsto_rpow_variable_zero
    (hh : Tendsto h l (𝓝 0)) (hp : Tendsto p l (𝓝 a)) (ha : 0 < a) :
    Tendsto (fun n => h n ^ p n) l (𝓝 0) := by
…

theorem OAI.Problem326.tendsto_rpow_div_rpow_zero_of_gap line 29

Source documentation

A strict limiting exponent gap gives a vanishing quotient of powers.

theorem tendsto_rpow_div_rpow_zero_of_gap
    (hpos : ∀ᶠ n in l, 0 < h n)
    (hh : Tendsto h l (𝓝 0))
    (hp : Tendsto p l (𝓝 a)) (hq : Tendsto q l (𝓝 b)) (hgap : b < a) :
    Tendsto (fun n => h n ^ p n / h n ^ q n) l (𝓝 0) := by
…

theorem OAI.Problem326.isLittleO_rpow_variable_of_gap line 40

Source documentation

Little-oh comparison remains valid for converging, variable exponents.

theorem isLittleO_rpow_variable_of_gap
    (hpos : ∀ᶠ n in l, 0 < h n)
    (hh : Tendsto h l (𝓝 0))
    (hp : Tendsto p l (𝓝 a)) (hq : Tendsto q l (𝓝 b)) (hgap : b < a) :
    (fun n => h n ^ p n) =o[l] (fun n => h n ^ q n) := by
…

theorem OAI.Problem326.tendsto_rpow_div_rpow_atTop_of_gap line 51

Source documentation

Reversing the strict limiting gap makes the quotient diverge to infinity.

theorem tendsto_rpow_div_rpow_atTop_of_gap
    (hpos : ∀ᶠ n in l, 0 < h n)
    (hh : Tendsto h l (𝓝 0))
    (hp : Tendsto p l (𝓝 a)) (hq : Tendsto q l (𝓝 b)) (hgap : a < b) :
    Tendsto (fun n => h n ^ p n / h n ^ q n) l atTop := by
…

theorem OAI.Problem326.exponent_le_of_eventually_rpow_le line 65

Source documentation

Eventual domination of powers forces the reverse order on limiting exponents.

theorem exponent_le_of_eventually_rpow_le [NeBot l]
    (hpos : ∀ᶠ n in l, 0 < h n)
    (hh : Tendsto h l (𝓝 0))
    (hp : Tendsto p l (𝓝 a)) (hq : Tendsto q l (𝓝 b))
    {C : ℝ} (hbound : ∀ᶠ n in l, h n ^ p n ≤ C * h n ^ q n) :
    b ≤ a := by
…

theorem OAI.Problem326.exponent_le_of_isBigO_rpow line 80

Source documentation

The big-oh version of the limiting exponent obstruction.

theorem exponent_le_of_isBigO_rpow [NeBot l]
    (hpos : ∀ᶠ n in l, 0 < h n)
    (hh : Tendsto h l (𝓝 0))
    (hp : Tendsto p l (𝓝 a)) (hq : Tendsto q l (𝓝 b))
    (hbound : (fun n => h n ^ p n) =O[l] (fun n => h n ^ q n)) :
    b ≤ a := by
…

theorem OAI.Problem326.eventually_pos_rpow_add_isLittleO line 92

Source documentation

A positive leading power remains positive under a little-oh perturbation.

theorem eventually_pos_rpow_add_isLittleO {r : α → ℝ} {C : ℝ}
    (hpos : ∀ᶠ n in l, 0 < h n) (hC : 0 < C)
    (hr : r =o[l] (fun n => h n ^ q n)) :
    ∀ᶠ n in l, 0 < C * h n ^ q n + r n := by
…

theorem OAI.Problem326.eventually_neg_neg_rpow_add_isLittleO line 104

Source documentation

The corresponding negative leading term stays strictly negative.

theorem eventually_neg_neg_rpow_add_isLittleO {r : α → ℝ} {C : ℝ}
    (hpos : ∀ᶠ n in l, 0 < h n) (hC : 0 < C)
    (hr : r =o[l] (fun n => h n ^ q n)) :
    ∀ᶠ n in l, -C * h n ^ q n + r n < 0 := by
…

theorem OAI.Problem326.isLittleO_sum_mul_rpow_variable_of_gap line 114

Source documentation

A finite linear combination of powers with larger limiting exponents is little-oh of the comparison power. Coefficients need not be positive.

theorem isLittleO_sum_mul_rpow_variable_of_gap {ι : Type uIota}
    (s : Finset ι) (c : ι → ℝ) {p : α → ι → ℝ} {a : ι → ℝ}
    (hpos : ∀ᶠ n in l, 0 < h n) (hh : Tendsto h l (𝓝 0))
    (hp : ∀ i ∈ s, Tendsto (fun n => p n i) l (𝓝 (a i)))
    (hq : Tendsto q l (𝓝 b)) (hgap : ∀ i ∈ s, b < a i) :
    (fun n => ∑ i ∈ s, c i * h n ^ p n i) =o[l] (fun n => h n ^ q n) := by
…