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 #

source

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

Instances For

source

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

source

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

source

@[simp]

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

conjneg trivChar = trivChar

source

@[simp]

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

IsSelfAdjoint trivChar

Convolution #

source

def conv {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 ∈ Finset.filter (fun (x : G × G) => x.1 + x.2 = a) Finset.univ, f x.1 * g x.2

Instances For

source

def «term_∗_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem conv_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 ∈ Finset.filter (fun (x : G × G) => x.1 + x.2 = a) Finset.univ, f x.1 * g x.2

source

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

source

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

source

theorem conv_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

source

theorem add_conv {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

source

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 : G → R) :

c • f ∗ g = c • (f ∗ g)

source

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 : G → R) :

f ∗ c • g = c • (f ∗ g)

source

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 : G → R) :

c • f ∗ g = c • (f ∗ g)

Alias of smul_conv.

source

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 : G → R) :

f ∗ c • g = c • (f ∗ g)

Alias of conv_smul.

source

@[simp]

theorem translate_conv {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)

source

@[simp]

theorem conv_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)

source

theorem conv_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

source

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 d : H) (f g : G → R) :

(c * d) • (f ∗ g) = c • f ∗ d • g

source

theorem conv_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)

source

theorem conv_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

source

theorem conv_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)

source

theorem conv_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

source

theorem conv_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)

source

theorem conv_conv_conv_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)

source

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 : G → R) (a : G) :

m ((f ∗ g) a) = (⇑m ∘ f ∗ ⇑m ∘ g) a

source

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 : G → R) :

⇑m ∘ (f ∗ g) = ⇑m ∘ f ∗ ⇑m ∘ g

source

theorem conv_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

source

theorem conv_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)

source

theorem conv_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)

source

theorem conv_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)

source

theorem conv_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)

source

theorem sum_conv_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)

source

theorem sum_conv {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

source

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

source

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

source

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

source

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

source

theorem support_conv_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 #

source

def dconv {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 ∈ Finset.filter (fun (x : G × G) => x.1 - x.2 = a) Finset.univ, f x.1 * (starRingEnd (G → R)) g x.2

Instances For

source

def «term_○_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem dconv_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 ∈ Finset.filter (fun (x : G × G) => x.1 - x.2 = a) Finset.univ, f x.1 * (starRingEnd (G → R)) g x.2

source

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

source

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

source

theorem dconv_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

source

theorem add_dconv {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

source

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 : G → R) :

c • f ○ g = c • (f ○ g)

source

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 : G → R) :

f ○ c • g = star c • (f ○ g)

source

@[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 : G → R) :

translate a f ○ g = translate a (f ○ g)

source

@[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 : G → R) :

f ○ translate a g = translate (-a) (f ○ g)

source

@[simp]

theorem conv_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

source

@[simp]

theorem dconv_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

source

@[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 : G → R) (a : G) :

(starRingEnd R) ((f ∗ g) a) = ((starRingEnd (G → R)) f ∗ (starRingEnd (G → R)) g) a

source

@[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 : G → R) (a : G) :

(starRingEnd R) ((f ○ g) a) = ((starRingEnd (G → R)) f ○ (starRingEnd (G → R)) g) a

source

@[simp]

theorem conj_conv {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

source

@[simp]

theorem conj_dconv {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

source

theorem IsSelfAdjoint.conv {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)

source

theorem IsSelfAdjoint.dconv {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)

source

@[simp]

theorem conjneg_conv {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

source

@[simp]

theorem conjneg_dconv {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

source

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 : G → R) :

c • f ○ g = c • (f ○ g)

Alias of smul_dconv.

source

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 : G → R) :

f ○ c • g = star c • (f ○ g)

Alias of dconv_smul.

source

theorem dconv_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

source

theorem conv_dconv_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)

source

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 h : G → R) :

f ∗ (g ○ h) = g ∗ (f ○ h)

source

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 h : G → R) :

f ∗ g ○ h = f ○ h ∗ g

source

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 h i : G → R) :

f ∗ g ○ (h ∗ i) = f ○ h ∗ (g ○ i)

