English
There exists c ∈ (0,1) such that for all large n and all i, c n ≤ r_i(n).
Русский
Существует c ∈ (0,1), такой что для больших n и для каждого i выполняется c n ≤ r_i(n).
LaTeX
$$$\exists c\in(0,1)\;\forall n\ge N,\; \forall i,\; c\,n \le r_i(n)$$$
Lean4
theorem exists_eventually_r_le_const_mul : ∃ c ∈ Set.Ioo (0 : ℝ) 1, ∀ᶠ (n : ℕ) in atTop, ∀ i, r i n ≤ c * n :=
by
let c := b (max_bi b) + (1 - b (max_bi b)) / 2
have h_max_bi_pos : 0 < b (max_bi b) := R.b_pos _
have h_max_bi_lt_one : 0 < 1 - b (max_bi b) :=
by
have : b (max_bi b) < 1 := R.b_lt_one _
linarith
have hc_pos : 0 < c := by positivity
have h₁ : 0 < (1 - b (max_bi b)) / 2 := by positivity
have hc_lt_one : c < 1 :=
calc
b (max_bi b) + (1 - b (max_bi b)) / 2
_ = b (max_bi b) * (1 / 2) + 1 / 2 := by ring
_ < 1 * (1 / 2) + 1 / 2 := by gcongr; exact R.b_lt_one _
_ = 1 := by norm_num
refine ⟨c, ⟨hc_pos, hc_lt_one⟩, ?_⟩
have hlo := isLittleO_self_div_log_id
rw [Asymptotics.isLittleO_iff] at hlo
have hlo' := hlo h₁
filter_upwards [hlo', R.eventually_r_le_b] with n hn hn'
intro i
rw [Real.norm_of_nonneg (by positivity)] at hn
simp only [Real.norm_of_nonneg (by positivity : 0 ≤ (n : ℝ))] at hn
calc
r i n ≤ b i * n + n / log n ^ 2 := by exact hn' i
_ ≤ b i * n + (1 - b (max_bi b)) / 2 * n := by gcongr
_ = (b i + (1 - b (max_bi b)) / 2) * n := by ring
_ ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * n := by gcongr; exact max_bi_le _
