English
IsBigOWith is defined as the property that there exists a bound for the norm of f by a constant multiple of the norm of g along l.
Русский
IsBigOWith определяется как свойство существования границы норм функции f, зависящей константами от нормы g вдоль l.
LaTeX
$$$\text{IsBigOWith}(c, l, f, g) \equiv \forall^\! x \in l, \|f(x)\| \le c \|g(x)\|.$$$
Lean4
/-- The Landau notation `f =O[l] 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 a constant multiple of `‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided
by this definition. -/
def IsBigO :=
val_proj @wrapped✝.{}
