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 #

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

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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)

source

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

source

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)

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

source

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 #

source

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

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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.

source

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.

source

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

source

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)

source

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)

source

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

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

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)

source

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

source

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

source

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)

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

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_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

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_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

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) = (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) = (ofReal ∘ f ∗ᵈ^ n) a

Documentation

APAP.Prereqs.Convolution.Discrete.Defs

Convolution #

Main declarations #

Notation #

Notes #

TODO #

Trivial character #

Convolution #

Difference convolution #

Iterated convolution #