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 #

source

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

Instances For

source

@[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

source

@[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

source

@[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

source

@[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 #

source

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

source

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)

source

@[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

source

@[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

source

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

source

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)

source

@[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

source

@[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

source

@[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

source

@[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 #

source

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

Instances For

source

def «term_∗^ₙ_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

@[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

source

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

source

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

source

@[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

source

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

source

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

source

@[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

source

@[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

source

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

source

@[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

source

@[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

Documentation

APAP.Prereqs.Convolution.Compact

Convolution in the compact normalisation #

Main declarations #

Notation #

Notes #

Convolution of functions #

Trivial character #

Convolution #

Iterated convolution #