div_isBoundedUnder_of_isBigO — Mathlib

English

For f,g: α→𝕜, under the hypothesis that g does not vanish asymptotically, f =O[l] g iff the norm of f/g is bounded on l.

Русский

Для функций f,g: α→𝕜, при условии, что g не обнуляется асимптотически, f =O[l] g тогда и только тогда, когда норма f/g ограничена на l.

LaTeX

$$$ (f =O[l] g) \\iff IsBoundedUnder (\\cdot ≤ \\cdot) l (\\|f \\cdot g^{-1}\\|) $$$

Lean4

theorem div_isBoundedUnder_of_isBigO {α : Type*} {l : Filter α} {f g : α → 𝕜} (h : f =O[l] g) :
    IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖ :=
  by
  obtain ⟨c, h₀, hc⟩ := h.exists_nonneg
  refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩
  rw [norm_div]
  exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

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