Theorem sum_Ico_le_integral_of_le

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