Commit 2024-05-05 11:45 1facc8b1

View on Github →

fix: move convolution to MeasureTheory namespace (#12376) also fix some porting notes

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

modified theorem BddAbove.continuous_convolution_left_of_integrable

modified theorem BddAbove.continuous_convolution_right_of_integrable

modified theorem BddAbove.convolutionExistsAt'

modified theorem BddAbove.convolutionExistsAt

modified theorem Continuous.convolution_integrand_fst

deleted theorem ConvolutionExists.add_distrib

deleted theorem ConvolutionExists.distrib_add

deleted def ConvolutionExists

deleted theorem ConvolutionExistsAt.add_distrib

deleted theorem ConvolutionExistsAt.distrib_add

deleted theorem ConvolutionExistsAt.integrable

deleted theorem ConvolutionExistsAt.integrable_swap

deleted theorem ConvolutionExistsAt.ofNorm'

deleted theorem ConvolutionExistsAt.ofNorm

deleted def ConvolutionExistsAt

modified theorem HasCompactSupport.contDiff_convolution_left

modified theorem HasCompactSupport.contDiff_convolution_right

modified theorem HasCompactSupport.continuous_convolution_left

modified theorem HasCompactSupport.continuous_convolution_right

modified theorem HasCompactSupport.convolutionExistsAt

modified theorem HasCompactSupport.convolutionExistsLeft

modified theorem HasCompactSupport.convolutionExistsRightOfContinuousLeft

modified theorem HasCompactSupport.convolutionExists_left_of_continuous_right

modified theorem HasCompactSupport.convolutionExists_right

modified theorem HasCompactSupport.convolution_integrand_bound_left

modified theorem HasCompactSupport.convolution_integrand_bound_right

modified theorem HasCompactSupport.convolution_integrand_bound_right_of_subset

modified theorem HasCompactSupport.hasDerivAt_convolution_left

modified theorem HasCompactSupport.hasDerivAt_convolution_right

modified theorem HasCompactSupport.hasFDerivAt_convolution_left

modified theorem HasCompactSupport.hasFDerivAt_convolution_right

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand'

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd'

modified theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd

added theorem MeasureTheory.ConvolutionExists.add_distrib

added theorem MeasureTheory.ConvolutionExists.distrib_add

added def MeasureTheory.ConvolutionExists

added theorem MeasureTheory.ConvolutionExistsAt.add_distrib

added theorem MeasureTheory.ConvolutionExistsAt.distrib_add

added theorem MeasureTheory.ConvolutionExistsAt.integrable

added theorem MeasureTheory.ConvolutionExistsAt.integrable_swap

added theorem MeasureTheory.ConvolutionExistsAt.ofNorm'

added theorem MeasureTheory.ConvolutionExistsAt.ofNorm

added def MeasureTheory.ConvolutionExistsAt

modified theorem MeasureTheory.Integrable.ae_convolution_exists

modified theorem MeasureTheory.Integrable.convolution_integrand

modified theorem MeasureTheory.Integrable.integrable_convolution

added theorem MeasureTheory.contDiffOn_convolution_left_with_param

added theorem MeasureTheory.contDiffOn_convolution_left_with_param_comp

added theorem MeasureTheory.contDiffOn_convolution_right_with_param

added theorem MeasureTheory.contDiffOn_convolution_right_with_param_aux

added theorem MeasureTheory.contDiffOn_convolution_right_with_param_comp

added theorem MeasureTheory.continuousOn_convolution_right_with_param

added theorem MeasureTheory.continuousOn_convolution_right_with_param_comp

added theorem MeasureTheory.convolutionExistsAt_flip

added theorem MeasureTheory.convolutionExistsAt_iff_integrable_swap

added theorem MeasureTheory.convolution_assoc'

added theorem MeasureTheory.convolution_assoc

added theorem MeasureTheory.convolution_congr

added theorem MeasureTheory.convolution_def

added theorem MeasureTheory.convolution_eq_right'

added theorem MeasureTheory.convolution_eq_swap

added theorem MeasureTheory.convolution_flip

added theorem MeasureTheory.convolution_integrand_bound_right_of_le_of_subset

added theorem MeasureTheory.convolution_lsmul

added theorem MeasureTheory.convolution_lsmul_swap

added theorem MeasureTheory.convolution_mono_right

added theorem MeasureTheory.convolution_mono_right_of_nonneg

added theorem MeasureTheory.convolution_mul

added theorem MeasureTheory.convolution_mul_swap

added theorem MeasureTheory.convolution_neg_of_neg_eq

added theorem MeasureTheory.convolution_precompR_apply

added theorem MeasureTheory.convolution_smul

added theorem MeasureTheory.convolution_tendsto_right

added theorem MeasureTheory.convolution_zero

added theorem MeasureTheory.dist_convolution_le'

added theorem MeasureTheory.dist_convolution_le

added theorem MeasureTheory.hasFDerivAt_convolution_right_with_param

added theorem MeasureTheory.integrable_posConvolution

added theorem MeasureTheory.integral_convolution

added theorem MeasureTheory.integral_posConvolution

added theorem MeasureTheory.posConvolution_eq_convolution_indicator

added theorem MeasureTheory.smul_convolution

added theorem MeasureTheory.support_convolution_subset

added theorem MeasureTheory.support_convolution_subset_swap

added theorem MeasureTheory.zero_convolution

deleted theorem contDiffOn_convolution_left_with_param

deleted theorem contDiffOn_convolution_left_with_param_comp

deleted theorem contDiffOn_convolution_right_with_param

deleted theorem contDiffOn_convolution_right_with_param_aux

deleted theorem contDiffOn_convolution_right_with_param_comp

deleted theorem continuousOn_convolution_right_with_param

deleted theorem continuousOn_convolution_right_with_param_comp

deleted theorem convolutionExistsAt_flip

deleted theorem convolutionExistsAt_iff_integrable_swap

deleted theorem convolution_assoc'

deleted theorem convolution_assoc

deleted theorem convolution_congr

deleted theorem convolution_def

deleted theorem convolution_eq_right'

deleted theorem convolution_eq_swap

deleted theorem convolution_flip

deleted theorem convolution_integrand_bound_right_of_le_of_subset

deleted theorem convolution_lsmul

deleted theorem convolution_lsmul_swap

deleted theorem convolution_mono_right

deleted theorem convolution_mono_right_of_nonneg

deleted theorem convolution_mul

deleted theorem convolution_mul_swap

deleted theorem convolution_neg_of_neg_eq

deleted theorem convolution_precompR_apply

deleted theorem convolution_smul

deleted theorem convolution_tendsto_right

deleted theorem convolution_zero

deleted theorem dist_convolution_le'

deleted theorem dist_convolution_le

deleted theorem hasFDerivAt_convolution_right_with_param

deleted theorem integrable_posConvolution

deleted theorem integral_convolution

deleted theorem integral_posConvolution

deleted theorem posConvolution_eq_convolution_indicator

deleted theorem smul_convolution

deleted theorem support_convolution_subset

deleted theorem support_convolution_subset_swap

deleted theorem zero_convolution

Modified docs/overview.yaml

Modified docs/undergrad.yaml