isBigOWith_iff_exists_eq_mul — Mathlib

English

Alternative formulation: u = o[l] v iff there exists φ with Tendsto φ to 0 and u = φ v (equivalently through l).

Русский

Альтернативная формулировка: u = o[l] v эквивалентно существованию φ с пределом 0 и u = φ v по l.

LaTeX

$$$ u =o[l] v \\iff \\exists \\phi : α \\to 𝕜, Tendsto \\phi l (\\mathcal{N} 0) ∧ u =ᶠ[l] \\phi \\cdot v $$$

Lean4

theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
    IsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v :=
  by
  constructor
  · intro h
    use fun x => u x / v x
    refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩
    simpa using div_le_of_le_mul₀ (norm_nonneg _) hc hy
  · rintro ⟨φ, hφ, h⟩
    exact isBigOWith_of_eq_mul φ hφ h

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