Commit 2025-05-13 06:46 590896b8

View on Github →

chore(HasFiniteIntegral): generalise to enorms (#24818) This is exhaustive for now: the remaining lemmas need stronger type classes.

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

added theorem MeasureTheory.HasFiniteIntegral.of_mem_Icc_of_ne_top

modified theorem MeasureTheory.hasFiniteIntegral_count_iff

added theorem MeasureTheory.hasFiniteIntegral_count_iff_enorm

modified theorem MeasureTheory.lintegral_enorm_add_left

modified theorem MeasureTheory.lintegral_enorm_add_right

modified theorem MeasureTheory.lintegral_enorm_zero