isLittleO_iff_tendsto — Mathlib

English

If IsBigOWith(c, l, u, v) holds and c ≥ 0, then there exists φ such that ‖φ‖ ≤ c and u = φ⋅v eventually.

Русский

Если IsBigOWith(c, l, u, v) выполняется и c ≥ 0, существует φ: α→𝕜, такое что по l выполняется ‖φ‖ ≤ c и u = φ·v почти всюду.

LaTeX

$$$ IsBigOWith\\ c\\ l\\ u\\ v \\Rightarrow \\exists \\phi : α \\to 𝕜, (∀ᶠ x \\in l, \\|\\phi(x)\\| \\le c) \\land u =ᶠ[l] \\phi \\cdot v $$$

Lean4

theorem isLittleO_iff_tendsto {f g : α → 𝕜} (hgf : ∀ x, g x = 0 → f x = 0) :
    f =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0) :=
  isLittleO_iff_tendsto' (Eventually.of_forall hgf)

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