Convolution

This file defines convolution of finite subsets A and B of group G as the map A ⋆ B : G → ℕ that maps x ∈ G to the number of distinct representations of x in the form x = ab for a ∈ A, b ∈ B. It is shown how convolution behaves under the change of order of A and B, as well as under the left and right actions on A, B, and the function argument.

def Finset.convolution {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : G → ℕ

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.

def Finset.addConvolution {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : G → ℕ

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.

theorem Finset.card_smul_inter_smul {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (x y : G) : (x • A ∩ y • B).card = A.convolution B⁻¹ (x⁻¹ * y)

theorem Finset.card_vadd_inter_vadd {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (x y : G) : ((x +ᵥ A) ∩ (y +ᵥ B)).card = A.addConvolution (-B) (-x + y)

theorem Finset.card_inter_smul {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (x : G) : (A ∩ x • B).card = A.convolution B⁻¹ x

theorem Finset.card_inter_vadd {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (x : G) : (A ∩ (x +ᵥ B)).card = A.addConvolution (-B) x

theorem Finset.card_smul_inter {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (x : G) : (x • A ∩ B).card = A.convolution B⁻¹ x⁻¹

theorem Finset.card_vadd_inter {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (x : G) : ((x +ᵥ A) ∩ B).card = A.addConvolution (-B) (-x)

theorem Finset.card_mul_inv_eq_convolution_inv {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (x : G) : {ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}.card = A.convolution B⁻¹ x

theorem Finset.card_add_neg_eq_addConvolution_neg {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (x : G) : {ab ∈ A ×ˢ B | ab.1 + -ab.2 = x}.card = A.addConvolution (-B) x

@[simp]

theorem Finset.convolution_pos {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} {x : G} : 0 < A.convolution B x ↔ x ∈ A * B

@[simp]

theorem Finset.addConvolution_pos {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} {x : G} : 0 < A.addConvolution B x ↔ x ∈ A + B

theorem Finset.convolution_ne_zero {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} {x : G} : A.convolution B x ≠ 0 ↔ x ∈ A * B

theorem Finset.addConvolution_ne_zero {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} {x : G} : A.addConvolution B x ≠ 0 ↔ x ∈ A + B

@[simp]

theorem Finset.convolution_eq_zero {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} {x : G} : A.convolution B x = 0 ↔ x ∉ A * B

@[simp]

theorem Finset.addConvolution_eq_zero {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} {x : G} : A.addConvolution B x = 0 ↔ x ∉ A + B

theorem Finset.convolution_le_card_left {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} {x : G} : A.convolution B x ≤ A.card

theorem Finset.addConvolution_le_card_left {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} {x : G} : A.addConvolution B x ≤ A.card

theorem Finset.convolution_le_card_right {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} {x : G} : A.convolution B x ≤ B.card

theorem Finset.addConvolution_le_card_right {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} {x : G} : A.addConvolution B x ≤ B.card

@[simp]

theorem Finset.convolution_inv {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (x : G) : A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x

@[simp]

theorem Finset.addConvolution_neg {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (x : G) : A.addConvolution B (-x) = (-B).addConvolution (-A) x

@[simp]

theorem Finset.op_smul_convolution_eq_convolution_smul {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (s : G) : (MulOpposite.op s • A).convolution B = A.convolution (s • B)

@[simp]

theorem Finset.op_vadd_addConvolution_eq_addConvolution_vadd {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (s : G) : (AddOpposite.op s +ᵥ A).addConvolution B = A.addConvolution (s +ᵥ B)

@[simp]

theorem Finset.smul_convolution_eq_convolution_inv_mul {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (s x : G) : (s • A).convolution B x = A.convolution B (s⁻¹ * x)

@[simp]

theorem Finset.vadd_addConvolution_eq_addConvolution_neg_add {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (s x : G) : (s +ᵥ A).addConvolution B x = A.addConvolution B (-s + x)

@[simp]

theorem Finset.convolution_op_smul_eq_convolution_mul_inv {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) (s x : G) : A.convolution (MulOpposite.op s • B) x = A.convolution B (x * s⁻¹)

@[simp]

theorem Finset.addConvolution_op_vadd_eq_addConvolution_add_neg {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) (s x : G) : A.addConvolution (AddOpposite.op s +ᵥ B) x = A.addConvolution B (x + -s)