eventually_deriv_one_add_smoothingFn

English

For each i, the ratio (ε(b_i n) − ε(n)) / (−log(b_i)/(log n)^2) tends to a nonzero constant; i.e., an asymptotic equivalence holds.

Русский

Для каждого i отношение (ε(b_i n) − ε(n)) к (−log(b_i)/(log n)^2) стремится к ненулевой константе; т.е. есть асимптотическое эквивалентное поведение.

LaTeX

$$$$ε(b_i n) - ε(n) \sim -\frac{\log(b_i)}{(\log n)^2}.$$$$

Lean4

theorem eventually_deriv_one_add_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_add] <;> aesop
    _ =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) :=
      by
      filter_upwards [eventually_gt_atTop 1] with x hx
      simp [deriv_smoothingFn hx]

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