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.

Convolution of functions

In this section, we define the convolution f ∗ g and difference convolution f ○ g of functions f g : α → β, and show how they interact.

def conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) : α → β

Convolution

Equations

• (f ∗ g) a = Finset.sum (Finset.filter (fun (x : α × α) => x.1 + x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * g x.2

def dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : α → β

Difference convolution

Equations

• (f ○ g) a = Finset.sum (Finset.filter (fun (x : α × α) => x.1 - x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * (starRingEnd (α → β)) g x.2

def trivChar {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [CommSemiring β] : α → β

The trivial character.

Equations

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

def «term_∗_» : Lean.TrailingParserDescr

Equations

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

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 {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = Finset.sum (Finset.filter (fun (x : α × α) => x.1 + x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * g x.2

theorem dconv_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = Finset.sum (Finset.filter (fun (x : α × α) => x.1 - x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * (starRingEnd (α → β)) g x.2

@[simp]

theorem trivChar_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [CommSemiring β] (a : α) : trivChar a = if a = 0 then 1 else 0

@[simp]

theorem conv_conjneg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : f ∗ conjneg g = f ○ g

@[simp]

theorem dconv_conjneg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : f ○ conjneg g = f ∗ g

@[simp]

theorem translate_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (a : α) (f : α → β) (g : α → β) : τ a f ∗ g = τ a (f ∗ g)

@[simp]

theorem translate_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (a : α) (f : α → β) (g : α → β) : τ a f ○ g = τ a (f ○ g)

@[simp]

theorem conv_translate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (a : α) (f : α → β) (g : α → β) : f ∗ τ a g = τ a (f ∗ g)

@[simp]

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

theorem conv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) : f ∗ g = g ∗ f

@[simp]

theorem conj_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : (starRingEnd (α → β)) (f ∗ g) = (starRingEnd (α → β)) f ∗ (starRingEnd (α → β)) g

@[simp]

theorem conj_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : (starRingEnd (α → β)) (f ○ g) = (starRingEnd (α → β)) f ○ (starRingEnd (α → β)) g

@[simp]

theorem conj_trivChar {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] : (starRingEnd (α → β)) trivChar = trivChar

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

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

@[simp]

theorem isSelfAdjoint_trivChar {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] : IsSelfAdjoint trivChar

@[simp]

theorem conjneg_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f ∗ g) = conjneg f ∗ conjneg g

@[simp]

theorem conjneg_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f ○ g) = g ○ f

@[simp]

theorem conjneg_trivChar {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] : conjneg trivChar = trivChar

@[simp]

theorem conv_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : f ∗ 0 = 0

@[simp]

theorem zero_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : 0 ∗ f = 0

@[simp]

theorem dconv_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) : f ○ 0 = 0

@[simp]

theorem zero_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) : 0 ○ f = 0

theorem conv_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : f ∗ (g + h) = f ∗ g + f ∗ h

theorem add_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : (f + g) ∗ h = f ∗ h + g ∗ h

theorem dconv_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : f ○ (g + h) = f ○ g + f ○ h

theorem add_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (f + g) ○ h = f ○ h + g ○ h

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

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

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

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

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

Alias of smul_conv.

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

Alias of smul_dconv.

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

Alias of conv_smul.

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

Alias of dconv_smul.

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

theorem conv_assoc {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : f ∗ g ∗ h = f ∗ (g ∗ h)

theorem conv_right_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : f ∗ g ∗ h = f ∗ h ∗ g

theorem conv_left_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : f ∗ (g ∗ h) = g ∗ (f ∗ h)

theorem conv_conv_conv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i)

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

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

theorem dconv_dconv_dconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ○ g ○ (h ○ i) = f ○ h ○ (g ○ i)

theorem map_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] {γ : Type u_4} [CommSemiring γ] [StarRing γ] (m : β →+* γ) (f : α → β) (g : α → β) (a : α) : m ((f ∗ g) a) = (⇑m ∘ f ∗ ⇑m ∘ g) a

theorem comp_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] {γ : Type u_4} [CommSemiring γ] [StarRing γ] (m : β →+* γ) (f : α → β) (g : α → β) : ⇑m ∘ (f ∗ g) = ⇑m ∘ f ∗ ⇑m ∘ g

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

theorem conv_eq_sum_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = Finset.sum Finset.univ fun (t : α) => f (a - t) * g t

theorem dconv_eq_sum_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = Finset.sum Finset.univ fun (t : α) => f (a - t) * (starRingEnd β) (g (-t))

theorem conv_eq_sum_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = Finset.sum Finset.univ fun (t : α) => f (a + t) * g (-t)

theorem dconv_eq_sum_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = Finset.sum Finset.univ fun (t : α) => f (a + t) * (starRingEnd β) (g t)

theorem conv_eq_sum_sub' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = Finset.sum Finset.univ fun (t : α) => f t * g (a - t)

theorem dconv_eq_sum_sub' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = Finset.sum Finset.univ fun (t : α) => f t * (starRingEnd β) (g (t - a))

theorem conv_eq_sum_add' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = Finset.sum Finset.univ fun (t : α) => f (-t) * g (a + t)

theorem dconv_eq_sum_add' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = Finset.sum Finset.univ fun (t : α) => f (-t) * (starRingEnd (α → β)) g (-(a + t))

theorem conv_apply_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (a : α) (b : α) : (f ∗ g) (a + b) = Finset.sum Finset.univ fun (t : α) => f (a + t) * g (b - t)

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

theorem dconv_apply_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (a : α) (b : α) : (f ○ g) (a - b) = Finset.sum Finset.univ fun (t : α) => f (a + t) * (starRingEnd β) (g (b + t))

theorem sum_conv_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (h : α → β) : (Finset.sum Finset.univ fun (a : α) => (f ∗ g) a * h a) = Finset.sum Finset.univ fun (a : α) => Finset.sum Finset.univ fun (b : α) => f a * g b * h (a + b)

theorem sum_dconv_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (Finset.sum Finset.univ fun (a : α) => (f ○ g) a * h a) = Finset.sum Finset.univ fun (a : α) => Finset.sum Finset.univ fun (b : α) => f a * (starRingEnd β) (g b) * h (a - b)

theorem sum_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) : (Finset.sum Finset.univ fun (a : α) => (f ∗ g) a) = (Finset.sum Finset.univ fun (a : α) => f a) * Finset.sum Finset.univ fun (a : α) => g a

theorem sum_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : (Finset.sum Finset.univ fun (a : α) => (f ○ g) a) = (Finset.sum Finset.univ fun (a : α) => f a) * Finset.sum Finset.univ fun (a : α) => (starRingEnd β) (g a)

@[simp]

theorem conv_const {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (b : β) : f ∗ Function.const α b = Function.const α ((Finset.sum Finset.univ fun (x : α) => f x) * b)

@[simp]

theorem const_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (b : β) (f : α → β) : Function.const α b ∗ f = Function.const α (b * Finset.sum Finset.univ fun (x : α) => f x)

@[simp]

theorem dconv_const {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (b : β) : f ○ Function.const α b = Function.const α ((Finset.sum Finset.univ fun (x : α) => f x) * (starRingEnd β) b)

@[simp]

theorem const_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (b : β) (f : α → β) : Function.const α b ○ f = Function.const α (b * Finset.sum Finset.univ fun (x : α) => (starRingEnd β) (f x))

@[simp]

theorem conv_trivChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : f ∗ trivChar = f

@[simp]

theorem trivChar_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : trivChar ∗ f = f

@[simp]

theorem dconv_trivChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) : f ○ trivChar = f

@[simp]

theorem trivChar_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) : trivChar ○ f = conjneg f

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

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

theorem indicate_conv_indicate_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (s : Finset α) (t : Finset α) (a : α) : (𝟭 s ∗ 𝟭 t) a = ↑(Finset.filter (fun (x : α × α) => x.1 + x.2 = a) (s ×ˢ t)).card

theorem indicate_dconv_indicate_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (s : Finset α) (t : Finset α) (a : α) : (𝟭 s ○ 𝟭 t) a = ↑(Finset.filter (fun (x : α × α) => x.1 - x.2 = a) (s ×ˢ t)).card

theorem indicate_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (s : Finset α) (f : α → β) : 𝟭 s ∗ f = Finset.sum s fun (a : α) => τ a f

theorem conv_indicate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (s : Finset α) : f ∗ 𝟭 s = Finset.sum s fun (a : α) => τ a f

theorem indicate_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (s : Finset α) (f : α → β) : 𝟭 s ○ f = Finset.sum s fun (a : α) => τ a (conjneg f)

theorem dconv_indicate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (s : Finset α) : f ○ 𝟭 s = Finset.sum s fun (a : α) => τ (-a) f

@[simp]

theorem conv_neg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] (f : α → β) (g : α → β) : f ∗ -g = -(f ∗ g)

@[simp]

theorem neg_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] (f : α → β) (g : α → β) : -f ∗ g = -(f ∗ g)

