dist_r_b' — Mathlib

English

For every i ∈ α, the distance between r_i(n) and b_i n is uniformly small: ‖(r_i(n) − b_i n)‖ ≤ n / (log n)^2 for large n.

Русский

Для каждого i ∈ α расстояние между r_i(n) и b_i n ограничено сверху на величину n / (log n)^2 при больших n.

LaTeX

$$$\forall i,\; \| r_i(n) - b_i n \| \le \dfrac{n}{(\log n)^2}$$$

Lean4

theorem dist_r_b' : ∀ᶠ n in atTop, ∀ i, ‖(r i n : ℝ) - b i * n‖ ≤ n / log n ^ 2 :=
  by
  rw [Filter.eventually_all]
  intro i
  simpa using IsLittleO.eventuallyLE (R.dist_r_b i)

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