Asymptotics #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We introduce these relations:
is_O_with c l f g
: "f is big O of g along l with constant c";f =O[l] g
: "f is big O of g along l";f =o[l] g
: "f is little o of g along l".
Here l
is any filter on the domain of f
and g
, which are assumed to be the same. The codomains
of f
and g
do not need to be the same; all that is needed that there is a norm associated with
these types, and it is the norm that is compared asymptotically.
The relation is_O_with c
is introduced to factor out common algebraic arguments in the proofs of
similar properties of is_O
and is_o
. Usually proofs outside of this file should use is_O
instead.
Often the ranges of f
and g
will be the real numbers, in which case the norm is the absolute
value. In general, we have
f =O[l] g ↔ (λ x, ‖f x‖) =O[l] (λ x, ‖g x‖)
,
and similarly for is_o
. But our setup allows us to use the notions e.g. with functions
to the integers, rationals, complex numbers, or any normed vector space without mentioning the
norm explicitly.
If f
and g
are functions to a normed field like the reals or complex numbers and g
is always
nonzero, we have
f =o[l] g ↔ tendsto (λ x, f x / (g x)) l (𝓝 0)
.
In fact, the right-to-left direction holds without the hypothesis on g
, and in the other direction
it suffices to assume that f
is zero wherever g
is. (This generalization is useful in defining
the Fréchet derivative.)
Definitions #
This version of the Landau notation is_O_with 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 is_O
instead of this relation.
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.
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 an arbitrarily small constant
multiple of ‖g‖
. In other words, ‖f‖ / ‖g‖
tends to 0
along l
, modulo division by zero
issues that are avoided by this definition.
Conversions #
f = O(g)
if and only if is_O_with c f g
for all sufficiently large c
.
Subsingleton #
Congruence #
Filter operations and transitivity #
Simplification : norm, abs #
Alias of the reverse direction of asymptotics.is_O_with_norm_right
.
Alias of the forward direction of asymptotics.is_O_with_norm_right
.
Alias of the forward direction of asymptotics.is_O_with_abs_right
.
Alias of the reverse direction of asymptotics.is_O_with_abs_right
.
Alias of the forward direction of asymptotics.is_O_with_norm_left
.
Alias of the reverse direction of asymptotics.is_O_with_norm_left
.
Alias of the forward direction of asymptotics.is_O_with_abs_left
.
Alias of the reverse direction of asymptotics.is_O_with_abs_left
.
Alias of the forward direction of asymptotics.is_O_with_norm_norm
.
Alias of the reverse direction of asymptotics.is_O_with_norm_norm
.
Alias of the forward direction of asymptotics.is_O_with_abs_abs
.
Alias of the reverse direction of asymptotics.is_O_with_abs_abs
.
Alias of the reverse direction of asymptotics.is_O_norm_norm
.
Alias of the forward direction of asymptotics.is_O_norm_norm
.
Alias of the forward direction of asymptotics.is_o_norm_norm
.
Alias of the reverse direction of asymptotics.is_o_norm_norm
.
Simplification: negate #
Alias of the reverse direction of asymptotics.is_O_with_neg_right
.
Alias of the forward direction of asymptotics.is_O_with_neg_right
.
Alias of the forward direction of asymptotics.is_O_with_neg_left
.
Alias of the reverse direction of asymptotics.is_O_with_neg_left
.
Product of functions (right) #
Addition and subtraction #
Zero, one, and other constants #
Alias of the reverse direction of asymptotics.is_O_one_iff
.