eventually_one_sub_smoothingFn_gt_const

English

For c < 1, there are infinitely large natural numbers n with c < 1 − ε(n). In other words, the same tail behavior holds along the natural numbers, i.e. ε(n) → 0 as n → ∞.

Русский

Для c < 1 существуют бесконечно большие натуральные числа n такие, что c < 1 − ε(n). Другими словами, та же асимптотика участия ε(n) уходит в нуль по мере n → ∞.

LaTeX

$$$$\forall c<1:\; \forall^{\infty} n\to\infty:\; c < 1 - \varepsilon(n).$$$$

Lean4

theorem eventually_one_sub_smoothingFn_gt_const (c : ℝ) (hc : c < 1) : ∀ᶠ (n : ℕ) in atTop, c < 1 - ε n :=
  Eventually.natCast_atTop (p := fun n => c < 1 - ε n) <| eventually_one_sub_smoothingFn_gt_const_real c hc

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