Theorem MonotoneOn.sum_le_integral

Modification history

2023-06-09 13:13
Mathlib/Analysis/SumIntegralComparisons.lean
feat: port Analysis.SumIntegralComparisons (#4902)
Added MonotoneOn.sum_le_integralView on Github →