Documentation Verification Report

Convolution

📁 Source: Mathlib/NumberTheory/LSeries/Convolution.lean

Statistics

Metric	Count
Definitions `convolution`, `«term_⍟_»`, `toArithmeticFunction`	3
Theorems `LSeriesHasSum_mul`, `LSeriesSummable_mul`, `LSeries_mul`, `LSeries_mul'`, `coe_mul`, `toArithmeticFunction_eq_self`, `abscissaOfAbsConv_convolution_le`, `convolution_congr`, `convolution_def`, `convolution_map_zero`, `term_convolution`, `term_convolution'`, `convolution`, `convolution`, `LSeries_convolution`, `LSeries_convolution'`, `toArithmeticFunction_congr`	17
Total	20

ArithmeticFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesHasSum_mul` 📖	mathematical	`LSeriesHasSum` `DFunLike.coe` `ArithmeticFunction` `Complex` `Complex.instZero` `instFunLikeNat`	`instMul` `Complex.instSemiring` `Complex.instMul`	—	`LSeriesHasSum.convolution` `coe_mul`
`LSeriesSummable_mul` 📖	mathematical	`LSeriesSummable` `DFunLike.coe` `ArithmeticFunction` `Complex` `Complex.instZero` `instFunLikeNat`	`instMul` `Complex.instSemiring`	—	`LSeriesSummable.convolution` `coe_mul`
`LSeries_mul` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `DFunLike.coe` `ArithmeticFunction` `Complex` `Complex.instZero` `instFunLikeNat` `Real.toEReal` `Complex.re`	`LSeries` `instMul` `Complex.instSemiring` `Complex.instMul`	—	`LSeries_convolution` `coe_mul`
`LSeries_mul'` 📖	mathematical	`LSeriesSummable` `DFunLike.coe` `ArithmeticFunction` `Complex` `Complex.instZero` `instFunLikeNat`	`LSeries` `instMul` `Complex.instSemiring` `Complex.instMul`	—	`LSeries_convolution'` `coe_mul`
`coe_mul` 📖	mathematical	—	`LSeries.convolution` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLikeNat` `instMul`	—	`toArithmeticFunction_eq_self`
`toArithmeticFunction_eq_self` 📖	mathematical	—	`toArithmeticFunction` `DFunLike.coe` `ArithmeticFunction` `instFunLikeNat`	—	`ext` `map_zero`

LSeries

Definitions

Name	Category	Theorems
`convolution` 📖	CompOp	18 math math: `convolution_one_eq_convolution_zeta`, `term_convolution'`, `convolution_def`, `LSeriesHasSum.convolution`, `ArithmeticFunction.coe_mul`, `ArithmeticFunction.convolution_vonMangoldt_const_one`, `ArithmeticFunction.convolution_vonMangoldt_zeta`, `LSeries_convolution'`, `term_convolution`, `DirichletCharacter.convolution_twist_vonMangoldt`, `abscissaOfAbsConv_convolution_le`, `DirichletCharacter.mul_convolution_distrib`, `LSeriesSummable.convolution`, `one_convolution_eq_zeta_convolution`, `convolution_congr`, `DirichletCharacter.convolution_mul_moebius`, `convolution_map_zero`, `LSeries_convolution`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abscissaOfAbsConv_convolution_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `convolution` `Complex` `Complex.instSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal`	—	`abscissaOfAbsConv_binop_le` `LSeriesSummable.convolution`
`convolution_congr` 📖	mathematical	—	`convolution`	—	`toArithmeticFunction_congr`
`convolution_def` 📖	mathematical	—	`convolution` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.divisorsAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `mul_ite` `MulZeroClass.mul_zero` `ite_mul` `MulZeroClass.zero_mul` `Nat.ne_zero_of_mem_divisorsAntidiagonal`
`convolution_map_zero` 📖	mathematical	—	`convolution` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`convolution_def` `Finset.sum_congr` `Nat.divisorsAntidiagonal_zero`
`term_convolution` 📖	mathematical	—	`term` `convolution` `Complex` `Complex.instSemiring` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Nat.divisorsAntidiagonal` `Complex.instMul`	—	`eq_or_ne` `Finset.sum_congr` `Nat.divisorsAntidiagonal_zero` `term_of_ne_zero` `convolution_def` `Finset.sum_div` `Nat.ne_zero_of_mem_divisorsAntidiagonal` `mul_comm_div` `div_div` `mul_div_assoc` `Complex.natCast_mul_natCast_cpow` `Nat.cast_mul` `mul_comm` `Nat.mem_divisorsAntidiagonal`
`term_convolution'` 📖	mathematical	—	`term` `convolution` `Complex` `Complex.instSemiring` `tsum` `Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instMul` `Set.instMembership` `SummationFilter.unconditional`	—	`eq_or_ne` `term_zero` `Set.ext` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `tsum_zero` `Finset.tsum_subtype'` `term_convolution`

LSeries.notation

Definitions

Name	Category	Theorems
`«term_⍟_»` 📖	CompOp	—

LSeriesHasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convolution` 📖	mathematical	`LSeriesHasSum`	`LSeries.convolution` `Complex` `Complex.instSemiring` `Complex.instMul`	—	`summable_mul_of_summable_norm` `Complex.instCompleteSpace` `Summable.norm` `Complex.instFiniteDimensionalReal` `HasSum.summable` `LSeries.term_convolution'` `HasSum.tsum_fiberwise` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.instT2Space` `HasSum.mul` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`

LSeriesSummable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convolution` 📖	mathematical	`LSeriesSummable`	`LSeries.convolution` `Complex` `Complex.instSemiring`	—	`LSeriesHasSum.LSeriesSummable` `LSeriesHasSum.convolution` `LSeriesHasSum`

(root)

Definitions

Name	Category	Theorems
`toArithmeticFunction` 📖	CompOp	4 math math: `ArithmeticFunction.toArithmeticFunction_eq_self`, `DirichletCharacter.apply_eq_toArithmeticFunction_apply`, `DirichletCharacter.isMultiplicative_toArithmeticFunction`, `toArithmeticFunction_congr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_convolution` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`LSeries` `LSeries.convolution` `Complex` `Complex.instSemiring` `Complex.instMul`	—	`LSeries_convolution'` `LSeriesSummable_of_abscissaOfAbsConv_lt_re`
`LSeries_convolution'` 📖	mathematical	`LSeriesSummable`	`LSeries` `LSeries.convolution` `Complex` `Complex.instSemiring` `Complex.instMul`	—	`LSeriesHasSum.LSeries_eq` `LSeriesHasSum.convolution` `LSeriesSummable.LSeriesHasSum`
`toArithmeticFunction_congr` 📖	mathematical	—	`toArithmeticFunction`	—	`ArithmeticFunction.ext`

---

← Back to Index