Discrete Convolution

Discrete convolution over monoids: (f ⋆[L] g) x is the sum of L (f a) (g b) over all pairs (a, b) with a * b = x, that is, over mulFiber x. Additive monoids are also supported.

Design

Uses a bilinear map L : E →ₗ[S] E' →ₗ[S] F to combine values, following MeasureTheory.convolution.

The index monoid M can be non-commutative (group algebras R[G] with non-abelian G).

@[to_additive] generates multiplicative and additive versions from a single definition. The mul/add distinction refers to the index monoid M: multiplicative sums over mulFiber x = {(a,b) | a * b = x}, additive sums over addFiber x = {(a,b) | a + b = x}.

Main Definitions

• mulFiber x: the fiber of multiplication at x, all pairs (a, b) with a * b = x.
• convolution L f g: the discrete convolution (f ⋆[L] g) x = ∑' ab : mulFiber x, L (f ab.1.1) (g ab.1.2).
• ringConvolution f g: convolution using multiplication to combine the values of f and g.
• ConvolutionExistsAt L f g x: the family indexed by mulFiber x is summable.
• ConvolutionExists L f g: ConvolutionExistsAt L f g x holds for every x.

Main Results

• single_convolution, convolution_single: identity element (Pi.single 1 e where L e is the identity map)
• ConvolutionExists.distrib_add, ConvolutionExists.add_distrib: distributivity over addition
• ConvolutionExistsAt.smul_convolution, ConvolutionExistsAt.convolution_smul: scalar multiplication
• convolution_comm: commutativity for symmetric bilinear maps over commutative monoids
• convolution_eq_sum_mulAntidiagonal: finite-sum formula when the index monoid has Finset.HasMulAntidiagonal
• single_ringConvolution, ringConvolution_single: identity laws for multiplication convolution
• ringConvolution_add, add_ringConvolution: distributivity over addition
• smul_ringConvolution, ringConvolution_smul: external scalar multiplication
• ringConvolution_comm: commutativity when both the indices and values are commutative

Notation

Notation	Operation
f ⋆[L] g	∑' ab : mulFiber x, L (f ab.1.1) (g ab.1.2)
f ⋆₊[L] g	∑' ab : addFiber x, L (f ab.1.1) (g ab.1.2)
f ⋆ᵣ g	ringConvolution f g
f ⋆ᵣ₊ g	addRingConvolution f g

Precedence design: f:68 and g:67 gives right associativity (f ⋆ g ⋆ h parses as f ⋆ (g ⋆ h)), matching function composition ∘ and MeasureTheory.convolution.

Multiplication Fiber

def DiscreteConvolution.mulFiber {M : Type u_1} [Monoid M] (x : M) : Set (M × M)

The fiber of multiplication at x: all pairs (a, b) with a * b = x.

Equations

• DiscreteConvolution.mulFiber x = Set.univ.mulAntidiagonal Set.univ x

def DiscreteConvolution.addFiber {M : Type u_1} [AddMonoid M] (x : M) : Set (M × M)

The fiber of addition at x: all pairs (a, b) with a + b = x.

Equations

• DiscreteConvolution.addFiber x = Set.univ.antidiagonal Set.univ x

theorem DiscreteConvolution.mem_mulFiber {M : Type u_1} [Monoid M] {x : M} {ab : M × M} : ab ∈ mulFiber x ↔ ab.1 * ab.2 = x

theorem DiscreteConvolution.mem_addFiber {M : Type u_1} [AddMonoid M] {x : M} {ab : M × M} : ab ∈ addFiber x ↔ ab.1 + ab.2 = x

theorem DiscreteConvolution.mulFiber_one_mem {M : Type u_1} [Monoid M] : (1, 1) ∈ mulFiber 1

theorem DiscreteConvolution.addFiber_zero_mem {M : Type u_1} [AddMonoid M] : (0, 0) ∈ addFiber 0

Convolution Definition and Existence

noncomputable def DiscreteConvolution.convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : M → F

The discrete convolution of f and g using bilinear map L: the value at x is the sum of L (f a) (g b) over all pairs (a, b) with a * b = x.

Equations

• DiscreteConvolution.convolution L f g x = ∑' (ab : ↑(DiscreteConvolution.mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)

noncomputable def DiscreteConvolution.addConvolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : M → F

Additive convolution: the value at x is the sum of L (f a) (g b) over all pairs (a, b) with a + b = x.

Equations

• DiscreteConvolution.addConvolution L f g x = ∑' (ab : ↑(DiscreteConvolution.addFiber x)), (L (f (↑ab).1)) (g (↑ab).2)

