English
For hn > 0, the interval Ico(⌊b(min_bi b)/2 · n⌋₊, n) is nonempty for all n > 0, ensuring a nontrivial base in the Akra–Bazzi induction step.
Русский
Пусть h_n > 0; промежуток Ico(⌊b(min_bi b)/2 · n⌋₊, n) непуст для любого n > 0, что обеспечивает ненулевой базовый шаг индукции Акры–Баззи.
LaTeX
$$$\\text{If } 0 < n,\\ \\mathrm{Ico}\\left(\\left\\lfloor \\frac{b\\big(\\min_i b\\big)}{2}\\,n\\right\\rfloor_+ , n\\right) \\neq \\varnothing.$$$
Lean4
theorem base_nonempty {n : ℕ} (hn : 0 < n) : (Finset.Ico (⌊b (min_bi b) / 2 * n⌋₊) n).Nonempty :=
by
let b' := b (min_bi b)
have hb_pos : 0 < b' := R.b_pos _
simp_rw [Finset.nonempty_Ico]
have :=
calc
⌊b' / 2 * n⌋₊ ≤ b' / 2 * n := by exact Nat.floor_le (by positivity)
_ < 1 / 2 * n := by gcongr; exact R.b_lt_one (min_bi b)
_ ≤ 1 * n := by gcongr; norm_num
_ = n := by simp
exact_mod_cast this
