isLittleO_const_left_of_ne — 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)\\| ≤ c) ∧ u =ᶠ[l] φ \\cdot v $$$

Lean4

theorem isLittleO_const_left_of_ne {c : E''} (hc : c ≠ 0) : (fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop :=
  by
  simp only [← isLittleO_one_left_iff ℝ]
  exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO, (isBigO_const_one ℝ c l).trans_isLittleO⟩

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