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
• iterCConv: 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.

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.

Trivial character

def trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] : G → R

The trivial character.

Equations

• trivNChar a = if a = 0 then ↑(Fintype.card G) else 0

@[simp]

theorem trivNChar_apply {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] (a : G) : trivNChar a = if a = 0 then ↑(Fintype.card G) else 0

@[simp]

theorem conj_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] : (starRingEnd (G → R)) trivNChar = trivNChar

@[simp]

theorem conjneg_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] : conjneg trivNChar = trivNChar

@[simp]

theorem isSelfAdjoint_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [StarRing R] : IsSelfAdjoint trivNChar

Convolution

theorem conv_apply_eq_smul_ddconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) (a : G) : (f ∗ g) a = (↑(Fintype.card G))⁻¹ • (f ∗ᵈ g) a

theorem conv_eq_smul_ddconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) : f ∗ g = (↑(Fintype.card G))⁻¹ • (f ∗ᵈ g)

@[simp]

theorem conv_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : f ∗ trivNChar = f

@[simp]

theorem trivNChar_conv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : trivNChar ∗ f = f

theorem dconv_apply_eq_smul_dddconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) (a : G) : (f ○ g) a = (↑(Fintype.card G))⁻¹ • (f ○ᵈ g) a

theorem dconv_eq_smul_dddconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) : f ○ g = (↑(Fintype.card G))⁻¹ • (f ○ᵈ g)

@[simp]

theorem dconv_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) : f ○ trivNChar = f

@[simp]

theorem trivNChar_dconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) : trivNChar ○ f = conjneg f

@[simp]

theorem one_conv_one {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] : 1 ∗ 1 = 1

@[simp]

theorem one_dconv_one {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] : 1 ○ 1 = 1

Iterated convolution

def iterCConv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : ℕ → G → R

Iterated convolution.

Equations

• f ∗^ₙ 0 = trivNChar
• f ∗^ₙ n.succ = f ∗^ₙ n ∗ f

def «term_∗^ₙ_» : Lean.TrailingParserDescr

Equations

• «term_∗^ₙ_» = Lean.ParserDescr.trailingNode `«term_∗^ₙ_» 78 78 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗^ₙ ") (Lean.ParserDescr.cat `term 79))

@[simp]

theorem iterCConv_zero {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : f ∗^ₙ 0 = trivNChar

@[simp]

theorem iterCConv_one {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : f ∗^ₙ 1 = f

theorem iterCConv_succ {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗^ₙ n ∗ f

theorem iterCConv_succ' {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗ f ∗^ₙ n

theorem iterCConv_add {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (m n : ℕ) : f ∗^ₙ (m + n) = f ∗^ₙ m ∗ f ∗^ₙ n

theorem iterCConv_mul {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (m n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ m ∗^ₙ n

theorem iterCConv_mul' {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (m n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ n ∗^ₙ m

theorem iterCConv_conv_distrib {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) (n : ℕ) : (f ∗ g) ∗^ₙ n = f ∗^ₙ n ∗ g ∗^ₙ n

@[simp]

theorem zero_iterCConv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] {n : ℕ} : n ≠ 0 → 0 ∗^ₙ n = 0

@[simp]

theorem smul_iterCConv {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f : G → R) (n : ℕ) : (c • f) ∗^ₙ n = c ^ n • f ∗^ₙ n

theorem comp_iterCConv {G : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) (n : ℕ) : ⇑m ∘ (f ∗^ₙ n) = ⇑m ∘ f ∗^ₙ n

theorem expect_iterCConv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (n : ℕ) : (Finset.univ.expect fun (a : G) => (f ∗^ₙ n) a) = (Finset.univ.expect fun (a : G) => f a) ^ n

@[simp]

theorem iterCConv_trivNChar {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (n : ℕ) : trivNChar ∗^ₙ n = trivNChar

theorem support_iterCConv_subset {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (n : ℕ) : Function.support (f ∗^ₙ n) ⊆ n • Function.support f

theorem map_iterCConv {G : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [Semifield S] [CharZero S] (m : R →+* S) (f : G → R) (a : G) (n : ℕ) : m ((f ∗^ₙ n) a) = (⇑m ∘ f ∗^ₙ n) a

@[simp]

theorem conj_iterCConv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) (n : ℕ) : (starRingEnd (G → R)) (f ∗^ₙ n) = (starRingEnd (G → R)) f ∗^ₙ n

@[simp]

theorem conjneg_iterCConv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) (n : ℕ) : conjneg (f ∗^ₙ n) = conjneg f ∗^ₙ n

theorem iterCConv_dconv_distrib {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) (n : ℕ) : (f ○ g) ∗^ₙ n = f ∗^ₙ n ○ g ∗^ₙ n

@[simp]

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

@[simp]

theorem NNReal.coe_iterCConv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f : G → NNReal) (n : ℕ) (a : G) : ↑((f ∗^ₙ n) a) = (toReal ∘ f ∗^ₙ n) a