isBigO_pure — Mathlib

English

Equivalence between IsBigO l f'' g'' and the corresponding equality for pure filter (i.e., analysis via isBigO with pure).

Русский

Эквивалентность между IsBigO l f'' g'' и соответствующим равенством через чистый фильтр.

LaTeX

$$IsBigO l f'' g''$$

Lean4

@[simp]
theorem isBigO_pure {x} : f'' =O[pure x] g'' ↔ g'' x = 0 → f'' x = 0 :=
  calc
    f'' =O[pure x] g'' ↔ (fun _y : α => f'' x) =O[pure x] fun _ => g'' x := isBigO_congr rfl rfl
    _ ↔ g'' x = 0 → f'' x = 0 := isBigO_const_const_iff _

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