Commit 2023-04-04 06:24 08a4542b

feat(measure_theory/function): Functions locally integrable on a set (#18673) This PR adds a definition for local integrability of a function on a set (a relative version of the existing "locally integrable"), and proves some elementary properties of this definition (in particular, functions continuous on s are locally integrable on s).