Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-24 14:17 a07493af

View on Github →

feat(analysis/convolution): the predicate convolution_exists (#13541)

This PR defines the predicate that a convolution exists.
This is not that interesting by itself, but it is a preparation for #13540
I'm using the full module doc for the convolution file, even though not everything promised in the module doc is in this PR.
From the sphere eversion project

Estimated changes

Created src/analysis/convolution.lean

added theorem bdd_above.convolution_exists_at'

added theorem bdd_above.convolution_exists_at

added theorem continuous.convolution_integrand_fst

added def convolution_exists

added theorem convolution_exists_at.integrable

added theorem convolution_exists_at.integrable_swap

added def convolution_exists_at

added theorem convolution_exists_at_flip

added theorem convolution_exists_at_iff_integrable_swap

added theorem has_compact_support.convolution_exists_at

added theorem has_compact_support.convolution_exists_left

added theorem has_compact_support.convolution_exists_left_of_continuous_right

added theorem has_compact_support.convolution_exists_right

added theorem has_compact_support.convolution_exists_right_of_continuous_left

added theorem has_compact_support.convolution_integrand_bound_left

added theorem has_compact_support.convolution_integrand_bound_right

added theorem measure_theory.ae_strongly_measurable.convolution_integrand'

added theorem measure_theory.ae_strongly_measurable.convolution_integrand

added theorem measure_theory.ae_strongly_measurable.convolution_integrand_snd'

added theorem measure_theory.ae_strongly_measurable.convolution_integrand_snd

added theorem measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd'

added theorem measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd

added theorem measure_theory.integrable.ae_convolution_exists

added theorem measure_theory.integrable.convolution_integrand