Convolution

The convolution of two functions is defined as #m/def/anal/fun

This forms a commutative, associative, bilinear product on integrable functions, thereby forming an -monoid.

Proof

For commutativity, note

Distributivity follows from Fubini's theorem. For linearity, note

and linearity in the other argument follows from commutativity.

#state/develop | #lang/en | #SemBr