AsymptoticEquivalent

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

Statistics

Metric	Count
Definitions `transEventuallyEqIsEquivalent`, `transIsBigOIsEquivalent`, `transIsEquivalentEventuallyEq`, `transIsEquivalentIsBigO`, `transIsEquivalentIsEquivalent`, `transIsEquivalentIsLittleO`, `transIsEquivalentIsTheta`, `transIsLittleOIsEquivalent`, `transIsThetaIsEquivalent`	9
Theorems `trans_isEquivalent`, `add_add_of_nonneg`, `add_const_of_norm_tendsto_atTop`, `add_isLittleO`, `comp_tendsto`, `congr_left`, `congr_right`, `const_add_of_norm_tendsto_atTop`, `div`, `exists_eq_mul`, `finsetProd`, `inv`, `isBigO`, `isBigO_symm`, `isLittleO`, `isTheta`, `isTheta_symm`, `listProd`, `mono`, `mul`, `multisetProd`, `neg`, `pow`, `refl`, `smul`, `sub_isLittleO`, `tendsto_atBot`, `tendsto_atBot_iff`, `tendsto_atTop`, `tendsto_atTop_iff`, `tendsto_const`, `tendsto_nhds`, `tendsto_nhds_iff`, `trans`, `trans_eventuallyEq`, `trans_isBigO`, `trans_isLittleO`, `trans_isTheta`, `zpow`, `add_isEquivalent`, `isEquivalent`, `trans_isEquivalent`, `trans_isEquivalent`, `isEquivalent_const_iff_tendsto`, `isEquivalent_iff_exists_eq_mul`, `isEquivalent_iff_tendsto_one`, `isEquivalent_map`, `isEquivalent_of_tendsto_one`, `isEquivalent_of_tendsto_one'`, `isEquivalent_zero_iff_eventually_zero`, `isEquivalent_zero_iff_isBigO_zero`, `isEquivalent`, `trans_isEquivalent`	53
Total	62

Asymptotics

Definitions

Name	Category	Theorems
`transEventuallyEqIsEquivalent` 📖	CompOp	—
`transIsBigOIsEquivalent` 📖	CompOp	—
`transIsEquivalentEventuallyEq` 📖	CompOp	—
`transIsEquivalentIsBigO` 📖	CompOp	—
`transIsEquivalentIsEquivalent` 📖	CompOp	—
`transIsEquivalentIsLittleO` 📖	CompOp	—
`transIsEquivalentIsTheta` 📖	CompOp	—
`transIsLittleOIsEquivalent` 📖	CompOp	—
`transIsThetaIsEquivalent` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEquivalent_const_iff_tendsto` 📖	mathematical	—	`IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`isLittleO_const_iff` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_const_nhds` `sub_neg_eq_add` `sub_add_cancel` `zero_add` `sub_self`
`isEquivalent_iff_exists_eq_mul` 📖	mathematical	—	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`IsEquivalent.eq_1` `isLittleO_iff_exists_eq_mul` `zero_add` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `tendsto_const_nhds` `sub_add_cancel` `add_mul` `Distrib.rightDistribClass` `one_mul` `Filter.EventuallyEq.fun_add` `Filter.EventuallyEq.refl` `sub_self` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `sub_mul` `Filter.EventuallyEq.fun_sub`
`isEquivalent_iff_tendsto_one` 📖	mathematical	`Filter.Eventually` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Filter.Tendsto` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`IsLittleO.tendsto_div_nhds_zero` `IsEquivalent.isLittleO` `Filter.tendsto_congr'` `Filter.Eventually.mono` `div_self` `tendsto_const_nhds` `sub_add_cancel` `zero_add` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `sub_div` `isEquivalent_of_tendsto_one`
`isEquivalent_map` 📖	mathematical	—	`IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.map`	—	`isLittleO_map`
`isEquivalent_of_tendsto_one` 📖	mathematical	`Filter.Tendsto` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing`	—	`Filter.Frequently.mono` `div_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `tendsto_nhds_unique_of_frequently_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `tendsto_const_nhds` `isEquivalent_iff_exists_eq_mul` `Filter.Eventually.mono` `div_mul_cancel_of_imp`
`isEquivalent_of_tendsto_one'` 📖	mathematical	`Filter.Tendsto` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing`	—	`isEquivalent_of_tendsto_one`
`isEquivalent_zero_iff_eventually_zero` 📖	mathematical	—	`IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Filter.EventuallyEq`	—	`IsEquivalent.eq_1` `sub_zero` `isLittleO_zero_right_iff`
`isEquivalent_zero_iff_isBigO_zero` 📖	mathematical	—	`IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `IsBigO` `NormedAddCommGroup.toNorm`	—	`IsEquivalent.isBigO` `isEquivalent_zero_iff_eventually_zero` `Filter.eventuallyEq_iff_exists_mem` `isBigO_zero_right_iff`

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_isEquivalent` 📖	—	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`trans` `Asymptotics.IsEquivalent.isBigO`

