eventually_one_add_smoothingFn_pos

English

The derivative of 1 − ε is o(1/x) at infinity, and is Theta of 1/x after appropriate normalization.

Русский

Производная 1 − ε есть o(1/x) в бесконечности, а после нормировки имеет порядок Θ(1/x).

LaTeX

$$$$\text{isLittleO}(\frac{d}{dx}(1-\varepsilon(x)), \frac{1}{x})\quad (x\to\infty),$$$$

Lean4

theorem eventually_one_add_smoothingFn_pos : ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε n :=
  by
  have h₁ := isLittleO_smoothingFn_one
  rw [isLittleO_iff] at h₁
  refine Eventually.natCast_atTop (p := fun n => 0 < 1 + ε n) ?_
  filter_upwards [h₁ (by simp : (0 : ℝ) < 1 / 2), eventually_gt_atTop 1] with x _ hx'
  have : 0 < log x := Real.log_pos hx'
  change 0 < 1 + 1 / log x
  positivity

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