English
For functions f: α → E and g: α → F, and a constant c, along a filter l the relation IsBigOWith c l f g expresses that eventually ||f(x)|| ≤ c ||g(x)||; it is the standard quantitative Big-O relation.
Русский
Для функций f: α → E и g: α → F и константы c, по фильтру l отношение IsBigOWith c l f g говорит, что в конечной стадии выполняется неравенство ||f(x)|| ≤ c ||g(x)||.
LaTeX
$$$\text{IsBigOWith}(c, l, f, g) \quad\text{means}\quad \forall^\! x\in l,\; \|f(x)\| \le c \|g(x)\|.$$$
Lean4
/-- This version of the Landau notation `IsBigOWith C l f g` where `f` and `g` are two functions on
a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by `C * ‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded by `C`, modulo division by zero issues that are
avoided by this definition. Probably you want to use `IsBigO` instead of this relation. -/
def IsBigOWith :=
val_proj @wrapped✝.{}