def DiscreteConvolution.«term_⋆[_]_» : Lean.TrailingParserDescr

Notation for discrete convolution with explicit bilinear map: (f ⋆[L] g) x = ∑' ab : mulFiber x, L (f ab.1.1) (g ab.1.2).

Equations

• One or more equations did not get rendered due to their size.

def DiscreteConvolution.«term_⋆₊[_]_» : Lean.TrailingParserDescr

Notation for additive convolution with explicit bilinear map: (f ⋆₊[L] g) x = ∑' ab : addFiber x, L (f ab.1.1) (g ab.1.2).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DiscreteConvolution.zero_convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E') : convolution L 0 f = 0

@[simp]

theorem DiscreteConvolution.zero_addConvolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E') : addConvolution L 0 f = 0

@[simp]

theorem DiscreteConvolution.convolution_zero {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) : convolution L f 0 = 0

@[simp]

theorem DiscreteConvolution.addConvolution_zero {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) : addConvolution L f 0 = 0

@[simp]

theorem DiscreteConvolution.single_convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] [DecidableEq M] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L e) y = y) : convolution L (Pi.single 1 e) f = f

@[simp]

theorem DiscreteConvolution.single_addConvolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] [DecidableEq M] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L e) y = y) : addConvolution L (Pi.single 0 e) f = f

@[simp]

theorem DiscreteConvolution.convolution_single {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] [DecidableEq M] (L : F →ₗ[S] E →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L y) e = y) : convolution L f (Pi.single 1 e) = f

@[simp]

theorem DiscreteConvolution.addConvolution_single {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] [DecidableEq M] (L : F →ₗ[S] E →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L y) e = y) : addConvolution L f (Pi.single 0 e) = f

def DiscreteConvolution.ConvolutionExistsAt {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M) : Prop

The convolution of f and g with bilinear map L exists at x: the family ab ↦ L (f ab.1.1) (g ab.1.2) indexed by mulFiber x is summable.

Equations

• DiscreteConvolution.ConvolutionExistsAt L f g x = Summable fun (ab : ↑(DiscreteConvolution.mulFiber x)) => (L (f (↑ab).1)) (g (↑ab).2)

def DiscreteConvolution.AddConvolutionExistsAt {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M) : Prop

The additive convolution of f and g with bilinear map L exists at x: the family ab ↦ L (f ab.1.1) (g ab.1.2) indexed by addFiber x is summable.

Equations

• DiscreteConvolution.AddConvolutionExistsAt L f g x = Summable fun (ab : ↑(DiscreteConvolution.addFiber x)) => (L (f (↑ab).1)) (g (↑ab).2)

