Commit 2025-01-23 15:33 e36d9d7c

View on Github →

feat: interval integrability of periodic functions (#20938) Add a theorem showing that a periodic function is interval integrable over every interval if it is interval integrable over one period. Add docstrings with section headings to improve readability. The theorem is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

modified theorem Function.Periodic.integral_le_sSup_add_zsmul_of_pos

added theorem Function.Periodic.intervalIntegrable

added theorem Function.Periodic.intervalIntegrable₀

modified theorem Function.Periodic.sInf_add_zsmul_le_integral_of_pos

modified theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos'

modified theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos'