eventually_r_le_b — Mathlib

English

There is an eventual upper bound: for all i ∈ α, 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) \le (b_i)\,n + \dfrac{n}{(\log n)^2}$ (для больших $n$)$$

Lean4

theorem eventually_r_le_b : ∀ᶠ (n : ℕ) in atTop, ∀ i, r i n ≤ (b i : ℝ) * n + (n / log n ^ 2) :=
  by
  filter_upwards [R.dist_r_b'] with n hn i
  calc
    r i n = b i * n + (r i n - b i * n) := by ring
    _ ≤ b i * n + ‖r i n - b i * n‖ := by gcongr; exact Real.le_norm_self _
    _ ≤ b i * n + n / log n ^ 2 := by gcongr; exact hn i

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