PowerAsymptotics.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.tendsto_rpow_ratio_zero line 16

Source documentation

A positive gap between limiting exponents makes the ratio of powers tend to zero, even when the numerator's exponent varies.

theorem tendsto_rpow_ratio_zero {α : Type uAlpha} {l : Filter α}
    {h p : α → ℝ} {p₀ q : ℝ}
    (hh : Tendsto h l (𝓝 0)) (hhpos : ∀ᶠ n in l, 0 < h n)
    (hp : Tendsto p l (𝓝 p₀)) (hgap : q < p₀) :
    Tendsto (fun n => h n ^ p n / h n ^ q) l (𝓝 0) := by
…

theorem OAI.Problem326.tendsto_rpow_ratio_atTop line 28

Source documentation

A negative limiting exponent gap makes the same ratio diverge.

theorem tendsto_rpow_ratio_atTop {α : Type uAlpha} {l : Filter α}
    {h p : α → ℝ} {p₀ q : ℝ}
    (hh : Tendsto h l (𝓝 0)) (hhpos : ∀ᶠ n in l, 0 < h n)
    (hp : Tendsto p l (𝓝 p₀)) (hgap : p₀ < q) :
    Tendsto (fun n => h n ^ p n / h n ^ q) l atTop := by
…

theorem OAI.Problem326.varying_rpow_isLittleO line 45

Source documentation

Little-o form of the varying-exponent comparison.

theorem varying_rpow_isLittleO {α : Type uAlpha} {l : Filter α}
    {h p : α → ℝ} {p₀ q : ℝ}
    (hh : Tendsto h l (𝓝 0)) (hhpos : ∀ᶠ n in l, 0 < h n)
    (hp : Tendsto p l (𝓝 p₀)) (hgap : q < p₀) :
    (fun n => h n ^ p n) =o[l] (fun n => h n ^ q) := by
…

theorem OAI.Problem326.rpow_isLittleO_at_zero line 57
Source documentation
Fixed distinct powers are asymptotically separated at zero from the right.
```
theorem rpow_isLittleO_at_zero {p q : ℝ} (hpq : q < p) :
    (fun h : ℝ => h ^ p) =o[𝓝[>] 0] (fun h => h ^ q) :=
…
```
theorem OAI.Problem326.tendsto_log_ratio_zero line 63
Source documentation
The exponents corresponding to any fixed initial state tend to zero.
```
theorem tendsto_log_ratio_zero (x : ℝ) :
    Tendsto (fun h : ℝ => Real.log x / Real.log h) (𝓝[>] 0) (𝓝 0) :=
…
```

theorem OAI.Problem326.exists_small_parameter_of_constants line 69

Source documentation

One small parameter simultaneously controls every fixed initial exponent and a prescribed rate-separation inequality.

theorem exists_small_parameter_of_constants {ι : Type uIota} [Finite ι] (x : ι → ℝ)
    {H h₀ B : ℝ} (hH : 0 < H) (hh₀ : 0 < h₀) (hB : 0 < B) (A : ℝ) :
    ∃ h : ℝ, 0 < h ∧ h < h₀ ∧ h < 1 ∧
      (∀ i, |Real.log (x i) / Real.log h| < H) ∧ h ^ H * A < B := by
…