mathlib3

6386d90a - feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514)

feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514) This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite. Co-authored-by: Sébastien Gouëzel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Remy Degenne <remydegenne@gmail.com> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>