Commit 2024-02-06 19:27 33c4af8d

View on Github →

feat: bounding integrals by asymptotics, part 1 (#10248) part 1: corollaries such as for atTop ℝ yet to come

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem MeasureTheory.integrable_iff_integrableAtFilter_cocompact

Created Mathlib/MeasureTheory/Integral/Asymptotics.lean

added theorem Asymptotics.IsBigO.integrable

added theorem Asymptotics.IsBigO.integrableAtFilter

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.integrableAtFilter_top