Asymptotics

📁 Source: Mathlib/Analysis/Normed/Operator/Asymptotics.lean

Statistics

Metric	Count
Definitions	0
Theorems isBigO_comp, isBigO_comp_rev, isBigO_sub, isBigO_sub_rev, isBigOWith_comp, isBigOWith_id, isBigOWith_sub, isBigO_comp, isBigO_id, isBigO_sub	10
Total	10

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_comp 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule EquivLike.toFunLike equivLike	—	ContinuousLinearMap.isBigO_comp
isBigO_comp_rev 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule EquivLike.toFunLike equivLike	—	Asymptotics.IsBigO.congr_left isBigO_comp symm_apply_apply
isBigO_sub 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule EquivLike.toFunLike equivLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	ContinuousLinearMap.isBigO_sub
isBigO_sub_rev 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule EquivLike.toFunLike equivLike	—	isBigO_comp_rev

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigOWith_comp 📖	mathematical	—	Asymptotics.IsBigOWith SeminormedAddCommGroup.toNorm Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm DFunLike.coe funLike	—	Asymptotics.IsBigOWith.comp_tendsto isBigOWith_id le_top
isBigOWith_id 📖	mathematical	—	Asymptotics.IsBigOWith SeminormedAddCommGroup.toNorm Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm DFunLike.coe funLike	—	Asymptotics.isBigOWith_of_le' le_opNorm
isBigOWith_sub 📖	mathematical	—	Asymptotics.IsBigOWith SeminormedAddCommGroup.toNorm Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm DFunLike.coe funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	isBigOWith_comp
isBigO_comp 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike	—	Asymptotics.IsBigOWith.isBigO isBigOWith_comp
isBigO_id 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike	—	Asymptotics.IsBigOWith.isBigO isBigOWith_id
isBigO_sub 📖	mathematical	—	Asymptotics.IsBigO SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	isBigO_comp

---

← Back to Index