Discrete Convolution API Design

Stream: mathlib4

[Fengyang Wang]

This is a topic derived from my PR #33130 where we formalized commutative unital Banach algebra structure of Cauchy product over l1 space. According to the feedback I got, there are two generalizations to be made to fit into Mathlib.

• Cauhcy product is specialized discrete convolution (finite support), but discrete convolution doesn't fit well in the existing MeasureTheory.convolution since a [AddGroup] structure is needed for operation x ↦ ∫ f(t)g(x - t) ∂t while the most common index ℕ is [AddMonoid].
• For reasons above, Discrete convolution warrants its own API

So there I go, I propose the following API design.

Basic setup

Discrete Convolution

Given two functions f, g : M → R where [Monoid M] and [Ring R], their convolution at a point x sums over all pairs (a, b) whose product equals x (MulFiber\`AddFiber`):

(f ⋆ g)(x) = ∑ f(a) · g(b)
            a·b = x

Typeclass Signature

Variable	Type	Role
M	[Monoid M] or [AddMonoid M]	Index set; elements label "positions" (e.g., ℕ for polynomial degrees, G for group algebra basis)
R	[CommSemiring R] or [NormedCommRing R]	Coefficient ring where function values live
f, g	M → R	Input functions to convolve
x	M	Point at which (f ⋆ g)(x) is evaluated
a, b	M	Summation indices satisfying a · b = x (or a + b = x for additive)

Generalized (bilinear) convolution:

Variable	Type	Role
S	[CommSemiring S]	Scalar ring for module structures
E, E', F	[Module S E], etc.	Codomains: f : M → E, g : M → E', result in F
L	E →ₗ[S] E' →ₗ[S] F	Bilinear map combining values; e.g., LinearMap.mul R R for ring multiplication

### Notations

| Notation     | Index Type           | Operation                                       |
|--------------|----------------------|-------------------------------------------------|
| `f ⋆[L] g`   | `Monoid M`           | `∑' ab : mulFiber x, L (f ab.1.1) (g ab.1.2)`   |
| `f ⋆₊[L] g`  | `AddMonoid M`        | `∑' ab : addFiber x, L (f ab.1.1) (g ab.1.2)`   |
| `f ⋆ₘ g`     | `Monoid M`           | `∑' ab : mulFiber x, f ab.1.1 * g ab.1.2`       |
| `f ⋆₊ₘ g`    | `AddMonoid M`        | `∑' ab : addFiber x, f ab.1.1 * g ab.1.2`       |
| `a ⋆ b`      | `HasAntidiagonal G`  | `∑ kl ∈ antidiagonal n, a kl.1 * b kl.2`        |

Examples (Semantic)

Additive index [AddMonoid ℕ] (power series):

(f ⋆ g)(3) = f(0)·g(3) + f(1)·g(2) + f(2)·g(1) + f(3)·g(0)

This is polynomial multiplication: if f and g represent coefficients, then (f ⋆ g)(n)
is the n-th coefficient of the product.

Multiplicative index [Group G] (group algebras):

(f ⋆ g)(x) = ∑ f(a) · g(b)    where a, b range over all pairs with a·b = x
            a·b = x

Cauchy Product as [HasAntidiagonal] type (Counterpart of HasCompactSupport in MeasureTheory.convolution)

namespace CauchyProduct

variable [AddMonoid G] [HasAntidiagonal G] [Semiring R]

/-- Cauchy product (convolution) via finite antidiagonal sum. -/
def apply (a b : G → R) : G → R :=
  fun n => ∑ kl ∈ antidiagonal n, a kl.1 * b kl.2

-- code

/-- `addMulConvolution` equals `CauchyProduct.apply` for `HasAntidiagonal` types. -/
theorem addMulConvolution_eq_cauchyProduct (f g : M → R) (x : M) :
    (f ⋆₊ₘ g) x = CauchyProduct.apply f g x := by

Extendibility

As per #30391, this extends to weighted concatenation of languages via FreeAddMonoid.

Current TODO

• Associativity for general bilinear maps (requires composition of bilinear maps);
  currently only proved for ℓ¹ ring multiplication in LpOneBanachAlgebra.lean

• Bridge to MeasureTheory.convolution: prove addMulConvolution f g = MeasureTheory.convolution f g (.mul ℝ R) Measure.count for [AddGroup M]

Concerns

• Notation collision: ⋆[L] in discrete vs MeasureTheory (volume default)
• There are definitely more concerns. Haven't figured out how to put them down in words.

I would love to hear your opinions on the current design. Where did I do well, where did I act silly, and what is the next step?

[Yaël Dillies]

Note that I have quite a bit about discrete convolution in APAP: https://yaeldillies.github.io/LeanAPAP/docs/LeanAPAP/Prereqs/Convolution/Discrete/Defs.html#conv

[Yaël Dillies]

I haven't pushed it to mathlib yet because I realised that in fact I wanted the compact convolution instead!

[Fengyang Wang]

Yaël Dillies said:

Note that I have quite a bit about discrete convolution in APAP: https://yaeldillies.github.io/LeanAPAP/docs/LeanAPAP/Prereqs/Convolution/Discrete/Defs.html#conv

Thank you! A key difference of the two approaches, according to the feedback I got from code reviews, we would like a discrete conv API for [Monoid M] and tsum. Your implementation is definitely enlightening. I'd like to know how you would like me to note if I were to carry over some functionalities from your implementation of discrete convolution?

[Yaël Dillies]

tsum is indeed the furthest you can go with the counting measure, but generality wasn't the only main concern in my case: I wanted something usable for the purpose of additive combinatorics, with as few unnecessary requirements (such as summability) as possible. What do you want to use the discrete convolution for?

[Fengyang Wang]

Mainly for establishing the Banach algebra structure of l1 space (initially weighted l1 norm) w.r.t. Cauchy product (dis. conv. w/ fin. supp.) in Mathlin (Analysis/Lp), but ended up needing to develop a whole API to make the maintainers happy. A notable use is this new implementation of a more general discrete conv. can be used in weighted concatenation of languages via List ~ free additive monoid.