Theorem sum_mul_Ico_le_integral_of_monotone_antitone

Modification history

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