eventually_asympBound_r_pos — Mathlib

English

The equivalent form of sumTransform aligns with the Akra–Bazzi decomposition.

Русский

Эквивалентная форма sumTransform согласуется с разложением Ака-Бази.

LaTeX

$$$\text{sumTransform}(p,g;n_0,n) = n^{p} \biggl(\sum_{u=n_0}^{n-1} \dfrac{g(u)}{u^{p+1}}\biggr)$$$

Lean4

theorem eventually_asympBound_r_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < asympBound g a b (r i n) :=
  by
  rw [Filter.eventually_all]
  exact fun i => (R.tendsto_atTop_r i).eventually R.eventually_asympBound_pos

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