Commit 2025-01-13 17:41 d3d990d0

View on Github →

feat: Estimating a finite sum by an interval integral, for the product of a monotone and an antitone function (#20456) From the Carleson project

Estimated changes

Modified Mathlib/Analysis/SumIntegralComparisons.lean

added theorem integral_le_sum_Ico_of_le

added theorem integral_le_sum_mul_Ico_of_antitone_monotone

added theorem sum_Ico_le_integral_of_le

added theorem sum_mul_Ico_le_integral_of_monotone_antitone

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.Integrable.mul_of_top_left

added theorem MeasureTheory.Integrable.mul_of_top_right

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

deleted theorem AntioneOn.integrableOn_isCompact

added theorem AntitoneOn.integrableOn_isCompact

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

added theorem intervalIntegral.integral_mono_on_of_le_Ioo