Convolution

📁 Source: Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_convolution_tendsto_right_of_locallyIntegrable, convolution_eq_right, convolution_tendsto_right, convolution_tendsto_right_of_continuous, dist_normed_convolution_le, normed_convolution_eq_right	6
Total	6

ContDiffBump

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_convolution_tendsto_right_of_locallyIntegrable 📖	mathematical	Filter.Tendsto Real rOut NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.Eventually Real.instLE Real.instMul rIn MeasureTheory.LocallyIntegrable SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.convolution Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup normed ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real BorelSpace.opensMeasurable Besicovitch.instHasBesicovitchCovering MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal NormedSpace.toIsBoundedSMul IsScalarTower.left VitaliFamily.ae_tendsto_average_norm_sub MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Filter.univ_mem' IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.convolution_eq_swap MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite PseudoEMetricSpace.pseudoMetrizableSpace ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg ContinuousAdd.measurableAdd tendsto_nhdsWithin_iff Filter.Eventually.of_forall rOut_pos Filter.Tendsto.comp Besicovitch.tendsto_filterAt MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub MeasureTheory.LocallyIntegrable.integrableOn_isCompact ProperSpace.isCompact_closedBall Filter.Tendsto.congr MeasureTheory.integral_neg_eq_self normed.congr_simp sub_neg_eq_add MeasureTheory.integral_add_left_eq_self integral_normed MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure tendsto_const_nhds support_normed_eq dist_eq_norm_sub' LT.lt.le dist_zero_right abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid nonneg_normed MeasureTheory.Measure.addHaar_real_closedBall_center normed_le_div_measure_closedBall_rOut
convolution_eq_right 📖	mathematical	—	MeasureTheory.convolution Real Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup toFun NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Real.semiring MeasureTheory.integral	—	NormedSpace.toIsBoundedSMul IsScalarTower.left SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.convolution_eq_right' Eq.subset Set.instReflSubset support_eq integral_smul_const
convolution_tendsto_right 📖	mathematical	Filter.Tendsto Real rOut NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.Eventually MeasureTheory.AEStronglyMeasurable SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Filter Filter.instSProd	MeasureTheory.convolution Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup normed ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction	—	MeasureTheory.convolution_tendsto_right secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal Filter.Eventually.of_forall nonneg_normed integral_normed MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure tendsto_support_normed_smallSets
convolution_tendsto_right_of_continuous 📖	mathematical	Filter.Tendsto Real rOut NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Continuous SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.convolution Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup normed ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction	—	convolution_tendsto_right Filter.Eventually.of_forall Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real Filter.Tendsto.comp Continuous.tendsto Filter.tendsto_snd tendsto_const_nhds
dist_normed_convolution_le 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instLE Dist.dist PseudoMetricSpace.toDist	MeasureTheory.convolution Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup normed ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction	—	MeasureTheory.dist_convolution_le secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal dist_self Metric.mem_ball_self rOut_pos Eq.subset Set.instReflSubset support_normed_eq MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure nonneg_normed integral_normed
normed_convolution_eq_right 📖	mathematical	—	MeasureTheory.convolution Real Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup normed ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.lsmul SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction	—	ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal NormedSpace.toIsBoundedSMul IsScalarTower.left SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.convolution_eq_right' Eq.subset Set.instReflSubset support_normed_eq integral_normed_smul

---

← Back to Index