source

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 h i : G → R) :

f ○ g ∗ (h ○ i) = f ∗ h ○ (g ∗ i)

source

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 h i : G → R) :

f ○ g ○ (h ○ i) = f ○ h ○ (g ○ i)

source

theorem map_dconv {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

source

theorem comp_dconv {G : Type u_1} [DecidableEq G] [AddCommGroup G] [Fintype G] (f g : G → NNReal) :

NNReal.toReal ∘ (f ○ g) = NNReal.toReal ∘ f ○ NNReal.toReal ∘ g

source

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 : G → R) (a : G) :

(f ○ g) a = ∑ t : G, f (a - t) * (starRingEnd R) (g (-t))

source

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 : G → R) (a : G) :

(f ○ g) a = ∑ t : G, f (a + t) * (starRingEnd R) (g t)

source

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 : G → R) (a : G) :

(f ○ g) a = ∑ t : G, f t * (starRingEnd R) (g (t - a))

source

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 : G → R) (a : G) :

(f ○ g) a = ∑ t : G, f (-t) * (starRingEnd (G → R)) g (-(a + t))

source

theorem dconv_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)

source

theorem dconv_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))

source

theorem sum_dconv_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)

source

theorem sum_dconv {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)

source

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

source

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

source

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

source

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

source

theorem support_dconv_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

source

@[simp]

theorem conv_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)

source

@[simp]

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

-f ∗ g = -(f ∗ g)

source

theorem conv_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

source

theorem sub_conv {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

source

@[simp]

theorem dconv_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)

source

@[simp]

theorem neg_dconv {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)

source

theorem dconv_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

source

theorem sub_dconv {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

source

@[simp]

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

↑((f ∗ g) a) = (RCLike.ofReal ∘ f ∗ RCLike.ofReal ∘ g) a

source

@[simp]

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

↑((f ○ g) a) = (RCLike.ofReal ∘ f ○ RCLike.ofReal ∘ g) a

source

@[simp]

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

RCLike.ofReal ∘ (f ∗ g) = RCLike.ofReal ∘ f ∗ RCLike.ofReal ∘ g

source

@[simp]

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

RCLike.ofReal ∘ (f ○ g) = RCLike.ofReal ∘ f ○ RCLike.ofReal ∘ g

source

@[simp]

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

↑((f ∗ g) a) = (Complex.ofReal ∘ f ∗ Complex.ofReal ∘ g) a

source

@[simp]

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

↑((f ○ g) a) = (Complex.ofReal ∘ f ○ Complex.ofReal ∘ g) a

source

@[simp]

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

Complex.ofReal ∘ (f ∗ g) = Complex.ofReal ∘ f ∗ Complex.ofReal ∘ g

source

@[simp]

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

Complex.ofReal ∘ (f ○ g) = Complex.ofReal ∘ f ○ Complex.ofReal ∘ g

source

@[simp]

theorem NNReal.coe_conv {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

source

@[simp]

theorem NNReal.coe_dconv {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

source

@[simp]

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

NNReal.toReal ∘ (f ∗ g) = NNReal.toReal ∘ f ∗ NNReal.toReal ∘ g

source

@[simp]

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

NNReal.toReal ∘ (f ○ g) = NNReal.toReal ∘ f ○ NNReal.toReal ∘ g

Iterated convolution #

source

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

Instances For

source

def «term_∗^_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

theorem iterConv_zero {G : Type u_1} {R : Type u_3} [DecidableEq G] [AddCommGroup G] [Fintype G] [CommSemiring R] (f : G → R) :

f ∗^ 0 = trivChar

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem iterConv_conv_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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

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

trivChar ∗^ n = trivChar

source

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

source

theorem iterConv_dconv_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

source

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

source

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

source

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)

source

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

source

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

source

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

Documentation

LeanAPAP.Prereqs.Convolution.Discrete.Defs

Convolution #

Main declarations #

Notation #

Notes #

TODO #

Trivial character #

Convolution #

Difference convolution #

Iterated convolution #