Commit 2023-01-07 13:53 9d81ef7e

View on Github →

feat(analysis/convolution): regularity of convolution for functions depending on a parameter (#17626) Show that the convolution of f and g is smooth when g is. A version of this statement is already in mathlib, but in this PR we prove the version where g depends on a parameter.

Estimated changes

Modified src/analysis/convolution.lean

added theorem cont_diff_on_convolution_left_with_param

added theorem cont_diff_on_convolution_left_with_param_comp

added theorem cont_diff_on_convolution_right_with_param

added theorem cont_diff_on_convolution_right_with_param_aux

added theorem cont_diff_on_convolution_right_with_param_comp

added theorem continuous_on_convolution_right_with_param'

added theorem continuous_on_convolution_right_with_param

added theorem continuous_on_convolution_right_with_param_comp'

added theorem continuous_on_convolution_right_with_param_comp

added theorem convolution_integrand_bound_right_of_le_of_subset

modified theorem has_compact_support.cont_diff_convolution_left

modified theorem has_compact_support.cont_diff_convolution_right

modified theorem has_compact_support.continuous_convolution_right

added theorem has_fderiv_at_convolution_right_with_param

Modified src/topology/support.lean

added theorem image_eq_one_of_nmem_mul_tsupport

deleted theorem image_eq_zero_of_nmem_mul_tsupport