Theorem MeasureTheory.Integrable.mul_of_top_right

Modification history

2025-01-13 17:41
Mathlib/MeasureTheory/Function/L1Space.lean
feat: Estimating a finite sum by an interval integral, for the product of a monotone and an antitone function (#20456) …
Added MeasureTheory.Integrable.mul_of_top_rightView on Github →