Convolution

This file defines several versions of the discrete convolution of functions.

Main declarations

• ddconv: Discrete convolution of two functions
• dddconv: Discrete difference convolution of two functions
• iterConv: Iterated convolution of a function

Notation

• f ∗ᵈ g: Convolution
• f ○ᵈ g: Difference convolution
• f ∗ᵈ^ n: Iterated convolution

Notes

Some lemmas could technically be generalised to a non-commutative semiring domain. Doesn't seem very useful given that the codomain in applications is either ℝ, ℝ≥0 or ℂ.

Similarly we could drop the commutativity assumption on the domain, but this is unneeded at this point in time.

TODO

Multiplicativise? Probably ugly and not very useful.

Convolution of functions

In this section, we define the convolution f ∗ᵈ g and difference convolution f ○ᵈ g of functions f g : G → R, and show how they interact.

theorem indicator_one_ddconv_indicator_one_eq_sum {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ∗ᵈ (↑t).indicator fun (x : G) => 1) a = ↑{x ∈ s ×ˢ t | x.1 + x.2 = a}.card

theorem indicator_one_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s : Finset G) (f : G → R) : ((↑s).indicator fun (x : G) => 1) ∗ᵈ f = ∑ a ∈ s, translate a f

theorem ddconv_indicator_one {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (f : G → R) (s : Finset G) : (f ∗ᵈ (↑s).indicator fun (x : G) => 1) = ∑ a ∈ s, translate a f

theorem indicator_one_ddconv_indicator_one_eq_card_vadd_inter_neg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ∗ᵈ (↑t).indicator fun (x : G) => 1) a = ↑((-a +ᵥ s) ∩ -t).card

theorem indicator_one_dddconv_Set.indicator_apply {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ○ᵈ (↑t).indicator fun (x : G) => 1) a = ↑{x ∈ s ×ˢ t | x.1 - x.2 = a}.card

theorem indicator_one_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (s : Finset G) (f : G → R) : ((↑s).indicator fun (x : G) => 1) ○ᵈ f = ∑ a ∈ s, translate a (conjneg f)

theorem dddconv_indicator_one_eq_sum {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (f : G → R) (s : Finset G) : (f ○ᵈ (↑s).indicator fun (x : G) => 1) = ∑ a ∈ s, translate (-a) f

theorem dddconv_indicator_one {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (f : G → R) (s : Finset G) : (f ○ᵈ (↑s).indicator fun (x : G) => 1) = f ∗ᵈ (-↑s).indicator fun (x : G) => 1

@[simp]

theorem mu_univ_ddconv_mu_univ {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] : mu Finset.univ ∗ᵈ mu Finset.univ = mu Finset.univ

theorem mu_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] (s : Finset G) (f : G → R) : mu s ∗ᵈ f = (↑s.card)⁻¹ • ∑ a ∈ s, translate a f

theorem ddconv_mu {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] (f : G → R) (s : Finset G) : f ∗ᵈ mu s = (↑s.card)⁻¹ • ∑ a ∈ s, translate a f

@[simp]

theorem mu_univ_dddconv_mu_univ {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] : mu Finset.univ ○ᵈ mu Finset.univ = mu Finset.univ

theorem mu_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] (s : Finset G) (f : G → R) : mu s ○ᵈ f = (↑s.card)⁻¹ • ∑ a ∈ s, translate a (conjneg f)

theorem dddconv_mu {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] (f : G → R) (s : Finset G) : f ○ᵈ mu s = (↑s.card)⁻¹ • ∑ a ∈ s, translate (-a) f

theorem expect_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) : (Finset.univ.expect fun (a : G) => (f ∗ᵈ g) a) = (∑ a : G, f a) * Finset.univ.expect fun (a : G) => g a

theorem expect_ddconv' {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) : (Finset.univ.expect fun (a : G) => (f ∗ᵈ g) a) = (Finset.univ.expect fun (a : G) => f a) * ∑ a : G, g a

theorem expect_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) : (Finset.univ.expect fun (a : G) => (f ○ᵈ g) a) = (∑ a : G, f a) * Finset.univ.expect fun (a : G) => (starRingEnd R) (g a)

theorem expect_dddconv' {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) : (Finset.univ.expect fun (a : G) => (f ○ᵈ g) a) = (Finset.univ.expect fun (a : G) => f a) * ∑ a : G, (starRingEnd R) (g a)

@[simp]

theorem balance_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f g : G → R) : Fintype.balance (f ∗ᵈ g) = Fintype.balance f ∗ᵈ Fintype.balance g

@[simp]

theorem balance_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] [StarRing R] (f g : G → R) : Fintype.balance (f ○ᵈ g) = Fintype.balance f ○ᵈ Fintype.balance g

Iterated convolution

theorem indicator_one_iterConv_apply {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s : Finset G) (n : ℕ) (a : G) : (((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n) a = ↑{x ∈ Fintype.piFinset fun (x : Fin n) => s | ∑ i : Fin n, x i = a}.card

theorem indicator_one_iterConv_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s : Finset G) (n : ℕ) (f : G → R) : ((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n ∗ᵈ f = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (∑ i : Fin n, a i) f

theorem ddconv_indicator_one_iterConv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (f : G → R) (s : Finset G) (n : ℕ) : f ∗ᵈ ((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (∑ i : Fin n, a i) f

theorem indicator_one_iterConv_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (s : Finset G) (n : ℕ) (f : G → R) : ((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n ○ᵈ f = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (∑ i : Fin n, a i) (conjneg f)

theorem dddconv_indicator_one_iterConv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] (f : G → R) (s : Finset G) (n : ℕ) : f ○ᵈ ((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (-∑ i : Fin n, a i) f

theorem mu_iterConv_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (s : Finset G) (n : ℕ) (f : G → R) : mu s ∗ᵈ^ n ∗ᵈ f = (Fintype.piFinset fun (x : Fin n) => s).expect fun (a : Fin n → G) => translate (∑ i : Fin n, a i) f

theorem ddconv_mu_iterConv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (s : Finset G) (n : ℕ) : f ∗ᵈ mu s ∗ᵈ^ n = (Fintype.piFinset fun (x : Fin n) => s).expect fun (a : Fin n → G) => translate (∑ i : Fin n, a i) f

theorem Finset.dens_addSubgroup_preimage_vadd_eq_indicator_one_ddconv_mu {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (a : G) (B : Finset G) {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] (V : S) [Fintype ↥V] : ↑((-a +ᵥ B).preimage Subtype.val ⋯).dens = (((↑B).indicator fun (x : G) => 1) ∗ᵈ mu (↑V).toFinset) a

theorem mu_iterConv_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (s : Finset G) (n : ℕ) (f : G → R) : mu s ∗ᵈ^ n ○ᵈ f = (Fintype.piFinset fun (x : Fin n) => s).expect fun (a : Fin n → G) => translate (∑ i : Fin n, a i) (conjneg f)

theorem dddconv_mu_iterConv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) (s : Finset G) (n : ℕ) : f ○ᵈ mu s ∗ᵈ^ n = (Fintype.piFinset fun (x : Fin n) => s).expect fun (a : Fin n → G) => translate (-∑ i : Fin n, a i) f

@[simp]

theorem balance_iterConv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f : G → R) {n : ℕ} : n ≠ 0 → Fintype.balance (f ∗ᵈ^ n) = Fintype.balance f ∗ᵈ^ n