@[simp]

theorem dconv_neg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] [StarRing β] (f : α → β) (g : α → β) : f ○ -g = -(f ○ g)

@[simp]

theorem neg_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] [StarRing β] (f : α → β) (g : α → β) : -f ○ g = -(f ○ g)

theorem conv_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] (f : α → β) (g : α → β) (h : α → β) : f ∗ (g - h) = f ∗ g - f ∗ h

theorem sub_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] (f : α → β) (g : α → β) (h : α → β) : (f - g) ∗ h = f ∗ h - g ∗ h

theorem dconv_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : f ○ (g - h) = f ○ g - f ○ h

theorem sub_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommRing β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (f - g) ○ h = f ○ h - g ○ h

@[simp]

theorem mu_univ_conv_mu_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] : μ Finset.univ ∗ μ Finset.univ = μ Finset.univ

@[simp]

theorem mu_univ_dconv_mu_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] : μ Finset.univ ○ μ Finset.univ = μ Finset.univ

theorem expect_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ∗ g) a) = (Finset.sum Finset.univ fun (a : α) => f a) * Finset.expect Finset.univ fun (a : α) => g a

theorem expect_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ○ g) a) = (Finset.sum Finset.univ fun (a : α) => f a) * Finset.expect Finset.univ fun (a : α) => (starRingEnd β) (g a)

