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.

Trivial character

def trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [CommSemiring R] : G → R

The trivial character.

Equations

• trivChar a = if a = 0 then 1 else 0

@[simp]

theorem trivChar_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [CommSemiring R] (a : G) : trivChar a = if a = 0 then 1 else 0

@[simp]

theorem conj_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] : (starRingEnd (G → R)) trivChar = trivChar

@[simp]

theorem conjneg_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] : conjneg trivChar = trivChar

@[simp]

theorem isSelfAdjoint_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [CommSemiring R] [StarRing R] : IsSelfAdjoint trivChar

Convolution

def conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) : G → R

Convolution

Equations

• (f ∗ g) a = ∑ x ∈ Finset.filter (fun (x : G × G) => x.1 + x.2 = a) Finset.univ, 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 conv_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) : (f ∗ g) a = ∑ x ∈ Finset.filter (fun (x : G × G) => x.1 + x.2 = a) Finset.univ, f x.1 * g x.2

@[simp]

theorem conv_zero {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : f ∗ 0 = 0

@[simp]

theorem zero_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : 0 ∗ f = 0

theorem conv_add {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ (g + h) = f ∗ g + f ∗ h

theorem add_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : (f + g) ∗ h = f ∗ h + g ∗ h

theorem smul_conv {G : Type u_1} {H : Type u_2} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [DistribSMul H R] [IsScalarTower H R R] (c : H) (f : G → R) (g : G → R) : c • f ∗ g = c • (f ∗ g)

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

theorem smul_conv_assoc {G : Type u_1} {H : Type u_2} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [DistribSMul H R] [IsScalarTower H R R] (c : H) (f : G → R) (g : G → R) : c • f ∗ g = c • (f ∗ g)

Alias of smul_conv.

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

Alias of conv_smul.

@[simp]

theorem translate_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (a : G) (f : G → R) (g : G → R) : τ a f ∗ g = τ a (f ∗ g)

@[simp]

theorem conv_translate {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (a : G) (f : G → R) (g : G → R) : f ∗ τ a g = τ a (f ∗ g)

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

theorem mul_smul_conv_comm {G : Type u_1} {H : Type u_2} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] [SMulCommClass H R R] (c : H) (d : H) (f : G → R) (g : G → R) : (c * d) • (f ∗ g) = c • f ∗ d • g

theorem conv_assoc {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ g ∗ h = f ∗ (g ∗ h)

theorem conv_right_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ g ∗ h = f ∗ h ∗ g

theorem conv_left_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ (g ∗ h) = g ∗ (f ∗ h)

theorem conv_rotate {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ g ∗ h = g ∗ h ∗ f

theorem conv_rotate' {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : f ∗ (g ∗ h) = g ∗ (h ∗ f)

theorem conv_conv_conv_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) (i : G → R) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i)

theorem map_conv {G : Type u_1} {R : Type u_3} {S : Type u_4} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [CommSemiring S] (m : R →+* S) (f : G → R) (g : G → R) (a : G) : m ((f ∗ g) a) = (⇑m ∘ f ∗ ⇑m ∘ g) a

theorem comp_conv {G : Type u_1} {R : Type u_3} {S : Type u_4} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [CommSemiring S] (m : R →+* S) (f : G → R) (g : G → R) : ⇑m ∘ (f ∗ g) = ⇑m ∘ f ∗ ⇑m ∘ g

theorem conv_eq_sum_sub {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) : (f ∗ g) a = ∑ t : G, f (a - t) * g t

theorem conv_eq_sum_add {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) : (f ∗ g) a = ∑ t : G, f (a + t) * g (-t)

theorem conv_eq_sum_sub' {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) : (f ∗ g) a = ∑ t : G, f t * g (a - t)

theorem conv_eq_sum_add' {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) : (f ∗ g) a = ∑ t : G, f (-t) * g (a + t)

theorem conv_apply_add {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (a : G) (b : G) : (f ∗ g) (a + b) = ∑ t : G, f (a + t) * g (b - t)

theorem sum_conv_mul {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) (h : G → R) : ∑ a : G, (f ∗ g) a * h a = ∑ a : G, ∑ b : G, f a * g b * h (a + b)

theorem sum_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) : ∑ a : G, (f ∗ g) a = (∑ a : G, f a) * ∑ a : G, g a

@[simp]

theorem conv_const {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (b : R) : f ∗ Function.const G b = Function.const G ((∑ x : G, f x) * b)

@[simp]

theorem const_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (b : R) (f : G → R) : Function.const G b ∗ f = Function.const G (b * ∑ x : G, f x)

@[simp]

theorem conv_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : f ∗ trivChar = f

@[simp]

theorem trivChar_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : trivChar ∗ f = f

theorem support_conv_subset {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (g : G → R) : Function.support (f ∗ g) ⊆ Function.support f + Function.support g

Difference convolution

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

Difference convolution

Equations

• (f ○ g) a = ∑ x ∈ Finset.filter (fun (x : G × G) => x.1 - x.2 = a) Finset.univ, 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 dconv_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) a = ∑ x ∈ Finset.filter (fun (x : G × G) => x.1 - x.2 = a) Finset.univ, f x.1 * (starRingEnd (G → R)) g x.2

@[simp]

theorem dconv_zero {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : f ○ 0 = 0

@[simp]

theorem zero_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : 0 ○ f = 0

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

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

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

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

@[simp]

theorem translate_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (a : G) (f : G → R) (g : G → R) : τ a f ○ g = τ a (f ○ g)

@[simp]

theorem dconv_translate {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (a : G) (f : G → R) (g : G → R) : f ○ τ a g = τ (-a) (f ○ g)

@[simp]

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

@[simp]

theorem dconv_conjneg {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) : f ○ conjneg g = f ∗ g

@[simp]

theorem conj_conv_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (starRingEnd R) ((f ∗ g) a) = ((starRingEnd (G → R)) f ∗ (starRingEnd (G → R)) g) a

@[simp]

theorem conj_dconv_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (starRingEnd R) ((f ○ g) a) = ((starRingEnd (G → R)) f ○ (starRingEnd (G → R)) g) a

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem conjneg_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) : conjneg (f ∗ g) = conjneg f ∗ conjneg g

@[simp]

theorem conjneg_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) : conjneg (f ○ g) = g ○ f

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

Alias of smul_dconv.

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

Alias of dconv_smul.

theorem dconv_right_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (h : G → R) : f ○ g ○ h = f ○ h ○ g

theorem conv_dconv_assoc {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (h : G → R) : f ∗ g ○ h = f ∗ (g ○ h)

theorem conv_dconv_left_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (h : G → R) : f ∗ (g ○ h) = g ∗ (f ○ h)

theorem conv_dconv_right_comm {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (h : G → R) : f ∗ g ○ h = f ○ h ∗ g

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

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

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

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

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

theorem dconv_eq_sum_sub {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) a = ∑ t : G, f (a - t) * (starRingEnd R) (g (-t))

theorem dconv_eq_sum_add {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) a = ∑ t : G, f (a + t) * (starRingEnd R) (g t)

theorem dconv_eq_sum_sub' {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) a = ∑ t : G, f t * (starRingEnd R) (g (t - a))

theorem dconv_eq_sum_add' {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) a = ∑ t : G, f (-t) * (starRingEnd (G → R)) g (-(a + t))

theorem dconv_apply_neg {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) : (f ○ g) (-a) = (starRingEnd R) ((g ○ f) a)

theorem dconv_apply_sub {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (a : G) (b : G) : (f ○ g) (a - b) = ∑ t : G, f (a + t) * (starRingEnd R) (g (b + t))

theorem sum_dconv_mul {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) (h : G → R) : ∑ a : G, (f ○ g) a * h a = ∑ a : G, ∑ b : G, f a * (starRingEnd R) (g b) * h (a - b)

theorem sum_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) : ∑ a : G, (f ○ g) a = (∑ a : G, f a) * ∑ a : G, (starRingEnd R) (g a)

@[simp]

theorem dconv_const {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (b : R) : f ○ Function.const G b = Function.const G ((∑ x : G, f x) * (starRingEnd R) b)

@[simp]

theorem const_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (b : R) (f : G → R) : Function.const G b ○ f = Function.const G (b * ∑ x : G, (starRingEnd R) (f x))

@[simp]

theorem dconv_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : f ○ trivChar = f

@[simp]

theorem trivChar_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : trivChar ○ f = conjneg f

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

@[simp]

theorem conv_neg {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] (f : G → R) (g : G → R) : f ∗ -g = -(f ∗ g)

@[simp]

theorem neg_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] (f : G → R) (g : G → R) : -f ∗ g = -(f ∗ g)

theorem conv_sub {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] (f : G → R) (g : G → R) (h : G → R) : f ∗ (g - h) = f ∗ g - f ∗ h

theorem sub_conv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] (f : G → R) (g : G → R) (h : G → R) : (f - g) ∗ h = f ∗ h - g ∗ h

@[simp]

theorem dconv_neg {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] [StarRing R] (f : G → R) (g : G → R) : f ○ -g = -(f ○ g)

@[simp]

theorem neg_dconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommRing R] [StarRing R] (f : G → R) (g : G → R) : -f ○ g = -(f ○ g)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Iterated convolution

def iterConv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : ℕ → G → R

Iterated convolution.

Equations

• f ∗^ 0 = trivChar
• 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 iterConv_zero {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : f ∗^ 0 = trivChar

@[simp]

theorem iterConv_one {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : f ∗^ 1 = f

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

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

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

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

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

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

@[simp]

theorem zero_iterConv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] {n : ℕ} : n ≠ 0 → 0 ∗^ n = 0

@[simp]

theorem smul_iterConv {G : Type u_1} {H : Type u_2} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring 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_iterConv {G : Type u_1} {R : Type u_3} {S : Type u_4} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [CommSemiring S] (m : R →+* S) (f : G → R) (n : ℕ) : ⇑m ∘ (f ∗^ n) = ⇑m ∘ f ∗^ n

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

theorem sum_iterConv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) (n : ℕ) : ∑ a : G, (f ∗^ n) a = (∑ a : G, f a) ^ n

@[simp]

theorem iterConv_trivChar {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (n : ℕ) : trivChar ∗^ n = trivChar

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

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

@[simp]

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

@[simp]

theorem conj_iterConv_apply {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) (n : ℕ) (a : G) : (starRingEnd R) ((f ∗^ n) a) = ((starRingEnd (G → R)) f ∗^ n) a

theorem IsSelfAdjoint.iterConv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] {f : G → R} [StarRing R] (hf : IsSelfAdjoint f) (n : ℕ) : IsSelfAdjoint (f ∗^ n)

@[simp]

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

@[simp]

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

@[simp]

theorem Complex.ofReal_iterConv {G : Type u_1} [DecidableEq G] [AddCommGroup G] [Fintype G] (f : G → ℝ) (n : ℕ) (a : G) : ↑((f ∗^ n) a) = (Complex.ofReal ∘ f ∗^ n) a