Theorem Function.Periodic.intervalIntegrable

Modification history

2025-08-11 13:56
Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
chore(IntegrableOn): generalise one more section to enorms (#27419)
Modified Function.Periodic.intervalIntegrableView on Github →
2025-01-23 15:33
Mathlib/MeasureTheory/Integral/Periodic.lean
feat: interval integrability of periodic functions (#20938) …
Added Function.Periodic.intervalIntegrableView on Github →