Theta

📁 Source: Mathlib/Analysis/Asymptotics/Theta.lean

Statistics

Metric	Count
Definitions `instTransForallEventuallyEqIsTheta`, `instTransForallIsBigOIsTheta`, `instTransForallIsLittleOIsTheta`, `instTransForallIsTheta`, `instTransForallIsThetaEventuallyEq`, `instTransForallIsThetaIsBigO`, `instTransForallIsThetaIsLittleO`	7
Theorems `trans_isTheta`, `add_isTheta`, `right_isTheta_add`, `right_isTheta_add'`, `trans_isTheta`, `add_isLittleO`, `comp_fst`, `comp_snd`, `const_mul_left`, `const_mul_right`, `const_smul_left`, `const_smul_right`, `div`, `eq_zero_iff`, `fiberwise_left`, `fiberwise_right`, `finsetProd`, `inv`, `isBigO_congr_left`, `isBigO_congr_right`, `isBoundedUnder_le_iff`, `isLittleO_congr_left`, `isLittleO_congr_right`, `isTheta_congr_left`, `isTheta_congr_right`, `listProd`, `mono`, `mul`, `multisetProd`, `norm_left`, `norm_right`, `of_const_mul_left`, `of_const_mul_right`, `of_const_smul_left`, `of_const_smul_right`, `of_norm_eventuallyEq`, `of_norm_eventuallyEq_norm`, `of_norm_left`, `of_norm_right`, `pow`, `smul`, `sup`, `tendsto_norm_atTop_iff`, `tendsto_zero_iff`, `trans`, `trans_eventuallyEq`, `trans_isBigO`, `trans_isLittleO`, `zpow`, `isTheta_bot`, `isTheta_comm`, `isTheta_const_const`, `isTheta_const_const_iff`, `isTheta_const_mul_left`, `isTheta_const_mul_right`, `isTheta_const_smul_left`, `isTheta_const_smul_right`, `isTheta_inv`, `isTheta_norm_left`, `isTheta_norm_right`, `isTheta_of_div_tendsto_nhds_ne_zero`, `isTheta_refl`, `isTheta_rfl`, `isTheta_sup`, `isTheta_zero_left`, `isTheta_zero_right`, `isTheta_principal`, `isTheta`, `trans_isTheta`	69
Total	76

Asymptotics

Definitions

Name	Category	Theorems
`instTransForallEventuallyEqIsTheta` 📖	CompOp	—
`instTransForallIsBigOIsTheta` 📖	CompOp	—
`instTransForallIsLittleOIsTheta` 📖	CompOp	—
`instTransForallIsTheta` 📖	CompOp	—
`instTransForallIsThetaEventuallyEq` 📖	CompOp	—
`instTransForallIsThetaIsBigO` 📖	CompOp	—
`instTransForallIsThetaIsLittleO` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTheta_bot` 📖	mathematical	—	`IsTheta` `Bot.bot` `Filter` `Filter.instBot`	—	—
`isTheta_comm` 📖	mathematical	—	`IsTheta`	—	`IsTheta.symm`
`isTheta_const_const` 📖	mathematical	—	`IsTheta` `NormedAddCommGroup.toNorm`	—	`isBigO_const_const`
`isTheta_const_const_iff` 📖	mathematical	—	`IsTheta` `NormedAddCommGroup.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`isTheta_const_mul_left` 📖	mathematical	—	`IsTheta` `NormedField.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`isTheta_const_smul_left`
`isTheta_const_mul_right` 📖	mathematical	—	`IsTheta` `NormedField.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`isTheta_const_smul_right`
`isTheta_const_smul_left` 📖	mathematical	—	`IsTheta` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`isBigO_const_smul_left` `NormedSpace.toNormSMulClass` `isBigO_const_smul_right`
`isTheta_const_smul_right` 📖	mathematical	—	`IsTheta` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`isBigO_const_smul_right` `NormedSpace.toNormSMulClass` `isBigO_const_smul_left`
`isTheta_inv` 📖	mathematical	—	`IsTheta` `NormedField.toNorm` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv_inv` `IsTheta.inv`
`isTheta_norm_left` 📖	mathematical	—	`IsTheta` `Real` `Real.norm` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—
`isTheta_norm_right` 📖	mathematical	—	`IsTheta` `Real` `Real.norm` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—
`isTheta_of_div_tendsto_nhds_ne_zero` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`IsTheta` `NormedField.toNorm`	—	`isBigO_of_div_tendsto_nhds_of_ne_zero` `inv_div` `Filter.Tendsto.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `inv_ne_zero`
`isTheta_refl` 📖	mathematical	—	`IsTheta`	—	`isBigO_refl`
`isTheta_rfl` 📖	mathematical	—	`IsTheta`	—	`isTheta_refl`
`isTheta_sup` 📖	mathematical	—	`IsTheta` `SeminormedAddCommGroup.toNorm` `Filter` `Filter.instSup`	—	`IsTheta.mono` `le_sup_left` `le_sup_right` `IsTheta.sup`
`isTheta_zero_left` 📖	mathematical	—	`IsTheta` `SeminormedAddCommGroup.toNorm` `NormedAddCommGroup.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Filter.EventuallyEq` `Pi.instZero` `NormedAddCommGroup.toAddCommGroup`	—	—
`isTheta_zero_right` 📖	mathematical	—	`IsTheta` `NormedAddCommGroup.toNorm` `SeminormedAddCommGroup.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Filter.EventuallyEq` `Pi.instZero` `NormedAddCommGroup.toAddCommGroup`	—	`isTheta_comm` `isTheta_zero_left`

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_isTheta` 📖	—	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Asymptotics.IsTheta`	—	—	`trans`

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_isTheta` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm` `Asymptotics.IsTheta`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.IsTheta.add_isLittleO` `add_comm`
`right_isTheta_add` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsTheta` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`right_isBigO_add` `add_isBigO` `Asymptotics.isBigO_refl`
`right_isTheta_add'` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsTheta` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`right_isTheta_add` `add_comm`
`trans_isTheta` 📖	—	`Asymptotics.IsLittleO` `Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	—	—	`trans_isBigO`

