mathlib

8a391fa4 - feat(analysis/convolution): weaken topological assumptions (#18012)

feat(analysis/convolution): weaken topological assumptions (#18012) We redefine `locally_integrable`: currently, this means "integrable on every compact set", and we change it to "integrable on a neighborhood of any point", to bring it in line with `is_locally_finite_measure`. This makes it possible to weaken a lot of assumptions in the file on convolutions, removing second countability or local compactness assumptions.