English
Let A and B be finite subsets of a group G. The convolution A * B is the function from G to the natural numbers given by (A * B)(x) = |{(a,b) ∈ A × B : a b = x}|, i.e., the number of representations of x as a product ab with a ∈ A and b ∈ B.
Русский
Пусть A и B — конечные подмножества группы G. Свёртка A * B — это отображение G в натуральные числа, задаваемое (A * B)(x) = |{(a,b) ∈ A × B : a b = x}|, то есть число представлений x в виде ab с a ∈ A и b ∈ B.
LaTeX
$$$ (A * B)(x) = \#\{(a,b) \in A \times B \mid a b = x\} $$$
Lean4
/-- Given finite subsets `A` and `B` of a group `G`, convolution of `A` and `B` is a map `G → ℕ`
that maps `x ∈ G` to the number of distinct representations of `x` in the form `x = ab`, where
`a ∈ A`, `b ∈ B`. -/
@[to_additive addConvolution /-- Given finite subsets `A` and `B` of an additive group `G`,
convolution of `A` and `B` is a map `G → ℕ` that maps `x ∈ G` to the number of distinct
representations of `x` in the form `x = a + b`, where `a ∈ A`, `b ∈ B`. -/
]
def convolution (A B : Finset G) : G → ℕ := fun x => #({ab ∈ A ×ˢ B | ab.1 * ab.2 = x})
