Convolution

This file defines several versions of the discrete convolution of functions.

Main declarations

• ddconv: Discrete convolution of two functions
• dddconv: 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 ddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f g : G → R) : G → R

Convolution

Equations

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

@[simp]

theorem ddconv_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_ddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : 0 ∗ᵈ f = 0

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

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

theorem smul_ddconv {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 : G → R) : c • f ∗ᵈ g = c • (f ∗ᵈ g)

theorem ddconv_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 : G → R) : f ∗ᵈ c • g = c • (f ∗ᵈ g)

theorem smul_ddconv_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 : G → R) : c • f ∗ᵈ g = c • (f ∗ᵈ g)

Alias of smul_ddconv.

theorem smul_ddconv_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 : G → R) : f ∗ᵈ c • g = c • (f ∗ᵈ g)

Alias of ddconv_smul.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem ddconv_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_ddconv {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 ddconv_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_ddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) : trivChar ∗ᵈ f = f

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

Difference convolution

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

Difference convolution

Equations

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

@[simp]

theorem dddconv_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_dddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : 0 ○ᵈ f = 0

@[simp]

theorem dddconv_fun_zero {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : (f ○ᵈ fun (x : G) => 0) = 0

@[simp]

theorem fun_zero_dddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f : G → R) : (fun (x : G) => 0) ○ᵈ f = 0

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

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

theorem smul_dddconv {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 : G → R) : c • f ○ᵈ g = c • (f ○ᵈ g)

theorem dddconv_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 : G → R) : f ○ᵈ c • g = star c • (f ○ᵈ g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem smul_dddconv_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 : G → R) : c • f ○ᵈ g = c • (f ○ᵈ g)

Alias of smul_dddconv.

theorem smul_dddconv_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 : G → R) : f ○ᵈ c • g = star c • (f ○ᵈ g)

Alias of dddconv_smul.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem sum_dddconv_mul {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f g 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_dddconv {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f g : G → R) : ∑ a : G, (f ○ᵈ g) a = (∑ a : G, f a) * ∑ a : G, (starRingEnd R) (g a)

@[simp]

theorem dddconv_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_dddconv {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 dddconv_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_dddconv {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_dddconv_subset {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f g : G → R) : Function.support (f ○ᵈ g) ⊆ Function.support f - Function.support g

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem NNReal.coe_comp_dddconv {G : Type u_1} [DecidableEq G] [AddCommGroup G] [Fintype G] (f g : G → NNReal) : toReal ∘ (f ○ᵈ g) = toReal ∘ f ○ᵈ 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_ddconv_distrib {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f 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_dddconv_distrib {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] [StarRing R] (f 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) = (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) = (ofReal ∘ f ∗ᵈ^ n) a