Commit 2023-06-09 13:13 171a4422

View on Github →

feat: port Analysis.SumIntegralComparisons (#4902)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SumIntegralComparisons.lean

added theorem AntitoneOn.integral_le_sum

added theorem AntitoneOn.integral_le_sum_Ico

added theorem AntitoneOn.sum_le_integral

added theorem AntitoneOn.sum_le_integral_Ico

added theorem MonotoneOn.integral_le_sum

added theorem MonotoneOn.integral_le_sum_Ico

added theorem MonotoneOn.sum_le_integral

added theorem MonotoneOn.sum_le_integral_Ico