isLittleO_iff_tendsto' — Mathlib

English

If f = o[l] g in a module setting, then the smul by the inverse of g converges to zero: g(x)⁻¹ • f(x) → 0.

Русский

Если f = o[l] g, то g(x)⁻¹ · f(x) стремится к нулю при x → l.

LaTeX

$$$ f =o[l] g \\Rightarrow \\text{Tendsto} (\\lambda x. (g(x))^{-1} \\cdot f(x))\\ l\\ (\\mathcal{N} 0) $$$

Lean4

theorem isLittleO_iff_tendsto' {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
    f =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0) :=
  ⟨IsLittleO.tendsto_div_nhds_zero, fun h =>
    (((isLittleO_one_iff _).mpr h).mul_isBigO (isBigO_refl g l)).congr' (hgf.mono fun _x => div_mul_cancel_of_imp)
      (Eventually.of_forall fun _x => one_mul _)⟩

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