Commit 2026-02-25 17:28 00d4a23f

View on Github →

feat: add congruence lemmas for integrability (#35086) Add simple congruence lemmas for interval- and circle integrability. Perform very minor golfing.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

added theorem circleIntegrable_neg_radius

added theorem crcleIntegrable_congr

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

added theorem IntervalIntegrable.comp_add_left_iff

added theorem IntervalIntegrable.comp_add_right_iff

added theorem IntervalIntegrable.comp_sub_right_iff

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

added theorem Function.Periodic.intervalIntegrable_iff

modified theorem Function.Periodic.intervalIntegrable₀

deleted theorem Function.Periodic.intervalIntegral_add_eq_of_pos