Asymptotics.IsTheta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_isLittleO` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm` `Asymptotics.IsLittleO`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`trans` `symm` `Asymptotics.IsLittleO.right_isTheta_add'` `Asymptotics.IsLittleO.trans_isTheta`
`comp_fst` 📖	mathematical	`Asymptotics.IsTheta`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Asymptotics.IsBigO.comp_fst`
`comp_snd` 📖	mathematical	`Asymptotics.IsTheta`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Asymptotics.IsBigO.comp_snd`
`const_mul_left` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`Asymptotics.isTheta_const_mul_left`
`const_mul_right` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`Asymptotics.isTheta_const_mul_right`
`const_smul_left` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`Asymptotics.isTheta_const_smul_left`
`const_smul_right` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`Asymptotics.isTheta_const_smul_right`
`div` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div_eq_mul_inv` `mul` `inv`
`eq_zero_iff` 📖	mathematical	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm`	`Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Filter.Eventually.mp` `Asymptotics.IsBigO.eq_zero_imp` `Filter.Eventually.mono`
`fiberwise_left` 📖	mathematical	`Asymptotics.IsTheta` `SProd.sprod` `Filter` `Filter.instSProd`	`Filter.Eventually`	—	`Asymptotics.IsBigO.fiberwise_left`
`fiberwise_right` 📖	mathematical	`Asymptotics.IsTheta` `SProd.sprod` `Filter` `Filter.instSProd`	`Filter.Eventually`	—	`Asymptotics.IsBigO.fiberwise_right`
`finsetProd` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`Asymptotics.IsBigO.finsetProd` `isBigO` `symm`
`inv` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`Asymptotics.IsBigO.inv_rev` `Asymptotics.IsBigO.eq_zero_imp`
`isBigO_congr_left` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsBigO`	—	`trans_isBigO` `symm`
`isBigO_congr_right` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsBigO`	—	`Asymptotics.IsBigO.trans_isTheta` `symm`
`isBoundedUnder_le_iff` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	—	`Asymptotics.isBigO_const_of_ne` `one_ne_zero'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `isBigO_congr_left`
`isLittleO_congr_left` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsLittleO`	—	`trans_isLittleO` `symm`
`isLittleO_congr_right` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsLittleO`	—	`Asymptotics.IsLittleO.trans_isTheta` `symm`
`isTheta_congr_left` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	—	—	`Iff.and` `isBigO_congr_left` `isBigO_congr_right`
`isTheta_congr_right` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	—	—	`Iff.and` `isBigO_congr_right` `isBigO_congr_left`
`listProd` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Asymptotics.IsBigO.listProd` `isBigO` `symm`
`mono` 📖	—	`Asymptotics.IsTheta` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`Asymptotics.IsBigO.mono`
`mul` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`smul`
`multisetProd` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Multiset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Multiset.map`	—	`Asymptotics.IsBigO.multisetProd` `isBigO` `symm`
`norm_left` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Real` `Real.norm` `Norm.norm`	—	`Asymptotics.isTheta_norm_left`
`norm_right` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Real` `Real.norm` `Norm.norm`	—	`Asymptotics.isTheta_norm_right`
`of_const_mul_left` 📖	—	`Asymptotics.IsTheta` `NormedField.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	—	`Asymptotics.isTheta_const_mul_left`
`of_const_mul_right` 📖	—	`Asymptotics.IsTheta` `NormedField.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	—	`Asymptotics.isTheta_const_mul_right`
`of_const_smul_left` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	—	`Asymptotics.isTheta_const_smul_left`
`of_const_smul_right` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	—	`Asymptotics.isTheta_const_smul_right`
`of_norm_eventuallyEq` 📖	mathematical	`Filter.EventuallyEq` `Real` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsTheta` `Real.norm`	—	`of_norm_eventuallyEq_norm` `Filter.Eventually.mono` `norm_norm`
`of_norm_eventuallyEq_norm` 📖	mathematical	`Filter.EventuallyEq` `Real` `Norm.norm`	`Asymptotics.IsTheta`	—	`Asymptotics.IsBigO.of_bound'` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`of_norm_left` 📖	—	`Asymptotics.IsTheta` `Real` `Real.norm` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—	`Asymptotics.isTheta_norm_left`
`of_norm_right` 📖	—	`Asymptotics.IsTheta` `Real` `Real.norm` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—	`Asymptotics.isTheta_norm_right`
`pow` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`Asymptotics.IsBigO.pow` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass`
`smul` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`Asymptotics.IsBigO.smul` `NormedSpace.toIsBoundedSMul` `NormedSpace.toNormSMulClass`
`sup` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Filter` `Filter.instSup`	—	`Asymptotics.IsBigO.sup`
`tendsto_norm_atTop_iff` 📖	mathematical	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	`Filter.Tendsto` `Real` `Norm.norm` `Filter.atTop` `Real.instPreorder`	—	`Asymptotics.isLittleO_const_left_of_ne` `one_ne_zero'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `isLittleO_congr_right`
`tendsto_zero_iff` 📖	mathematical	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `isLittleO_congr_left`
`trans` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm`	—	—	`Asymptotics.IsBigO.trans`
`trans_eventuallyEq` 📖	—	`Asymptotics.IsTheta` `Filter.EventuallyEq`	—	—	`Asymptotics.IsBigO.trans_eventuallyEq` `Filter.EventuallyEq.trans_isBigO` `Filter.EventuallyEq.symm`
`trans_isBigO` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm` `Asymptotics.IsBigO`	—	—	`Asymptotics.IsBigO.trans`
`trans_isLittleO` 📖	—	`Asymptotics.IsTheta` `SeminormedAddCommGroup.toNorm` `Asymptotics.IsLittleO`	—	—	`Asymptotics.IsBigO.trans_isLittleO`
`zpow` 📖	mathematical	`Asymptotics.IsTheta` `NormedField.toNorm`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow_natCast` `pow` `zpow_negSucc` `inv`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTheta_principal` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `NormedAddGroup.toSeminormedAddGroup` `IsCompact`	`Asymptotics.IsTheta` `NormedAddGroup.toNorm` `SeminormedAddGroup.toNorm` `Filter.principal`	—	`isBigO_principal` `isBigO_rev_principal`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTheta` 📖	mathematical	`Filter.EventuallyEq`	`Asymptotics.IsTheta`	—	`trans_isTheta` `Asymptotics.isTheta_rfl`
`trans_isTheta` 📖	—	`Filter.EventuallyEq` `Asymptotics.IsTheta`	—	—	`trans_isBigO` `Asymptotics.IsBigO.trans_eventuallyEq` `symm`

---

← Back to Index