isLittleO_irrefl' — Mathlib

English

There exist functions f with nonzero values frequently, for which f is not little-o of itself along l.

Русский

Существуют функции, которые часто не являются мал-o самой себя вдоль л.

LaTeX

$$∃ᶠ x ∈ l, f'(x) ≠ 0 ⇒ ¬ (f' =o[l] f')$$

Lean4

theorem isLittleO_irrefl' (h : ∃ᶠ x in l, ‖f' x‖ ≠ 0) : ¬f' =o[l] f' :=
  by
  intro ho
  rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩
  rw [one_div, ← div_eq_inv_mul] at hle
  exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_ge hle

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