Asymptotics.IsEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_add_of_nonneg` 📖	mathematical	`Pi.hasLe` `Real` `Real.instLE` `Pi.instZero` `Real.instZero` `Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Pi.instAdd` `Real.instAdd`	—	`add_sub_add_comm` `abs_eq_self` `Real.instIsOrderedAddMonoid` `Asymptotics.IsLittleO.add_add`
`add_const_of_norm_tendsto_atTop` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `Real` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Real.instPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add_isLittleO` `Asymptotics.isLittleO_const_left`
`add_isLittleO` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add_sub_right_comm` `Asymptotics.IsLittleO.add`
`comp_tendsto` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto`	—	—	`Asymptotics.IsLittleO.comp_tendsto`
`congr_left` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq`	—	—	`Asymptotics.IsLittleO.congr'` `Filter.EventuallyEq.sub` `Filter.EventuallyEq.refl`
`congr_right` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq`	—	—	`symm` `congr_left`
`const_add_of_norm_tendsto_atTop` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `Real` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Real.instPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Asymptotics.IsLittleO.add_isEquivalent` `Asymptotics.isLittleO_const_left`
`div` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div_eq_mul_inv` `mul` `inv`
`exists_eq_mul` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`Asymptotics.isEquivalent_iff_exists_eq_mul`
`finsetProd` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`multisetProd`
`inv` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`Asymptotics.isEquivalent_iff_exists_eq_mul` `inv_one` `Filter.Tendsto.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mul_comm` `mul_inv_rev` `Filter.EventuallyEq.fun_inv`
`isBigO` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm`	—	`Asymptotics.IsBigO.congr_of_sub` `Asymptotics.IsBigO.symm` `Asymptotics.IsLittleO.isBigO` `Asymptotics.isBigO_refl`
`isBigO_symm` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm`	—	`sub_add_cancel` `Asymptotics.IsLittleO.right_isBigO_add` `isLittleO`
`isLittleO` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	—
`isTheta` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm`	—	`isBigO` `isBigO_symm`
`isTheta_symm` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm`	—	`isBigO_symm` `isBigO`
`listProd` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`mul`
`mono` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`Asymptotics.IsLittleO.mono`
`mul` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`smul`
`multisetProd` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Multiset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Multiset.map`	—	`Quotient.mk_surjective` `listProd`
`neg` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`eq_1` `sub_neg_eq_add` `neg_add_eq_sub` `neg_sub` `Asymptotics.IsLittleO.neg_right` `Asymptotics.IsLittleO.neg_left` `isLittleO`
`pow` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`pow_zero` `refl` `pow_succ` `mul`
`refl` 📖	mathematical	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`eq_1` `sub_self` `Asymptotics.isLittleO_zero`
`smul` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`exists_eq_mul` `Pi.mul_apply` `mul_comm` `SemigroupAction.mul_smul` `smul_sub` `Filter.EventuallyEq.fun_sub` `Filter.EventuallyEq.comp₂` `Filter.EventuallyEq.refl` `Asymptotics.isLittleO_congr` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.rfl` `Asymptotics.IsBigO.smul_isLittleO` `NormedSpace.toIsBoundedSMul` `NormedSpace.toNormSMulClass` `Asymptotics.isBigO_refl` `Asymptotics.IsBigO.exists_pos` `isBigO` `Asymptotics.isLittleO_iff` `Filter.Eventually.mp` `Nat.instAtLeastTwoHAddOfNat` `dist_eq_norm` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `eq_1` `Filter.Eventually.mono` `Asymptotics.IsBigOWith_def` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `norm_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `sub_smul` `one_smul` `sub_add` `sub_sub_cancel` `norm_add_le` `norm_smul` `add_le_add_left` `covariant_swap_add_of_covariant_add` `add_le_add_right` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add`
`sub_isLittleO` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add_isLittleO` `Asymptotics.IsLittleO.neg_left`
`tendsto_atBot` 📖	—	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`neg_neg` `Filter.Tendsto.comp` `Filter.tendsto_neg_atTop_atBot` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `tendsto_atTop` `neg` `Filter.tendsto_neg_atBot_atTop`
`tendsto_atBot_iff` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tendsto_atBot` `symm`
`tendsto_atTop` 📖	—	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`exists_eq_mul` `symm` `Filter.Tendsto.congr'` `Filter.EventuallyEq.symm` `Filter.Tendsto.atTop_mul_pos` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `mul_comm`
`tendsto_atTop_iff` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tendsto_atTop` `symm`
`tendsto_const` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`em` `Filter.tendsto_congr'` `Asymptotics.isEquivalent_zero_iff_eventually_zero` `tendsto_const_nhds` `Asymptotics.isEquivalent_const_iff_tendsto`
`tendsto_nhds` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `sub_add_cancel` `Asymptotics.IsLittleO.add` `Asymptotics.IsLittleO.trans` `isLittleO` `symm` `Asymptotics.isEquivalent_const_iff_tendsto` `trans`
`tendsto_nhds_iff` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`tendsto_nhds` `symm`
`trans` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`Asymptotics.IsLittleO.triangle` `Asymptotics.IsLittleO.trans_isBigO` `isLittleO` `isBigO`
`trans_eventuallyEq` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.EventuallyEq`	—	—	`trans` `Filter.EventuallyEq.isEquivalent`
`trans_isBigO` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm`	—	—	`Asymptotics.IsBigO.trans` `isBigO`
`trans_isLittleO` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm`	—	—	`Asymptotics.IsBigO.trans_isLittleO` `isBigO`
`trans_isTheta` 📖	—	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsTheta` `NormedAddCommGroup.toNorm`	—	—	`Asymptotics.IsTheta.trans` `isTheta`
`zpow` 📖	mathematical	`Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow_natCast` `pow` `zpow_negSucc` `inv`

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_isEquivalent` 📖	mathematical	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Asymptotics.IsEquivalent.add_isLittleO` `add_comm`
`isEquivalent` 📖	mathematical	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—
`trans_isEquivalent` 📖	—	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`trans_isBigO` `Asymptotics.IsEquivalent.isBigO`

Asymptotics.IsTheta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_isEquivalent` 📖	—	`Asymptotics.IsTheta` `NormedAddCommGroup.toNorm` `Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`trans` `Asymptotics.IsEquivalent.isTheta`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEquivalent` 📖	mathematical	`Filter.EventuallyEq`	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Asymptotics.IsEquivalent.congr_right` `Asymptotics.isLittleO_refl_left`
`trans_isEquivalent` 📖	—	`Filter.EventuallyEq` `Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`Asymptotics.IsEquivalent.trans` `isEquivalent`

---

← Back to Index