eventually_asympBound_pos — Mathlib

English

The transformed asymptotic bound is equivalent to n^p times a factor (1 + sum …).

Русский

Переобразованное асимптотическое ограничение эквивалентно произведению n^p на множитель (1 + сумма …).

LaTeX

$$$\text{asympBound} = n^{p(a,b)} \cdot \Bigl(1 + \sum_{u

Lean4

theorem eventually_asympBound_pos : ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n := by
  filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn

Похожие утверждения