Commit 2026-04-07 13:03 88619f3b

View on Github →

feat(MeasureTheory/Integral/Average): add laverage_mono_ae and setLAverage_le_essSup (#37551) Add monotonicity and essential supremum bounds for the Lebesgue average:

  • laverage_mono_ae
  • setLAverage_mono_ae (tagged @[gcongr])
  • setLAverage_le_essSup
  • laverage_le_essSup Upstreamed from the Carleson project.

Estimated changes