Asymptotic equivalence up to a constant #
In this file we define Asymptotics.IsTheta l f g
(notation: f =Θ[l] g
) as
f =O[l] g ∧ g =O[l] f
, then prove basic properties of this equivalence relation.
We say that f
is Θ(g)
along a filter l
(notation: f =Θ[l] g
) if f =O[l] g
and
g =O[l] f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Asymptotics.instTransForallIsTheta = { trans := ⋯ }
Equations
- Asymptotics.instTransForallIsBigOIsTheta = { trans := ⋯ }
Equations
- Asymptotics.instTransForallIsThetaIsBigO = { trans := ⋯ }
Equations
- Asymptotics.instTransForallIsLittleOIsTheta = { trans := ⋯ }
Equations
- Asymptotics.instTransForallIsThetaIsLittleO = { trans := ⋯ }
Equations
- Asymptotics.instTransForallIsThetaEventuallyEq = { trans := ⋯ }
Equations
- Asymptotics.instTransForallEventuallyEqIsTheta = { trans := ⋯ }
Alias of the forward direction of Asymptotics.isTheta_norm_left
.
Alias of the reverse direction of Asymptotics.isTheta_norm_left
.
Alias of the reverse direction of Asymptotics.isTheta_norm_right
.
Alias of the forward direction of Asymptotics.isTheta_norm_right
.
Alias of the forward direction of Asymptotics.isTheta_const_smul_left
.
Alias of the reverse direction of Asymptotics.isTheta_const_smul_left
.
Alias of the forward direction of Asymptotics.isTheta_const_smul_right
.
Alias of the reverse direction of Asymptotics.isTheta_const_smul_right
.
Alias of the reverse direction of Asymptotics.isTheta_const_mul_left
.
Alias of the forward direction of Asymptotics.isTheta_const_mul_left
.
Alias of the reverse direction of Asymptotics.isTheta_const_mul_right
.
Alias of the forward direction of Asymptotics.isTheta_const_mul_right
.