asympBound_pos — Mathlib

English

The asymptotic bound is positive for n > 0 under suitable conditions on g and the Akra–Bazzi data.

Русский

Асимптотическое ограничение положительно для n>0 при подходящих условиях на g и данные Ака-Бази.

LaTeX

$$$0 < \text{asympBound}(g,a,b;n) \quad \text{for } n>0$ (under hypotheses).$$

Lean4

theorem asympBound_pos (n : ℕ) (hn : 0 < n) : 0 < asympBound g a b n := by
  calc
    0 < (n : ℝ) ^ p a b * (1 + 0) := by aesop (add safe Real.rpow_pos_of_pos)
    _ ≤ asympBound g a b n := by
      simp only [asympBound_def']
      gcongr n ^ p a b * (1 + ?_)
      have := R.g_nonneg
      aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

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