English
For functions u and v into a field, u = o[l] v iff there exists φ with Tendsto φ to 0 and u = φ v (almost everywhere).
Русский
Для функций u и v в поле, u = o[l] v тогда и только тогда, когда существует φ с пределом 0 и u = φ v почти всюду.
LaTeX
$$$ u =o[l] v \\iff \\exists \\phi : α \\to 𝕜, Tendsto \\phi l (\\mathcal{N} 0) ∧ u =ᶠ[l] \\phi \\cdot v $$$
Lean4
/-- If `‖φ‖` is eventually bounded by `c`, and `u =ᶠ[l] φ * v`, then we have `IsBigOWith c u v l`.
This does not require any assumptions on `c`, which is why we keep this version along with
`IsBigOWith_iff_exists_eq_mul`. -/
theorem isBigOWith_of_eq_mul {u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c) (h : u =ᶠ[l] φ * v) :
IsBigOWith c l u v := by
simp only [IsBigOWith_def]
refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)
simp only [Pi.mul_apply]
refine (norm_mul_le _ _).trans ?_
gcongr
