Commit 2024-04-04 09:42 434972cc

View on Github →

feat: bounding integrals by asymptotics, part 2: corollaries (#10388) Shortcuts for linearly ordered domains and/or continuous functions. As an example, I golf the existing integrable_of_isBigO_exp_neg. Another example usage: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/1909a40253607bd2df18a738fc504fe81b132974/PrimeNumberTheoremAnd/PerronFormula.lean#L414-L436

Estimated changes

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop

added theorem MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot

added theorem MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin

added theorem MeasureTheory.integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin

added theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot

added theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop

added theorem MeasureTheory.integrable_iff_integrableAtFilter_atTop

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

added theorem measurableEmbedding_inv

Modified Mathlib/MeasureTheory/Integral/Asymptotics.lean

added theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot

added theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot_atTop

added theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop

added theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant

added theorem MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact

added theorem MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atBot

added theorem MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop

Modified Mathlib/MeasureTheory/Integral/ExpDecay.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.IntegrableAtFilter.sup_iff