isBigO_iff_exists_eq_mul — Mathlib

English

Alternative presentation: for any c ≥ 0, IsBigOWith c l u v implies there exists φ with bound and matching multiplicative form.

Русский

Альтернативая формулировка: для любого c ≥ 0 IsBigOWith c l u v приводит к существованию φ с ограничением и соответствующей формой умножения.

LaTeX

$$$ IsBigOWith\\ c\\ l\\ u\\ v \\Rightarrow \\Exists \\phi : α \\to 𝕜, (∀ᶠ x in l, \\|\\phi x\\| ≤ c) ∧ u =ᶠ[l] φ \\cdot v $$$

Lean4

theorem isBigO_iff_exists_eq_mul : u =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v :=
  by
  constructor
  · rintro h
    rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
    rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩
    exact ⟨φ, ⟨c, hφ⟩, huvφ⟩
  · rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩
    exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

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