Convolution

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

Main declarations

• conv: Discrete convolution of two functions
• dconv: 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 indicate_conv_indicate_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 ∗ 𝟭 t) a = ↑(Finset.filter (fun (x : G × G) => x.1 + x.2 = a) (s ×ˢ t)).card

theorem indicate_conv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (s : Finset G) (f : G → R) : 𝟭 s ∗ f = ∑ a ∈ s, translate a f

theorem conv_indicate {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] (f : G → R) (s : Finset G) : f ∗ 𝟭 s = ∑ a ∈ s, translate a f

theorem indicate_conv_indicate_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 ∗ 𝟭 t) a = ↑((-a +ᵥ s) ∩ -t).card

theorem indicate_dconv_indicate_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 ○ 𝟭 t) a = ↑(Finset.filter (fun (x : G × G) => x.1 - x.2 = a) (s ×ˢ t)).card

theorem indicate_dconv {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 ○ f = ∑ a ∈ s, translate a (conjneg f)

theorem dconv_indicate {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 = ∑ a ∈ s, translate (-a) f

@[simp]

theorem mu_univ_conv_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_conv {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 conv_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_dconv_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_dconv {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 dconv_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_conv {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_conv' {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_dconv {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_dconv' {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_conv {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_dconv {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 indicate_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 ∗^ n) a = ↑(Finset.filter (fun (x : Fin n → G) => ∑ i : Fin n, x i = a) (Fintype.piFinset fun (x : Fin n) => s)).card

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

theorem conv_indicate_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 ∗^ n = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (∑ i : Fin n, a i) f

theorem indicate_iterConv_dconv {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 ∗^ n ○ f = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (∑ i : Fin n, a i) (conjneg f)

theorem dconv_indicate_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 ∗^ n = ∑ a ∈ Fintype.piFinset fun (x : Fin n) => s, translate (-∑ i : Fin n, a i) f

theorem mu_iterConv_conv {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 conv_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 mu_iterConv_dconv {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 dconv_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