not_isLittleO — Mathlib

English

If f'' = O_l g' and f'' is frequently nonzero along l, then g' is not little-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_isLittleO (h : f'' =O[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =o[l] f'' := fun h' =>
  isLittleO_irrefl hf (h.trans_isLittleO h')

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