not_isBigO — Mathlib

English

If f'' = o_l g' and f'' is frequently nonzero along l, then g' is not Big-O of f'' along l.

Русский

Если f'' = o_l g' и f'' принимает ненулевые значения часто вдоль l, то g' не является Большим-O по отношению к f'' вдоль l.

LaTeX

$$$\bigl(f'' = o_l g'\bigr) \land \bigl(\exists^{\mathrm{frequently}} x \in l: f''(x) \neq 0\bigr) \implies \neg\bigl(g' = O_l f''\bigr)$$$

Lean4

theorem not_isBigO (h : f'' =o[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =O[l] f'' := fun h' =>
  isLittleO_irrefl hf (h.trans_isBigO h')

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