Convolution in the compact normalisation

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

Main declarations

• cconv: Discrete convolution of two functions in the compact normalisation
• cdconv: 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

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

Convolution

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

Equations

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

theorem cconv_apply {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 = {x : G × G | x.1 + x.2 = a}.expect fun (x : G × G) => f x.1 * g x.2

theorem cconv_apply_eq_smul_conv {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 cconv_eq_smul_conv {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 cconv_zero {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) : f ∗ₙ 0 = 0

@[simp]

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

theorem cconv_add {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g h : G → R) : f ∗ₙ (g + h) = f ∗ₙ g + f ∗ₙ h

theorem add_cconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g h : G → R) : (f + g) ∗ₙ h = f ∗ₙ h + g ∗ₙ h

theorem smul_cconv {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ∗ₙ g = c • (f ∗ₙ g)

theorem cconv_smul {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [DistribSMul H R] [SMulCommClass H R R] (c : H) (f g : G → R) : f ∗ₙ c • g = c • (f ∗ₙ g)

theorem smul_cconv_assoc {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ∗ₙ g = c • (f ∗ₙ g)

Alias of smul_cconv.

theorem smul_cconv_left_comm {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [DistribSMul H R] [SMulCommClass H R R] (c : H) (f g : G → R) : f ∗ₙ c • g = c • (f ∗ₙ g)

Alias of cconv_smul.

@[simp]

theorem translate_cconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (a : G) (f g : G → R) : translate a f ∗ₙ g = translate a (f ∗ₙ g)

@[simp]

theorem cconv_translate {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (a : G) (f g : G → R) : f ∗ₙ translate a g = translate a (f ∗ₙ g)

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

theorem mul_smul_cconv_comm {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 d : H) (f g : G → R) : (c * d) • (f ∗ₙ g) = c • f ∗ₙ d • g

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

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

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

theorem cconv_cconv_cconv_comm {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g h i : G → R) : f ∗ₙ g ∗ₙ (h ∗ₙ i) = f ∗ₙ h ∗ₙ (g ∗ₙ i)

theorem map_cconv {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 : G → R) (a : G) : m ((f ∗ₙ g) a) = (⇑m ∘ f ∗ₙ ⇑m ∘ g) a

theorem comp_cconv {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 : G → R) : ⇑m ∘ (f ∗ₙ g) = ⇑m ∘ f ∗ₙ ⇑m ∘ g

theorem cconv_eq_expect_sub {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 = Finset.univ.expect fun (t : G) => f (a - t) * g t

theorem cconv_eq_expect_add {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 = Finset.univ.expect fun (t : G) => f (a + t) * g (-t)

theorem cconv_eq_expect_sub' {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 = Finset.univ.expect fun (t : G) => f t * g (a - t)

theorem cconv_eq_expect_add' {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 = Finset.univ.expect fun (t : G) => f (-t) * g (a + t)

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

theorem expect_cconv_mul {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g h : G → R) : (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 * g b * h (a + b)

theorem expect_cconv {G : Type u_1} {R : Type u_3} [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) * Finset.univ.expect fun (a : G) => g a

@[simp]

theorem cconv_const {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f : G → R) (b : R) : f ∗ₙ Function.const G b = Function.const G ((Finset.univ.expect fun (x : G) => f x) * b)

@[simp]

theorem const_cconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (b : R) (f : G → R) : Function.const G b ∗ₙ f = Function.const G (b * Finset.univ.expect fun (x : G) => f x)

@[simp]

theorem cconv_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_cconv {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 support_cconv_subset {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] (f g : G → R) : Function.support (f ∗ₙ g) ⊆ Function.support f + Function.support g

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

Difference convolution

Equations

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

def «term_○ₙ_» : Lean.TrailingParserDescr

Equations

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

theorem cdconv_apply {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 = {x : G × G | x.1 - x.2 = a}.expect fun (x : G × G) => f x.1 * (starRingEnd (G → R)) g x.2

theorem cdconv_apply_eq_smul_dconv {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 cdconv_eq_smul_dconv {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 cconv_conjneg {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 ∗ₙ conjneg g = f ○ₙ g

@[simp]

theorem cdconv_conjneg {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 ○ₙ conjneg g = f ∗ₙ g

@[simp]

theorem translate_cdconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (a : G) (f g : G → R) : translate a f ○ₙ g = translate a (f ○ₙ g)

@[simp]

theorem cdconv_translate {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (a : G) (f g : G → R) : f ○ₙ translate a g = translate (-a) (f ○ₙ g)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem cdconv_add {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h : G → R) : f ○ₙ (g + h) = f ○ₙ g + f ○ₙ h

theorem add_cdconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h : G → R) : (f + g) ○ₙ h = f ○ₙ h + g ○ₙ h

theorem smul_cdconv {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ○ₙ g = c • (f ○ₙ g)

theorem cdconv_smul {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] [Star H] [DistribSMul H R] [SMulCommClass H R R] [StarModule H R] (c : H) (f g : G → R) : f ○ₙ c • g = star c • (f ○ₙ g)

theorem smul_cdconv_assoc {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] [DistribSMul H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (f g : G → R) : c • f ○ₙ g = c • (f ○ₙ g)

Alias of smul_cdconv.

theorem smul_cdconv_left_comm {G : Type u_1} {H : Type u_2} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] [Star H] [DistribSMul H R] [SMulCommClass H R R] [StarModule H R] (c : H) (f g : G → R) : f ○ₙ c • g = star c • (f ○ₙ g)

Alias of cdconv_smul.

theorem cconv_cdconv_cconv_comm {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h i : G → R) : f ∗ₙ g ○ₙ (h ∗ₙ i) = f ○ₙ h ∗ₙ (g ○ₙ i)

theorem cdconv_cconv_cdconv_comm {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h i : G → R) : f ○ₙ g ∗ₙ (h ○ₙ i) = f ∗ₙ h ○ₙ (g ∗ₙ i)

theorem cdconv_cdconv_cdconv_comm {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h i : G → R) : f ○ₙ g ○ₙ (h ○ₙ i) = f ○ₙ h ○ₙ (g ○ₙ i)

theorem cdconv_eq_expect_add {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 = Finset.univ.expect fun (t : G) => f (a + t) * (starRingEnd R) (g t)

theorem cdconv_eq_expect_sub {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 = Finset.univ.expect fun (t : G) => f t * (starRingEnd R) (g (t - a))

theorem cdconv_apply_neg {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) = (starRingEnd R) ((g ○ₙ f) a)

theorem cdconv_apply_sub {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 b : G) : (f ○ₙ g) (a - b) = Finset.univ.expect fun (t : G) => f (a + t) * (starRingEnd R) (g (b + t))

theorem expect_cdconv_mul {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g h : G → R) : (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 R) (g b) * h (a - b)

theorem expect_cdconv {G : Type u_1} {R : Type u_3} [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) * Finset.univ.expect fun (a : G) => (starRingEnd R) (g a)

@[simp]

theorem cdconv_const {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f : G → R) (b : R) : f ○ₙ Function.const G b = Function.const G ((Finset.univ.expect fun (x : G) => f x) * (starRingEnd R) b)

@[simp]

theorem const_cdconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (b : R) (f : G → R) : Function.const G b ○ₙ f = Function.const G (b * Finset.univ.expect fun (x : G) => (starRingEnd R) (f x))

@[simp]

theorem cdconv_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_cdconv {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

theorem support_cdconv_subset {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] (f g : G → R) : Function.support (f ○ₙ g) ⊆ Function.support f - Function.support g

@[simp]

theorem cconv_neg {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f g : G → R) : f ∗ₙ -g = -(f ∗ₙ g)

@[simp]

theorem neg_cconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f g : G → R) : -f ∗ₙ g = -(f ∗ₙ g)

theorem cconv_sub {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f g h : G → R) : f ∗ₙ (g - h) = f ∗ₙ g - f ∗ₙ h

theorem sub_cconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] (f g h : G → R) : (f - g) ∗ₙ h = f ∗ₙ h - g ∗ₙ h

@[simp]

theorem cdconv_neg {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] [StarRing R] (f g : G → R) : f ○ₙ -g = -(f ○ₙ g)

@[simp]

theorem neg_cdconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] [StarRing R] (f g : G → R) : -f ○ₙ g = -(f ○ₙ g)

theorem cdconv_sub {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] [StarRing R] (f g h : G → R) : f ○ₙ (g - h) = f ○ₙ g - f ○ₙ h

theorem sub_cdconv {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field R] [CharZero R] [StarRing R] (f g h : G → R) : (f - g) ○ₙ h = f ○ₙ h - g ○ₙ h

@[simp]

theorem indicate_univ_cconv_indicate_univ {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] : 𝟭 Finset.univ ∗ₙ 𝟭 Finset.univ = 𝟭 Finset.univ

@[simp]

theorem indicate_univ_cdconv_mu_univ {G : Type u_1} {R : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield R] [CharZero R] [StarRing R] : 𝟭 Finset.univ ○ₙ 𝟭 Finset.univ = 𝟭 Finset.univ

@[simp]

theorem balance_cconv {G : Type u_1} {R : Type u_3} [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_cdconv {G : Type u_1} {R : Type u_3} [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

@[simp]

theorem RCLike.coe_cconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G) : ↑((f ∗ₙ g) a) = (ofReal ∘ f ∗ₙ ofReal ∘ g) a

@[simp]

theorem RCLike.coe_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G) : ↑((f ○ₙ g) a) = (ofReal ∘ f ○ₙ ofReal ∘ g) a

@[simp]

theorem RCLike.coe_comp_cconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) : ofReal ∘ (f ∗ₙ g) = ofReal ∘ f ∗ₙ ofReal ∘ g

@[simp]

theorem RCLike.coe_comp_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) : ofReal ∘ (f ○ₙ g) = ofReal ∘ f ○ₙ ofReal ∘ g

@[simp]

theorem Complex.coe_cconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) (a : G) : ↑((f ∗ₙ g) a) = (ofReal ∘ f ∗ₙ ofReal ∘ g) a

@[simp]

theorem Complex.coe_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) (a : G) : ↑((f ○ₙ g) a) = (ofReal ∘ f ○ₙ ofReal ∘ g) a

@[simp]

theorem Complex.ofReal_comp_cconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) : ofReal ∘ (f ∗ₙ g) = ofReal ∘ f ∗ₙ ofReal ∘ g

@[simp]

theorem Complex.ofReal_comp_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) : ofReal ∘ (f ○ₙ g) = ofReal ∘ f ○ₙ ofReal ∘ g

@[simp]

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

@[simp]

theorem NNReal.coe_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → NNReal) (a : G) : ↑((f ○ₙ g) a) = (toReal ∘ f ○ₙ toReal ∘ g) a

@[simp]

theorem NNReal.coe_comp_cconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → NNReal) : toReal ∘ (f ∗ₙ g) = toReal ∘ f ∗ₙ toReal ∘ g

@[simp]

theorem NNReal.coe_comp_cdconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → NNReal) : toReal ∘ (f ○ₙ g) = toReal ∘ f ○ₙ toReal ∘ g

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_cconv_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_cdconv_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