Asymptotics #
We introduce these relations:
IsBigOWith 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 IsBigOWith c
is introduced to factor out common algebraic arguments in the proofs of
similar properties of IsBigO
and IsLittleO
. Usually proofs outside of this file should use
IsBigO
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 ↔ (fun x ↦ ‖f x‖) =O[l] (fun x ↦ ‖g x‖)
,
and similarly for IsLittleO
. 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 (fun 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 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.
Instances For
Definition of IsBigOWith
. We record it in a lemma as IsBigOWith
is irreducible.
Alias of the forward direction of Asymptotics.isBigOWith_iff
.
Definition of IsBigOWith
. We record it in a lemma as IsBigOWith
is irreducible.
Alias of the reverse direction of Asymptotics.isBigOWith_iff
.
Definition of IsBigOWith
. We record it in a lemma as IsBigOWith
is irreducible.
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.
Equations
- f =O[l] g = ∃ (c : ℝ), Asymptotics.IsBigOWith c l f g
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definition of IsBigO
in terms of filters, with the constant in the lower bound.
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.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of the forward direction of Asymptotics.isLittleO_iff_forall_isBigOWith
.
Definition of IsLittleO
in terms of IsBigOWith
.
Alias of the reverse direction of Asymptotics.isLittleO_iff_forall_isBigOWith
.
Definition of IsLittleO
in terms of IsBigOWith
.
Alias of the forward direction of Asymptotics.isLittleO_iff
.
Definition of IsLittleO
in terms of filters.
Alias of the reverse direction of Asymptotics.isLittleO_iff
.
Definition of IsLittleO
in terms of filters.
Conversions #
f = O(g)
if and only if IsBigOWith c f g
for all sufficiently large c
.
f = O(g)
if and only if ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖
for all sufficiently large c
.
Subsingleton #
Congruence #
Filter operations and transitivity #
Equations
- Asymptotics.transIsBigOIsBigO = { trans := ⋯ }
Equations
- Asymptotics.transIsLittleOIsBigO = { trans := ⋯ }
Equations
- Asymptotics.transIsBigOIsLittleO = { trans := ⋯ }
Simplification : norm, abs #
Alias of the reverse direction of Asymptotics.isBigOWith_norm_right
.
Alias of the forward direction of Asymptotics.isBigOWith_norm_right
.
Alias of the reverse direction of Asymptotics.isBigOWith_abs_right
.
Alias of the forward direction of Asymptotics.isBigOWith_abs_right
.
Alias of the reverse direction of Asymptotics.isBigO_norm_right
.
Alias of the forward direction of Asymptotics.isBigO_norm_right
.
Alias of the reverse direction of Asymptotics.isLittleO_norm_right
.
Alias of the forward direction of Asymptotics.isLittleO_norm_right
.
Alias of the forward direction of Asymptotics.isBigOWith_norm_left
.
Alias of the reverse direction of Asymptotics.isBigOWith_norm_left
.
Alias of the forward direction of Asymptotics.isBigOWith_abs_left
.
Alias of the reverse direction of Asymptotics.isBigOWith_abs_left
.
Alias of the forward direction of Asymptotics.isBigO_norm_left
.
Alias of the reverse direction of Asymptotics.isBigO_norm_left
.
Alias of the reverse direction of Asymptotics.isLittleO_norm_left
.
Alias of the forward direction of Asymptotics.isLittleO_norm_left
.
Alias of the reverse direction of Asymptotics.isBigOWith_norm_norm
.
Alias of the forward direction of Asymptotics.isBigOWith_norm_norm
.
Alias of the forward direction of Asymptotics.isBigOWith_abs_abs
.
Alias of the reverse direction of Asymptotics.isBigOWith_abs_abs
.
Alias of the reverse direction of Asymptotics.isBigO_norm_norm
.
Alias of the forward direction of Asymptotics.isBigO_norm_norm
.
Alias of the forward direction of Asymptotics.isBigO_abs_abs
.
Alias of the reverse direction of Asymptotics.isBigO_abs_abs
.
Alias of the reverse direction of Asymptotics.isLittleO_norm_norm
.
Alias of the forward direction of Asymptotics.isLittleO_norm_norm
.
Alias of the forward direction of Asymptotics.isLittleO_abs_abs
.
Alias of the reverse direction of Asymptotics.isLittleO_abs_abs
.
Simplification: negate #
Alias of the forward direction of Asymptotics.isBigOWith_neg_right
.
Alias of the reverse direction of Asymptotics.isBigOWith_neg_right
.
Alias of the forward direction of Asymptotics.isBigO_neg_right
.
Alias of the reverse direction of Asymptotics.isBigO_neg_right
.
Alias of the forward direction of Asymptotics.isLittleO_neg_right
.
Alias of the reverse direction of Asymptotics.isLittleO_neg_right
.
Alias of the reverse direction of Asymptotics.isBigOWith_neg_left
.
Alias of the forward direction of Asymptotics.isBigOWith_neg_left
.
Alias of the reverse direction of Asymptotics.isBigO_neg_left
.
Alias of the forward direction of Asymptotics.isBigO_neg_left
.
Alias of the reverse direction of Asymptotics.isLittleO_neg_left
.
Alias of the forward direction of Asymptotics.isLittleO_neg_left
.
Product of functions (right) #
Addition and subtraction #
Zero, one, and other constants #
Alias of the reverse direction of Asymptotics.isBigO_one_iff
.
The condition f = O[𝓝[≠] a] 1
is equivalent to f = O[𝓝 a] 1
.
(fun x ↦ c) =O[l] f
if and only if f
is bounded away from zero.
Multiplication by a constant #
Multiplication #
Inverse #
Scalar multiplication #
Sum #
Relation between f = o(g)
and f / g → 0
#
Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto'
.
Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto
.
Eventually (u / v) * v = u #
If u
and v
are linked by an IsBigOWith
relation, then we
eventually have (u / v) * v = u
, even if v
vanishes.
Equivalent definitions of the form ∃ φ, u =ᶠ[l] φ * v
in a NormedField
. #
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
.
Alias of the forward direction of Asymptotics.isBigO_iff_exists_eq_mul
.
Alias of the forward direction of Asymptotics.isLittleO_iff_exists_eq_mul
.
Miscellaneous lemmas #
If f x = O(g x)
along cofinite
, then there exists a positive constant C
such that
‖f x‖ ≤ C * ‖g x‖
whenever g x ≠ 0
.
Alias of Asymptotics.IsBigO.natCast_atTop
.
Alias of Asymptotics.IsLittleO.natCast_atTop
.
Transfer IsBigOWith
over a PartialHomeomorph
.
Transfer IsBigO
over a PartialHomeomorph
.
Transfer IsLittleO
over a PartialHomeomorph
.
Transfer IsBigOWith
over a Homeomorph
.
The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.