Convolution

📁 Source: Mathlib/Analysis/Fourier/Convolution.lean

Statistics

Metric	Count
Definitions convolution	1
Theorems fourier_bilin_convolution_eq, fourier_bilin_convolution_eq_integral, fourier_mul_convolution_eq, fourier_smul_convolution_eq, integrable_prod_sub, convolution_apply, convolution_continuous_left, convolution_flip, fourier_convolution, fourier_convolution_apply	10
Total	11

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourier_bilin_convolution_eq 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Continuous	FourierTransform.fourier instFourierTransform MeasureTheory.convolution Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedSpace.complexToReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left fourier_bilin_convolution_eq_integral smul_smul AddChar.map_add_eq_mul inner_add_left map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.integral_apply MeasureTheory.Integrable.const_mul MeasureTheory.Integrable.norm MeasureTheory.Integrable.mono MeasureTheory.AEStronglyMeasurable.smul ContinuousLinearMap.continuousSMul RingHomSurjective.ids SeminormedAddCommGroup.to_isUniformAddGroup Continuous.comp_aestronglyMeasurable Continuous.cexp continuous_id' MeasureTheory.AEStronglyMeasurable.mul_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.continuous_ofReal MeasureTheory.AEStronglyMeasurable.const_mul instIsTopologicalRingReal Continuous.neg IsTopologicalRing.toContinuousNeg MeasureTheory.AEStronglyMeasurable.inner_const aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable secondCountable_of_proper FiniteDimensional.proper_real Continuous.clm_apply continuous_const Continuous.aestronglyMeasurable secondCountableTopologyEither_of_left Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass Circle.norm_smul norm_mul NormedDivisionRing.toNormMulClass norm_norm ContinuousLinearMap.le_opNorm ContinuousLinearMap.integral_comp_comm ContinuousLinearMap.instCompleteSpace FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology
fourier_bilin_convolution_eq_integral 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Continuous	FourierTransform.fourier instFourierTransform MeasureTheory.convolution NormedSpace.complexToReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.integral Circle Circle.instSMul SMulZeroClass.toSMul Complex AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg Inner.inner InnerProductSpace.toInner instRCLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids MeasureTheory.convolution_flip MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular locallyCompact_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instWeaklyLocallyCompactSpaceOfLocallyCompactSpace MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg ContinuousAdd.measurableAdd MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal MeasureTheory.integral_integral_swap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Integrable.mono integrable_prod_sub MeasureTheory.AEStronglyMeasurable.smul Circle.instContinuousSMul IsBoundedSMul.continuousSMul Continuous.comp_aestronglyMeasurable continuous_fourierChar Continuous.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal continuous_id' MeasureTheory.AEStronglyMeasurable.inner_const MeasureTheory.AEStronglyMeasurable.fst aestronglyMeasurable_id TopologicalSpace.pseudoMetrizableSpace_prod Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyProd Continuous.clm_apply Continuous.comp' continuous_const Continuous.fst Continuous.snd MeasureTheory.AEStronglyMeasurable.prodMk Continuous.aestronglyMeasurable Continuous.sub IsTopologicalAddGroup.to_continuousSub MeasureTheory.AEStronglyMeasurable.snd Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass le_imp_le_of_le_of_le ContinuousLinearMap.le_opNorm₂ le_refl mul_assoc Circle.norm_smul norm_mul NormedDivisionRing.toNormMulClass norm_norm add_sub_cancel MeasureTheory.integral_sub_right_eq_self MeasureTheory.IsAddLeftInvariant.isAddRightInvariant
fourier_mul_convolution_eq 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Continuous SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	FourierTransform.fourier instFourierTransform NonUnitalNormedRing.toNormedAddCommGroup MeasureTheory.convolution Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedSpace.complexToReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	fourier_bilin_convolution_eq
fourier_smul_convolution_eq 📖	mathematical	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Continuous	FourierTransform.fourier instFourierTransform MeasureTheory.convolution Complex.instNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace NormedSpace.complexToReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.lsmul NormedAlgebra.id NontriviallyNormedField.toNormedField NormedSpace.toModule 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Complex.instSemiring	—	fourier_bilin_convolution_eq Complex.instCompleteSpace NormedSpace.toIsBoundedSMul IsScalarTower.left
integrable_prod_sub 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Continuous	Real pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing Prod.instMeasurableSpace instMul Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul ContinuousLinearMap.hasOpNorm ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid MeasureTheory.Measure.prod	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.Integrable.const_mul MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integrable_prod_iff' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper Continuous.comp_aestronglyMeasurable continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.AEStronglyMeasurable.prodMk MeasureTheory.AEStronglyMeasurable.norm Continuous.aestronglyMeasurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right PseudoEMetricSpace.pseudoMetrizableSpace Continuous.sub IsTopologicalAddGroup.to_continuousSub Continuous.fst continuous_id' Continuous.snd MeasureTheory.AEStronglyMeasurable.snd aestronglyMeasurable_id TopologicalSpace.pseudoMetrizableSpace_prod TopologicalSpace.instSecondCountableTopologyProd Filter.univ_mem' MeasureTheory.Integrable.mul_const MeasureTheory.Integrable.norm MeasureTheory.Integrable.comp_sub_right ContinuousAdd.measurableAdd MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Integrable.bdd_mul MeasureTheory.aestronglyMeasurable_const le_refl norm_mul NormedDivisionRing.toNormMulClass norm_norm MeasureTheory.integral_mul_const MeasureTheory.integral_sub_right_eq_self RingHomIsometric.ids

SchwartzMap

Definitions

Name	Category	Theorems
convolution 📖	CompOp	5 math math: convolution_apply, convolution_continuous_left, convolution_flip, fourier_convolution_apply, fourier_convolution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convolution_apply 📖	mathematical	—	DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFunLike ContinuousLinearMap Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Complex.instRCLike RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass EuclideanDomain.toCommRing Field.toEuclideanDomain ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul LinearMap.instFunLike convolution MeasureTheory.convolution DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul FourierPair.fourierInv_fourier_eq instFourierPair fourierInv_coe MeasureTheory.integral_congr_ae Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass fourier_convolution_apply Continuous.fourierInv_fourier_eq BddAbove.continuous_convolution_right_of_integrable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real norm_le_seminorm integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume continuous MeasureTheory.Integrable.integrable_convolution ContinuousAdd.measurableMul₂ ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourier_convolution pairing_apply_apply
convolution_continuous_left 📖	mathematical	—	Continuous SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul LinearMap.instFunLike convolution	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.continuous SMulCommClass.complexToReal instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul RingHomIsometric.ids
convolution_flip 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul LinearMap.instFunLike convolution ContinuousLinearMap.flip DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul RingHomIsometric.ids
fourier_convolution 📖	mathematical	—	FourierTransform.fourier SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransform DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul LinearMap.instFunLike convolution NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace pairing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace FourierInvPair.fourier_fourierInv_eq instFourierInvPair
fourier_convolution_apply 📖	mathematical	—	DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFunLike FourierTransform.fourier instFourierTransform ContinuousLinearMap Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Complex.instRCLike RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass EuclideanDomain.toCommRing Field.toEuclideanDomain ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul LinearMap.instFunLike convolution Real.instFourierTransform MeasureTheory.convolution DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourier_convolution Real.fourier_bilin_convolution_eq integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real continuous

---

← Back to Index