Commit 2022-02-21 08:48 8b93d3a5

feat(measure_theory/function/lp_space): generalize some integrable lemmas to mem_ℒp (#11231) I would like to define integrable as mem_ℒp for p = 1 and remove the has_finite_integral prop. But first we need to generalize everything we have about integrable to mem_ℒp. This is one step towards that goal.