eventually_r_ge — Mathlib

English

(1 + smoothingFn x) is asymptotically equivalent to 1 as x → ∞.

Русский

(1 + сглаживающая функция x) асимптотически эквивалентна 1 при x → ∞.

LaTeX

$$$ (1 + \varepsilon x) \sim_{[\,atTop\]} 1 $$$

Lean4

theorem eventually_r_ge (C : ℝ) : ∀ᶠ (n : ℕ) in atTop, ∀ i, C ≤ r i n :=
  by
  obtain ⟨c, hc_mem, hc⟩ := R.exists_eventually_const_mul_le_r
  filter_upwards [eventually_ge_atTop ⌈C / c⌉₊, hc] with n hn₁ hn₂ i
  have h₁ := hc_mem.1
  calc
    C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ i

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