isLittleO_irrefl — Mathlib

English

If a function f'' is frequently nonzero along a filter l, then f'' is not little-o of itself along l.

Русский

Если функция f'' принимает ненулевые значения часто вдоль фильтра l, то она не является малым-o по отношению к самой себе взад вдоль l.

LaTeX

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

Lean4

theorem isLittleO_irrefl (h : ∃ᶠ x in l, f'' x ≠ 0) : ¬f'' =o[l] f'' :=
  isLittleO_irrefl' <| h.mono fun _x => norm_ne_zero_iff.mpr

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