DiscreteConvolution

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/DiscreteConvolution.lean

Statistics

Metric	Count
Definitions AddConvolutionExists, AddConvolutionExistsAt, ConvolutionExists, ConvolutionExistsAt, addConvolution, addFiber, convolution, mulFiber, «term_⋆[_]_», «term_⋆₊[_]_»	10
Theorems add_distrib, distrib_add, add_distrib, convolution_vadd, distrib_add, vadd_convolution, add_distrib, distrib_add, add_distrib, convolution_smul, distrib_add, smul_convolution, addConvolution_comm, addConvolution_indicator_zero_left, addConvolution_indicator_zero_right, addConvolution_zero, addFiber_zero_mem, convolution_comm, convolution_indicator_one_left, convolution_indicator_one_right, convolution_zero, mem_addFiber, mem_mulFiber, mulFiber_one_mem, zero_addConvolution, zero_convolution	26
Total	36

DiscreteConvolution

Definitions

Name	Category	Theorems
AddConvolutionExists 📖	MathDef	—
AddConvolutionExistsAt 📖	MathDef	—
ConvolutionExists 📖	MathDef	—
ConvolutionExistsAt 📖	MathDef	—
addConvolution 📖	CompOp	11 math math: AddConvolutionExists.add_distrib, addConvolution_zero, AddConvolutionExistsAt.convolution_vadd, zero_addConvolution, AddConvolutionExistsAt.distrib_add, AddConvolutionExistsAt.vadd_convolution, addConvolution_indicator_zero_left, addConvolution_comm, addConvolution_indicator_zero_right, AddConvolutionExistsAt.add_distrib, AddConvolutionExists.distrib_add
addFiber 📖	CompOp	2 math math: addFiber_zero_mem, mem_addFiber
convolution 📖	CompOp	11 math math: convolution_zero, ConvolutionExists.distrib_add, ConvolutionExists.add_distrib, convolution_comm, ConvolutionExistsAt.add_distrib, ConvolutionExistsAt.smul_convolution, ConvolutionExistsAt.convolution_smul, convolution_indicator_one_right, convolution_indicator_one_left, ConvolutionExistsAt.distrib_add, zero_convolution
mulFiber 📖	CompOp	2 math math: mem_mulFiber, mulFiber_one_mem
«term_⋆[_]_» 📖	CompOp	—
«term_⋆₊[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addConvolution_comm 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	addConvolution AddCommMonoid.toAddMonoid	—	smulCommClass_self Equiv.tsum_eq
addConvolution_indicator_zero_left 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	addConvolution Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set Set.instSingletonSet	—	smulCommClass_self Set.indicator_apply tsum_eq_single SummationFilter.instLeAtTopUnconditional Set.mem_singleton_iff
addConvolution_indicator_zero_right 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	addConvolution Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set Set.instSingletonSet	—	smulCommClass_self Set.indicator_apply tsum_eq_single SummationFilter.instLeAtTopUnconditional Set.mem_singleton_iff
addConvolution_zero 📖	mathematical	—	addConvolution Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tsum_zero
addFiber_zero_mem 📖	mathematical	—	Set Set.instMembership addFiber AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Set.mem_addAntidiagonal Set.mem_univ add_zero
convolution_comm 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	convolution CommMonoid.toMonoid	—	smulCommClass_self Equiv.tsum_eq
convolution_indicator_one_left 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	convolution Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set Set.instSingletonSet MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	smulCommClass_self Set.indicator_apply tsum_eq_single SummationFilter.instLeAtTopUnconditional
convolution_indicator_one_right 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	convolution Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set Set.instSingletonSet MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	smulCommClass_self Set.indicator_apply tsum_eq_single SummationFilter.instLeAtTopUnconditional
convolution_zero 📖	mathematical	—	convolution Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tsum_zero
mem_addFiber 📖	mathematical	—	Set Set.instMembership addFiber AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Set.mem_addAntidiagonal Set.mem_univ
mem_mulFiber 📖	mathematical	—	Set Set.instMembership mulFiber MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
mulFiber_one_mem 📖	mathematical	—	Set Set.instMembership mulFiber MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mul_one
zero_addConvolution 📖	mathematical	—	addConvolution Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tsum_zero
zero_convolution 📖	mathematical	—	convolution Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smulCommClass_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tsum_zero

DiscreteConvolution.AddConvolutionExists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_distrib 📖	mathematical	DiscreteConvolution.AddConvolutionExists	DiscreteConvolution.addConvolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self DiscreteConvolution.AddConvolutionExistsAt.add_distrib
distrib_add 📖	mathematical	DiscreteConvolution.AddConvolutionExists	DiscreteConvolution.addConvolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self DiscreteConvolution.AddConvolutionExistsAt.distrib_add

DiscreteConvolution.AddConvolutionExistsAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_distrib 📖	mathematical	DiscreteConvolution.AddConvolutionExistsAt	DiscreteConvolution.addConvolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Summable.tsum_add SummationFilter.instNeBotUnconditional
convolution_vadd 📖	mathematical	DiscreteConvolution.AddConvolutionExistsAt	DiscreteConvolution.addConvolution Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Summable.tsum_const_smul SummationFilter.instNeBotUnconditional
distrib_add 📖	mathematical	DiscreteConvolution.AddConvolutionExistsAt	DiscreteConvolution.addConvolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Summable.tsum_add SummationFilter.instNeBotUnconditional
vadd_convolution 📖	mathematical	DiscreteConvolution.AddConvolutionExistsAt	DiscreteConvolution.addConvolution Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Summable.tsum_const_smul SummationFilter.instNeBotUnconditional

DiscreteConvolution.ConvolutionExists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_distrib 📖	mathematical	DiscreteConvolution.ConvolutionExists	DiscreteConvolution.convolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self DiscreteConvolution.ConvolutionExistsAt.add_distrib
distrib_add 📖	mathematical	DiscreteConvolution.ConvolutionExists	DiscreteConvolution.convolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self DiscreteConvolution.ConvolutionExistsAt.distrib_add

DiscreteConvolution.ConvolutionExistsAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_distrib 📖	mathematical	DiscreteConvolution.ConvolutionExistsAt	DiscreteConvolution.convolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Summable.tsum_add SummationFilter.instNeBotUnconditional
convolution_smul 📖	mathematical	DiscreteConvolution.ConvolutionExistsAt	DiscreteConvolution.convolution Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Summable.tsum_const_smul SummationFilter.instNeBotUnconditional
distrib_add 📖	mathematical	DiscreteConvolution.ConvolutionExistsAt	DiscreteConvolution.convolution Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Summable.tsum_add SummationFilter.instNeBotUnconditional
smul_convolution 📖	mathematical	DiscreteConvolution.ConvolutionExistsAt	DiscreteConvolution.convolution Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Summable.tsum_const_smul SummationFilter.instNeBotUnconditional

---

← Back to Index