Commit 2023-01-05 13:17 8a391fa4

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.