[Merged by Bors] - feat(MeasureTheory/Integral/Average): add laverage_mono_ae and setLAverage_le_essSup#37551

pitmonticone wants to merge 3 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

pitmonticone:carleson/laverage-mono-essSuppitmonticone/mathlib4:carleson/laverage-mono-essSupCopy head branch name to clipboard