eventually_deriv_one_sub_smoothingFn

English

For each i, the expression ε(b_i n) − ε(n) is Θ(log(b_i))/log(n)^2 as n → ∞.

Русский

Для каждого i выражение ε(b_i n) − ε(n) имеет порядок Θ(log(b_i))/log(n)^2 при n → ∞.

LaTeX

$$$$ε(b_i n) - ε(n) = Θ\left(\frac{\log(b_i)}{(\log n)^2}\right) \quad(n\to\infty).$$$$

Lean4

theorem eventually_deriv_one_sub_smoothingFn : deriv (fun x => 1 - ε x) =ᶠ[atTop] fun x => x⁻¹ / (log x ^ 2) :=
  calc
    deriv (fun x => 1 - ε x)
    _ =ᶠ[atTop] -(deriv ε) := by filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_sub] <;> aesop
    _ =ᶠ[atTop] fun x => x⁻¹ / (log x ^ 2) :=
      by
      filter_upwards [eventually_gt_atTop 1] with x hx
      simp [deriv_smoothingFn hx, neg_div]

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