English
There exists a positive constant c such that for every i ∈ α, r_i(n) ≥ c n for all sufficiently large n, where c = b(min_i b)/2.
Русский
Существует положительная константа c такая, что для каждого i ∈ α, r_i(n) ≥ c n при достаточно large n, где c = b(min_i b)/2.
LaTeX
$$$\exists c>0\;\exists N\;\forall n\ge N\; \forall i,\; r_i(n) \ge c\,n$$$
Lean4
theorem eventually_b_le_r : ∀ᶠ (n : ℕ) in atTop, ∀ i, (b i : ℝ) * n - (n / log n ^ 2) ≤ r i n :=
by
filter_upwards [R.dist_r_b'] with n hn i
have h₁ : 0 ≤ b i := le_of_lt <| R.b_pos _
rw [sub_le_iff_le_add, add_comm, ← sub_le_iff_le_add]
calc
(b i : ℝ) * n - r i n
_ = ‖b i * n‖ - ‖(r i n : ℝ)‖ := by simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]
_ ≤ ‖(b i * n : ℝ) - r i n‖ := (norm_sub_norm_le _ _)
_ = ‖(r i n : ℝ) - b i * n‖ := (norm_sub_rev _ _)
_ ≤ n / log n ^ 2 := hn i
