Documentation Verification Report

Asymptotics

📁 Source: Mathlib/MeasureTheory/Integral/Asymptotics.lean

Statistics

Metric	Count
Definitions	0
Theorems `eventually_integrableOn`, `integrable`, `integrableAtFilter`, `set_integral_isBigO`, `integrable_of_isBigO_atBot`, `integrable_of_isBigO_atBot_atTop`, `integrable_of_isBigO_atTop`, `integrable_of_isBigO_atTop_of_norm_isNegInvariant`, `integrable_of_isBigO_cocompact`, `integrableOn_of_isBigO_atBot`, `integrableOn_of_isBigO_atTop`	11
Total	11

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_integrableOn` 📖	mathematical	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `Filter.Eventually` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.restrict` `MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	`Filter.Eventually` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`bound` `Filter.Eventually.exists_mem` `Filter.mem_prod_iff` `Filter.eventually_iff_exists_mem` `Filter.inter_mem` `MeasureTheory.Integrable.mono'` `MeasureTheory.integrable_const` `MeasureTheory.Measure.restrict_apply_univ` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.self_mem_ae_restrict` `Filter.univ_mem'`
`integrable` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Top.top` `Filter` `Filter.instTop` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrableAtFilter_top` `PseudoEMetricSpace.pseudoMetrizableSpace` `integrableAtFilter` `Filter.isMeasurablyGenerated_top` `Filter.univ_mem` `MeasureTheory.AEStronglyMeasurable.restrict`
`integrableAtFilter` 📖	mathematical	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `StronglyMeasurableAtFilter` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.IntegrableAtFilter` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.IntegrableAtFilter` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`bound` `Filter.Eventually.exists_measurable_mem_of_smallSets` `Filter.Eventually.and` `Filter.Eventually.smallSets` `StronglyMeasurableAtFilter.eventually` `MeasureTheory.IntegrableAtFilter.eventually` `MeasureTheory.Integrable.mono` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.norm` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_mem` `LE.le.trans` `le_abs_self`
`set_integral_isBigO` 📖	mathematical	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`bound` `Filter.Eventually.exists_mem` `Filter.mem_prod_iff` `Asymptotics.isBigO_iff` `Filter.eventually_iff_exists_mem` `mul_assoc` `smul_eq_mul` `MeasureTheory.measureReal_restrict_apply_univ` `MeasureTheory.integral_const` `Real.instCompleteSpace` `mul_comm` `integral_smul_const` `LE.le.trans` `MeasureTheory.norm_integral_le_integral_norm` `MeasureTheory.integral_mono_of_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `norm_nonneg` `MeasureTheory.integrable_const` `MeasureTheory.Measure.restrict_apply_univ` `Filter.mp_mem` `MeasureTheory.self_mem_ae_restrict`

MeasureTheory.LocallyIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_of_isBigO_atBot` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrable_iff_integrableAtFilter_atBot` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter` `aestronglyMeasurable`
`integrable_of_isBigO_atBot_atTop` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IntegrableAtFilter` `Filter.atTop`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter` `aestronglyMeasurable`
`integrable_of_isBigO_atTop` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrable_iff_integrableAtFilter_atTop` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter` `aestronglyMeasurable`
`integrable_of_isBigO_atTop_of_norm_isNegInvariant` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Norm.norm` `NormedAddCommGroup.toNorm` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Asymptotics.IsBigO` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop` `locallyIntegrableOn` `MeasureTheory.integrableOn_univ` `Set.Iic_union_Ici_of_le` `le_rfl` `MeasureTheory.integrableOn_union` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Measure.map_neg_eq_self` `MeasurableEmbedding.restrict_map` `measurableEmbedding_neg` `Set.neg_Iic` `neg_zero` `MeasureTheory.IntegrableOn.eq_1` `MeasurableEmbedding.integrable_map_iff` `MeasureTheory.Integrable.congr'` `MeasureTheory.AEStronglyMeasurable.comp_aemeasurable` `MeasureTheory.AEStronglyMeasurable.restrict` `aestronglyMeasurable` `Measurable.aemeasurable` `MeasurableNeg.measurable_neg` `Filter.EventuallyEq.restrict`
`integrable_of_isBigO_cocompact` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.cocompact` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrable_iff_integrableAtFilter_cocompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter` `aestronglyMeasurable`

MeasureTheory.LocallyIntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_of_isBigO_atBot` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atBot` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `Filter.Iic_mem_atBot` `aestronglyMeasurable`
`integrableOn_of_isBigO_atTop` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `MeasureTheory.IntegrableAtFilter`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop` `PseudoEMetricSpace.pseudoMetrizableSpace` `Asymptotics.IsBigO.integrableAtFilter` `Filter.Ici_mem_atTop` `aestronglyMeasurable`

---

← Back to Index