theorem expect_conv' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ∗ g) a) = (Finset.expect Finset.univ fun (a : α) => f a) * Finset.sum Finset.univ fun (a : α) => g a

theorem expect_dconv' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ○ g) a) = (Finset.expect Finset.univ fun (a : α) => f a) * Finset.sum Finset.univ fun (a : α) => (starRingEnd β) (g a)

theorem mu_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] (s : Finset α) (f : α → β) : μ s ∗ f = (↑s.card)⁻¹ • Finset.sum s fun (a : α) => τ a f

theorem conv_mu {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] (f : α → β) (s : Finset α) : f ∗ μ s = (↑s.card)⁻¹ • Finset.sum s fun (a : α) => τ a f

theorem mu_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] (s : Finset α) (f : α → β) : μ s ○ f = (↑s.card)⁻¹ • Finset.sum s fun (a : α) => τ a (conjneg f)

theorem dconv_mu {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] (f : α → β) (s : Finset α) : f ○ μ s = (↑s.card)⁻¹ • Finset.sum s fun (a : α) => τ (-a) f

@[simp]

theorem balance_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) : Finset.balance (f ∗ g) = Finset.balance f ∗ Finset.balance g

@[simp]

theorem balance_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [StarRing β] [CharZero β] (f : α → β) (g : α → β) : Finset.balance (f ○ g) = Finset.balance f ○ Finset.balance g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Iterated convolution

def iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : ℕ → α → β

Iterated convolution.

Equations

