Commit 2026-04-24 08:11 937b8ae9

View on Github →

feat(MeasureTheory): Integral over Ioi tends to zero (#34298) This PR proves that if f is integrable on Ioi a, then ∫ x in Ioi (b i), f x ∂μ tends to zero as b i tends to infinity. This is an easy corollary of intervalIntegral_tendsto_integral_Ioi.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.aecover_Ici_of_Ico

added theorem MeasureTheory.aecover_Iio_of_Ico

added theorem MeasureTheory.tendsto_integral_Ici_zero

added theorem MeasureTheory.tendsto_integral_Ico_integral_Ici

added theorem MeasureTheory.tendsto_integral_Ico_integral_Iio

added theorem MeasureTheory.tendsto_integral_Iic_zero

added theorem MeasureTheory.tendsto_integral_Iio_zero

added theorem MeasureTheory.tendsto_integral_Ioi_zero

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

added theorem intervalIntegral.integral_Ici_sub_Ici'

added theorem intervalIntegral.integral_Ici_sub_Ici