Convolution in the compact normalisation

This file defines several versions of the discrete convolution of functions with the compact normalisation.

Main declarations

• conv: Discrete convolution of two functions in the compact normalisation
• dconv: Discrete difference convolution of two functions in the compact normalisation
• iterConv: Iterated convolution of a function in the compact normalisation

Notation

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

Notes

Some lemmas could technically be generalised to a division ring. 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.

def conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : G → K

Compact convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b + c = a.

Equations

• (f ∗ g) a = {x : G × G | x.1 + x.2 = a}.expect fun (x : G × G) => f x.1 * g x.2

def «term_∗_» : Lean.TrailingParserDescr

Compact convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b + c = a.

Equations

• «term_∗_» = Lean.ParserDescr.trailingNode `«term_∗_» 71 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗ ") (Lean.ParserDescr.cat `term 72))

theorem conv_apply {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = {x : G × G | x.1 + x.2 = a}.expect fun (x : G × G) => f x.1 * g x.2

theorem conv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : f ∗ g = g ∗ f

theorem conv_eq_expect_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f (a - t) * g t

theorem conv_eq_expect_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f (a + t) * g (-t)

theorem conv_eq_expect_sub' {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f t * g (a - t)

theorem conv_apply_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a b : G) : (f ∗ g) (a + b) = Finset.univ.expect fun (t : G) => f (a + t) * g (b - t)

def dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : G → K

Compact difference convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b - c = a.

Equations

• (f ○ g) a = {x : G × G | x.1 - x.2 = a}.expect fun (x : G × G) => f x.1 * (starRingEnd (G → K)) g x.2

def «term_○_» : Lean.TrailingParserDescr

Compact difference convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b - c = a.

Equations

• «term_○_» = Lean.ParserDescr.trailingNode `«term_○_» 71 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 72))

@[simp]

theorem conv_conjneg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : f ∗ conjneg g = f ○ g

@[simp]

theorem conj_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (starRingEnd (G → K)) (f ∗ g) = (starRingEnd (G → K)) f ∗ (starRingEnd (G → K)) g

@[simp]

theorem conj_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (starRingEnd (G → K)) (f ○ g) = (starRingEnd (G → K)) f ○ (starRingEnd (G → K)) g

theorem IsSelfAdjoint.conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] {f g : G → K} [StarRing K] (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ g)

theorem IsSelfAdjoint.dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] {f g : G → K} [StarRing K] (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ g)

theorem dconv_eq_expect_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = Finset.univ.expect fun (t : G) => f (a + t) * (starRingEnd K) (g t)

theorem dconv_eq_expect_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = Finset.univ.expect fun (t : G) => f t * (starRingEnd K) (g (t - a))

theorem expect_dconv_mul {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h : G → K) : (Finset.univ.expect fun (a : G) => (f ○ g) a * h a) = Finset.univ.expect fun (a : G) => Finset.univ.expect fun (b : G) => f a * (starRingEnd K) (g b) * h (a - b)

theorem expect_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (Finset.univ.expect fun (a : G) => (f ○ g) a) = (Finset.univ.expect fun (a : G) => f a) * Finset.univ.expect fun (a : G) => (starRingEnd K) (g a)

theorem dconv_indicator_one {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f : G → K) (s : Finset G) : (f ○ (↑s).indicator fun (x : G) => 1) = (↑(Fintype.card G))⁻¹ • ∑ a ∈ s, translate (-a) f

theorem indicator_one_dconv_indicator_one_eq_dens {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a = ↑(s ∩ (a +ᵥ t)).dens

theorem indicator_one_dconv_indicator_one_eq_addConvolution_div {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a = ↑(s.addConvolution (-t) a) / ↑(Fintype.card G)

theorem expect_indicator_one_dconv_indicator_one {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) : (Finset.univ.expect fun (a : G) => (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a) = ↑s.dens * ↑t.dens

theorem expect_indicator_one_dconv_indicator_sq {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) : (Finset.univ.expect fun (x : G) => (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) x ^ 2) = ↑(s.addEnergy' t)