Commit 2024-02-09 14:17 117789e2

View on Github →

feat: generalize cocompact_eq (#10285) example use case: cocompact_le with integrable_iff_integrableAtFilter_cocompact from #10248 becomes a way to prove integrability from big-O estimates (e.g. #10258)

Estimated changes

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/Topology/Algebra/Order/Compact.lean

added theorem atBot_atTop_le_cocompact

added theorem atBot_le_cocompact

added theorem atTop_le_cocompact

added theorem cocompact_eq_atBot

added theorem cocompact_eq_atBot_atTop

added theorem cocompact_eq_atTop

added theorem cocompact_le_atBot

added theorem cocompact_le_atBot_atTop

added theorem cocompact_le_atTop

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem Nat.cocompact_eq

Modified Mathlib/Topology/Instances/Int.lean

deleted theorem Int.cocompact_eq

Modified Mathlib/Topology/Instances/Real.lean

deleted theorem Real.atBot_le_cocompact

deleted theorem Real.atTop_le_cocompact

deleted theorem Real.cocompact_eq