Commit 2023-06-21 15:32 c46fb45b

View on Github →

feat: port Analysis.Convolution (#4929)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convolution.lean

added theorem BddAbove.continuous_convolution_left_of_integrable

added theorem BddAbove.continuous_convolution_right_of_integrable

added theorem BddAbove.convolutionExistsAt'

added theorem BddAbove.convolutionExistsAt

added theorem ContDiffBump.convolution_eq_right

added theorem ContDiffBump.convolution_tendsto_right_of_continuous

added theorem ContDiffBump.dist_normed_convolution_le

added theorem ContDiffBump.normed_convolution_eq_right

added theorem Continuous.convolution_integrand_fst

added theorem ConvolutionExists.add_distrib

added theorem ConvolutionExists.distrib_add

added def ConvolutionExists

added theorem ConvolutionExistsAt.add_distrib

added theorem ConvolutionExistsAt.distrib_add

added theorem ConvolutionExistsAt.integrable

added theorem ConvolutionExistsAt.integrable_swap

added theorem ConvolutionExistsAt.ofNorm'

added theorem ConvolutionExistsAt.ofNorm

added def ConvolutionExistsAt

added theorem HasCompactSupport.contDiff_convolution_left

added theorem HasCompactSupport.contDiff_convolution_right

added theorem HasCompactSupport.continuous_convolution_left

added theorem HasCompactSupport.continuous_convolution_right

added theorem HasCompactSupport.convolutionExistsAt

added theorem HasCompactSupport.convolutionExistsLeft

added theorem HasCompactSupport.convolutionExistsRightOfContinuousLeft

added theorem HasCompactSupport.convolutionExists_left_of_continuous_right

added theorem HasCompactSupport.convolutionExists_right

added theorem HasCompactSupport.convolution_integrand_bound_left

added theorem HasCompactSupport.convolution_integrand_bound_right

added theorem HasCompactSupport.convolution_integrand_bound_right_of_subset

added theorem HasCompactSupport.hasDerivAt_convolution_left

added theorem HasCompactSupport.hasDerivAt_convolution_right

added theorem HasCompactSupport.hasFDerivAt_convolution_left

added theorem HasCompactSupport.hasFDerivAt_convolution_right

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand'

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd'

added theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd

added theorem MeasureTheory.Integrable.ae_convolution_exists

added theorem MeasureTheory.Integrable.convolution_integrand

added theorem MeasureTheory.Integrable.integrable_convolution

added theorem contDiffOn_convolution_left_with_param

added theorem contDiffOn_convolution_left_with_param_comp

added theorem contDiffOn_convolution_right_with_param

added theorem contDiffOn_convolution_right_with_param_aux

added theorem contDiffOn_convolution_right_with_param_comp

added theorem continuousOn_convolution_right_with_param'

added theorem continuousOn_convolution_right_with_param

added theorem continuousOn_convolution_right_with_param_comp'

added theorem continuousOn_convolution_right_with_param_comp

added theorem convolutionExistsAt_flip

added theorem convolutionExistsAt_iff_integrable_swap

added theorem convolution_assoc'

added theorem convolution_assoc

added theorem convolution_congr

added theorem convolution_def

added theorem convolution_eq_right'

added theorem convolution_eq_swap

added theorem convolution_flip

added theorem convolution_integrand_bound_right_of_le_of_subset

added theorem convolution_lsmul

added theorem convolution_lsmul_swap

added theorem convolution_mono_right

added theorem convolution_mono_right_of_nonneg

added theorem convolution_mul

added theorem convolution_mul_swap

added theorem convolution_neg_of_neg_eq

added theorem convolution_precompR_apply

added theorem convolution_smul

added theorem convolution_tendsto_right

added theorem convolution_zero

added theorem dist_convolution_le'

added theorem dist_convolution_le

added theorem hasFDerivAt_convolution_right_with_param

added theorem integrable_posConvolution

added theorem integral_convolution

added theorem integral_posConvolution

added theorem posConvolution_eq_convolution_indicator

added theorem smul_convolution

added theorem support_convolution_subset

added theorem support_convolution_subset_swap

added theorem zero_convolution

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added theorem ContinuousLinearMap.le_of_op_norm_le_of_le

added theorem ContinuousLinearMap.le_of_op_norm₂_le_of_le