Commit 2023-11-08 07:48 aff5c83d

View on Github →

feat: continuity of parametric integrals with weaker assumptions (#8247) The current version of continuity of parametric integrals assume a first countable topology, to apply the dominated convergence theorem. When one deals with continuous compactly supported functions, this is not necessary, and a direct elementary approach makes it possible to remove the first countable assumption.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

modified theorem BddAbove.continuous_convolution_right_of_integrable

modified theorem HasCompactSupport.continuous_convolution_left

deleted theorem continuousOn_convolution_right_with_param'

modified theorem continuousOn_convolution_right_with_param

deleted theorem continuousOn_convolution_right_with_param_comp'

modified theorem continuousOn_convolution_right_with_param_comp

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem continuousOn_integral_bilinear_of_locally_integrable_of_compact_support

added theorem continuousOn_integral_of_compact_support