Commit 2026-06-01 07:16 1c303148

View on Github →

feat(MeasureTheory/Integral): add integral_congr_uIoo (#39391) This PR adds some congruence lemmas for interval integrals under NoAtoms μ and golfs some lemmas. | Lemma | Heartbeats | Proof Elaboration Time |

Estimated changes

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

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

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

added theorem IntervalIntegrable.congr_uIoo

added theorem intervalIntegrable_congr_uIoo

added theorem intervalIntegral.integral_congr_Ioo_of_le

added theorem intervalIntegral.integral_congr_uIoo

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

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