• f ∗^ 0 = trivChar
• f ∗^ Nat.succ n = 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 {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : f ∗^ 0 = trivChar

@[simp]

theorem iterConv_one {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) : f ∗^ 1 = f

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem iterConv_conv_distrib {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (g : α → β) (n : ℕ) : (f ∗ g) ∗^ n = f ∗^ n ∗ g ∗^ n

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

@[simp]

theorem zero_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] {n : ℕ} : n ≠ 0 → 0 ∗^ n = 0

@[simp]

theorem smul_iterConv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [Monoid γ] [DistribMulAction γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (n : ℕ) : (c • f) ∗^ n = c ^ n • f ∗^ n

theorem comp_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] {γ : Type u_4} [CommSemiring γ] [StarRing γ] (m : β →+* γ) (f : α → β) (n : ℕ) : ⇑m ∘ (f ∗^ n) = ⇑m ∘ f ∗^ n

theorem map_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] {γ : Type u_4} [CommSemiring γ] [StarRing γ] (m : β →+* γ) (f : α → β) (a : α) (n : ℕ) : m ((f ∗^ n) a) = (⇑m ∘ f ∗^ n) a

theorem sum_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (n : ℕ) : (Finset.sum Finset.univ fun (a : α) => (f ∗^ n) a) = (Finset.sum Finset.univ fun (a : α) => f a) ^ n

@[simp]

theorem iterConv_trivChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (n : ℕ) : trivChar ∗^ n = trivChar

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

theorem indicate_iterConv_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (s : Finset α) (n : ℕ) (a : α) : (𝟭 s ∗^ n) a = ↑(Finset.filter (fun (x : Fin n → α) => (Finset.sum Finset.univ fun (i : Fin n) => x i) = a) (s^^n)).card

theorem indicate_iterConv_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (s : Finset α) (n : ℕ) (f : α → β) : 𝟭 s ∗^ n ∗ f = Finset.sum (s^^n) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) f

theorem conv_indicate_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f : α → β) (s : Finset α) (n : ℕ) : f ∗ 𝟭 s ∗^ n = Finset.sum (s^^n) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) f

theorem indicate_iterConv_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (s : Finset α) (n : ℕ) (f : α → β) : 𝟭 s ∗^ n ○ f = Finset.sum (s^^n) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) (conjneg f)

theorem dconv_indicate_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] [StarRing β] (f : α → β) (s : Finset α) (n : ℕ) : f ○ 𝟭 s ∗^ n = Finset.sum (s^^n) fun (a : Fin n → α) => τ (-Finset.sum Finset.univ fun (i : Fin n) => a i) f

theorem mu_iterConv_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Module ℚ≥0 β] (s : Finset α) (n : ℕ) (f : α → β) : μ s ∗^ n ∗ f = Finset.expect (Fintype.piFinset fun (x : Fin n) => s) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) f

theorem conv_mu_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Module ℚ≥0 β] (f : α → β) (s : Finset α) (n : ℕ) : f ∗ μ s ∗^ n = Finset.expect (Fintype.piFinset fun (x : Fin n) => s) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) f

theorem mu_iterConv_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Module ℚ≥0 β] [StarRing β] (s : Finset α) (n : ℕ) (f : α → β) : μ s ∗^ n ○ f = Finset.expect (Fintype.piFinset fun (x : Fin n) => s) fun (a : Fin n → α) => τ (Finset.sum Finset.univ fun (i : Fin n) => a i) (conjneg f)

theorem dconv_mu_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Module ℚ≥0 β] [StarRing β] (f : α → β) (s : Finset α) (n : ℕ) : f ○ μ s ∗^ n = Finset.expect (Fintype.piFinset fun (x : Fin n) => s) fun (a : Fin n → α) => τ (-Finset.sum Finset.univ fun (i : Fin n) => a i) f

@[simp]

theorem balance_iterConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) {n : ℕ} : n ≠ 0 → Finset.balance (f ∗^ n) = Finset.balance f ∗^ n

@[simp]

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

@[simp]

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