Theorem integral_le_sum_mul_Ico_of_antitone_monotone

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 integral_le_sum_mul_Ico_of_antitone_monotoneView on Github →