def DiscreteConvolution.ConvolutionExists {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : Prop

The convolution of f and g with bilinear map L exists at every point, that is, ConvolutionExistsAt L f g x holds for every x.

This does not assert that the resulting function convolution L f g is summable over M.

Equations

• DiscreteConvolution.ConvolutionExists L f g = ∀ (x : M), DiscreteConvolution.ConvolutionExistsAt L f g x

def DiscreteConvolution.AddConvolutionExists {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : Prop

The additive convolution of f and g with bilinear map L exists at every point, that is, AddConvolutionExistsAt L f g x holds for every x.

This does not assert that the resulting function addConvolution L f g is summable over M.

Equations

• DiscreteConvolution.AddConvolutionExists L f g = ∀ (x : M), DiscreteConvolution.AddConvolutionExistsAt L f g x

theorem DiscreteConvolution.ConvolutionExistsAt.distrib_add {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f : M → E} {g g' : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExistsAt L f g x) (hfg' : ConvolutionExistsAt L f g' x) : convolution L f (g + g') x = convolution L f g x + convolution L f g' x

theorem DiscreteConvolution.AddConvolutionExistsAt.distrib_add {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f : M → E} {g g' : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExistsAt L f g x) (hfg' : AddConvolutionExistsAt L f g' x) : addConvolution L f (g + g') x = addConvolution L f g x + addConvolution L f g' x

theorem DiscreteConvolution.ConvolutionExists.distrib_add {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f : M → E} {g g' : M → E'} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExists L f g) (hfg' : ConvolutionExists L f g') : convolution L f (g + g') = convolution L f g + convolution L f g'

theorem DiscreteConvolution.AddConvolutionExists.distrib_add {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f : M → E} {g g' : M → E'} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExists L f g) (hfg' : AddConvolutionExists L f g') : addConvolution L f (g + g') = addConvolution L f g + addConvolution L f g'

theorem DiscreteConvolution.ConvolutionExistsAt.add_distrib {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f f' : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExistsAt L f g x) (hfg' : ConvolutionExistsAt L f' g x) : convolution L (f + f') g x = convolution L f g x + convolution L f' g x

theorem DiscreteConvolution.AddConvolutionExistsAt.add_distrib {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f f' : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExistsAt L f g x) (hfg' : AddConvolutionExistsAt L f' g x) : addConvolution L (f + f') g x = addConvolution L f g x + addConvolution L f' g x

theorem DiscreteConvolution.ConvolutionExists.add_distrib {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f f' : M → E} {g : M → E'} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExists L f g) (hfg' : ConvolutionExists L f' g) : convolution L (f + f') g = convolution L f g + convolution L f' g

theorem DiscreteConvolution.AddConvolutionExists.add_distrib {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] [T2Space F] [ContinuousAdd F] {f f' : M → E} {g : M → E'} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExists L f g) (hfg' : AddConvolutionExists L f' g) : addConvolution L (f + f') g = addConvolution L f g + addConvolution L f' g

theorem DiscreteConvolution.ConvolutionExistsAt.smul_convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [Module S E] [Module S E'] {F : Type u_8} [AddCommMonoid F] [Module S F] [TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F] {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExistsAt L f g x) : convolution L (c • f) g x = c • convolution L f g x

theorem DiscreteConvolution.AddConvolutionExistsAt.vadd_convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [Module S E] [Module S E'] {F : Type u_8} [AddCommMonoid F] [Module S F] [TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F] {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExistsAt L f g x) : addConvolution L (c • f) g x = c • addConvolution L f g x

theorem DiscreteConvolution.ConvolutionExistsAt.convolution_smul {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [Module S E] [Module S E'] {F : Type u_8} [AddCommMonoid F] [Module S F] [TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F] {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : ConvolutionExistsAt L f g x) : convolution L f (c • g) x = c • convolution L f g x

theorem DiscreteConvolution.AddConvolutionExistsAt.convolution_vadd {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [Module S E] [Module S E'] {F : Type u_8} [AddCommMonoid F] [Module S F] [TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F] {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F) (hfg : AddConvolutionExistsAt L f g x) : addConvolution L f (c • g) x = c • addConvolution L f g x

Finite Multiplication Fibers

theorem DiscreteConvolution.mulFiber_finite {M : Type u_1} [Monoid M] [Finset.HasMulAntidiagonal M] (x : M) : (mulFiber x).Finite

Multiplication fibers are finite when the index monoid has Finset.HasMulAntidiagonal.

theorem DiscreteConvolution.addFiber_finite {M : Type u_1} [AddMonoid M] [Finset.HasAntidiagonal M] (x : M) : (addFiber x).Finite

Addition fibers are finite when the index monoid has Finset.HasAntidiagonal.

theorem DiscreteConvolution.convolution_eq_sum_mulAntidiagonal {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [Finset.HasMulAntidiagonal M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M) : convolution L f g x = ∑ ab ∈ Finset.mulAntidiagonal x, (L (f ab.1)) (g ab.2)

Convolution is a finite sum when the index monoid has Finset.HasMulAntidiagonal.

theorem DiscreteConvolution.addConvolution_eq_sum_antidiagonal {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [Finset.HasAntidiagonal M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M) : addConvolution L f g x = ∑ ab ∈ Finset.antidiagonal x, (L (f ab.1)) (g ab.2)

Additive convolution is a finite sum when the index monoid has Finset.HasAntidiagonal.

theorem DiscreteConvolution.convolutionExists_of_hasMulAntidiagonal {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [Finset.HasMulAntidiagonal M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : ConvolutionExists L f g

Convolution exists whenever the index monoid has Finset.HasMulAntidiagonal, since every fiber is then finite.

theorem DiscreteConvolution.addConvolutionExists_of_hasAntidiagonal {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [Finset.HasAntidiagonal M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') : AddConvolutionExists L f g

Additive convolution exists whenever the index monoid has Finset.HasAntidiagonal, since every fiber is then finite.

Commutativity

theorem DiscreteConvolution.convolution_comm {M : Type u_1} {S : Type u_2} {E : Type u_3} [CommMonoid M] [CommSemiring S] [AddCommMonoid E] [Module S E] [TopologicalSpace E] (L : E →ₗ[S] E →ₗ[S] E) (f g : M → E) (hL : ∀ (x y : E), (L x) y = (L y) x) : convolution L f g = convolution L g f

theorem DiscreteConvolution.addConvolution_comm {M : Type u_1} {S : Type u_2} {E : Type u_3} [AddCommMonoid M] [CommSemiring S] [AddCommMonoid E] [Module S E] [TopologicalSpace E] (L : E →ₗ[S] E →ₗ[S] E) (f g : M → E) (hL : ∀ (x y : E), (L x) y = (L y) x) : addConvolution L f g = addConvolution L g f

Convolution with Multiplication

noncomputable def DiscreteConvolution.ringConvolution {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [Monoid M] [TopologicalSpace R] (f g : M → R) : M → R

The discrete convolution of two functions using multiplication to combine their values.

Equations

• DiscreteConvolution.ringConvolution f g = DiscreteConvolution.convolution (LinearMap.mul ℕ R) f g

noncomputable def DiscreteConvolution.addRingConvolution {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [AddMonoid M] [TopologicalSpace R] (f g : M → R) : M → R

The additive-index convolution using multiplication to combine values.

Equations

• DiscreteConvolution.addRingConvolution f g = DiscreteConvolution.addConvolution (LinearMap.mul ℕ R) f g

def DiscreteConvolution.«term_⋆ᵣ_» : Lean.TrailingParserDescr

Notation for convolution using multiplication to combine values.

Equations

• One or more equations did not get rendered due to their size.

def DiscreteConvolution.«term_⋆ᵣ₊_» : Lean.TrailingParserDescr

Notation for additive-index convolution using multiplication to combine values.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DiscreteConvolution.ringConvolution_apply {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [Monoid M] [TopologicalSpace R] (f g : M → R) (x : M) : ringConvolution f g x = ∑' (ab : ↑(mulFiber x)), f (↑ab).1 * g (↑ab).2

@[simp]

theorem DiscreteConvolution.addRingConvolution_apply {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [AddMonoid M] [TopologicalSpace R] (f g : M → R) (x : M) : addRingConvolution f g x = ∑' (ab : ↑(addFiber x)), f (↑ab).1 * g (↑ab).2

@[simp]

theorem DiscreteConvolution.zero_ringConvolution {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [Monoid M] [TopologicalSpace R] (f : M → R) : ringConvolution 0 f = 0

@[simp]

theorem DiscreteConvolution.zero_addRingConvolution {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [AddMonoid M] [TopologicalSpace R] (f : M → R) : addRingConvolution 0 f = 0

@[simp]

theorem DiscreteConvolution.ringConvolution_zero {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [Monoid M] [TopologicalSpace R] (f : M → R) : ringConvolution f 0 = 0

@[simp]

theorem DiscreteConvolution.addRingConvolution_zero {M : Type u_1} {R : Type u_7} [NonUnitalNonAssocSemiring R] [AddMonoid M] [TopologicalSpace R] (f : M → R) : addRingConvolution f 0 = 0

@[simp]

theorem DiscreteConvolution.single_ringConvolution {M : Type u_1} {R : Type u_7} [Monoid M] [NonAssocSemiring R] [TopologicalSpace R] [DecidableEq M] (f : M → R) : ringConvolution (Pi.single 1 1) f = f

@[simp]

theorem DiscreteConvolution.single_addRingConvolution {M : Type u_1} {R : Type u_7} [AddMonoid M] [NonAssocSemiring R] [TopologicalSpace R] [DecidableEq M] (f : M → R) : addRingConvolution (Pi.single 0 1) f = f

@[simp]

theorem DiscreteConvolution.ringConvolution_single {M : Type u_1} {R : Type u_7} [Monoid M] [NonAssocSemiring R] [TopologicalSpace R] [DecidableEq M] (f : M → R) : ringConvolution f (Pi.single 1 1) = f

@[simp]

theorem DiscreteConvolution.addRingConvolution_single {M : Type u_1} {R : Type u_7} [AddMonoid M] [NonAssocSemiring R] [TopologicalSpace R] [DecidableEq M] (f : M → R) : addRingConvolution f (Pi.single 0 1) = f

theorem DiscreteConvolution.ringConvolution_add {M : Type u_1} {R : Type u_7} [Monoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [T2Space R] [ContinuousAdd R] (f g h : M → R) (hfg : ConvolutionExists (LinearMap.mul ℕ R) f g) (hfh : ConvolutionExists (LinearMap.mul ℕ R) f h) : ringConvolution f (g + h) = ringConvolution f g + ringConvolution f h

theorem DiscreteConvolution.addRingConvolution_add {M : Type u_1} {R : Type u_7} [AddMonoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [T2Space R] [ContinuousAdd R] (f g h : M → R) (hfg : AddConvolutionExists (LinearMap.mul ℕ R) f g) (hfh : AddConvolutionExists (LinearMap.mul ℕ R) f h) : addRingConvolution f (g + h) = addRingConvolution f g + addRingConvolution f h

theorem DiscreteConvolution.add_ringConvolution {M : Type u_1} {R : Type u_7} [Monoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [T2Space R] [ContinuousAdd R] (f g h : M → R) (hfh : ConvolutionExists (LinearMap.mul ℕ R) f h) (hgh : ConvolutionExists (LinearMap.mul ℕ R) g h) : ringConvolution (f + g) h = ringConvolution f h + ringConvolution g h

theorem DiscreteConvolution.add_addRingConvolution {M : Type u_1} {R : Type u_7} [AddMonoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [T2Space R] [ContinuousAdd R] (f g h : M → R) (hfh : AddConvolutionExists (LinearMap.mul ℕ R) f h) (hgh : AddConvolutionExists (LinearMap.mul ℕ R) g h) : addRingConvolution (f + g) h = addRingConvolution f h + addRingConvolution g h

theorem DiscreteConvolution.smul_ringConvolution {M : Type u_1} {S : Type u_2} {R : Type u_7} [Monoid M] [NonUnitalNonAssocSemiring R] [DistribSMul S R] [TopologicalSpace R] [T2Space R] [ContinuousConstSMul S R] [IsScalarTower S R R] (c : S) (f g : M → R) (hfg : ConvolutionExists (LinearMap.mul ℕ R) f g) : ringConvolution (c • f) g = c • ringConvolution f g

External scalar multiplication in the first factor commutes with convolution.

theorem DiscreteConvolution.smul_addRingConvolution {M : Type u_1} {S : Type u_2} {R : Type u_7} [AddMonoid M] [NonUnitalNonAssocSemiring R] [DistribSMul S R] [TopologicalSpace R] [T2Space R] [ContinuousConstSMul S R] [IsScalarTower S R R] (c : S) (f g : M → R) (hfg : AddConvolutionExists (LinearMap.mul ℕ R) f g) : addRingConvolution (c • f) g = c • addRingConvolution f g

theorem DiscreteConvolution.ringConvolution_smul {M : Type u_1} {S : Type u_2} {R : Type u_7} [Monoid M] [NonUnitalNonAssocSemiring R] [DistribSMul S R] [TopologicalSpace R] [T2Space R] [ContinuousConstSMul S R] [SMulCommClass S R R] (c : S) (f g : M → R) (hfg : ConvolutionExists (LinearMap.mul ℕ R) f g) : ringConvolution f (c • g) = c • ringConvolution f g

External scalar multiplication in the second factor commutes with convolution.

theorem DiscreteConvolution.addRingConvolution_smul {M : Type u_1} {S : Type u_2} {R : Type u_7} [AddMonoid M] [NonUnitalNonAssocSemiring R] [DistribSMul S R] [TopologicalSpace R] [T2Space R] [ContinuousConstSMul S R] [SMulCommClass S R R] (c : S) (f g : M → R) (hfg : AddConvolutionExists (LinearMap.mul ℕ R) f g) : addRingConvolution f (c • g) = c • addRingConvolution f g

theorem DiscreteConvolution.ringConvolution_comm {M : Type u_1} {R : Type u_7} [CommMonoid M] [NonUnitalNonAssocCommSemiring R] [TopologicalSpace R] (f g : M → R) : ringConvolution f g = ringConvolution g f

theorem DiscreteConvolution.addRingConvolution_comm {M : Type u_1} {R : Type u_7} [AddCommMonoid M] [NonUnitalNonAssocCommSemiring R] [TopologicalSpace R] (f g : M → R) : addRingConvolution f g = addRingConvolution g f

theorem DiscreteConvolution.ringConvolution_eq_sum_mulAntidiagonal {M : Type u_1} {R : Type u_7} [Monoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [Finset.HasMulAntidiagonal M] (f g : M → R) (x : M) : ringConvolution f g x = ∑ ab ∈ Finset.mulAntidiagonal x, f ab.1 * g ab.2

Multiplication convolution as a finite sum over the mulAntidiagonal.

theorem DiscreteConvolution.addRingConvolution_eq_sum_antidiagonal {M : Type u_1} {R : Type u_7} [AddMonoid M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [Finset.HasAntidiagonal M] (f g : M → R) (x : M) : addRingConvolution f g x = ∑ ab ∈ Finset.antidiagonal x, f ab.1 * g ab.2

Additive-index multiplication convolution as a finite sum over the antidiagonal.