isBigO_iff_isBoundedUnder_le_div — Mathlib

English

If g''(x) ≠ 0 eventually, then f = O_l g'' is equivalent to IsBoundedUnder (≤) l (‖f‖/‖g''‖).

Русский

Если g''(x) ≠ 0 почти везде по l, тогда f = O_l g'' эквивалентно ограниченности отношения ‖f‖/‖g''‖ по l.

LaTeX

$$$ (\forall\!^{\!\!} x \in l, g''(x) \neq 0) \Rightarrow (f =O[l] g'' \iff IsBoundedUnder (\le) l (\|f\|/\|g''\|)). $$$

Lean4

theorem isBigO_iff_isBoundedUnder_le_div (h : ∀ᶠ x in l, g'' x ≠ 0) :
    f =O[l] g'' ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖ / ‖g'' x‖ :=
  by
  simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]
  exact exists_congr fun c => eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

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