Commit 2022-03-01 07:35 c223a81b

feat(measure_theory/function/locally_integrable): define locally integrable (#12216)

• Define the locally integrable predicate
• Move all results about integrability on compact sets to a new file
• Rename some lemmas from integrable_on_compact -> locally_integrable, if appropriate.
• Weaken some type-class assumptions (also on is_compact_interval)
• Simplify proof of continuous.integrable_of_has_compact_support
• Rename variables in moved lemmas to sensible names