Discrete Convolution

Discrete convolution over monoids: (f ⋆[L] g) x = ∑' (a, b) : mulFiber x, L (f a) (g b) where mulFiber x = {(a, b) | a * b = 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) (g ab.2).
• ConvolutionExistsAt L f g x: the convolution sum is summable at x.
• ConvolutionExists L f g: the convolution sum is summable at every point.

Main Results

• convolution_indicator_one_left, convolution_indicator_one_right: identity element (Set.indicator {1} (fun _ => 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

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)

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.

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.

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_6} [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: (f ⋆[L] g) x = ∑' (a, b) : mulFiber x, L (f a) (g b).

noncomputable def DiscreteConvolution.addConvolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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: (f ⋆₊[L] g) x = ∑' ab : 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) (g ab.2).

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

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

@[simp]

theorem DiscreteConvolution.zero_convolution {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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_6} [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_6} [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_6} [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.convolution_indicator_one_left {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L e) y = y) : convolution L ({1}.indicator fun (x : M) => e) f = f

@[simp]

theorem DiscreteConvolution.addConvolution_indicator_zero_left {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F) (hL : ∀ (y : F), (L e) y = y) : addConvolution L ({0}.indicator fun (x : M) => e) f = f

@[simp]

theorem DiscreteConvolution.convolution_indicator_one_right {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [Monoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] (L : F →ₗ[S] E →ₗ[S] F) (f : M → F) (e : E) (hL : ∀ (y : F), (L y) e = y) : convolution L f ({1}.indicator fun (x : M) => e) = f

@[simp]

theorem DiscreteConvolution.addConvolution_indicator_zero_right {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [AddMonoid M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid F] [Module S E] [Module S F] [TopologicalSpace F] (L : F →ₗ[S] E →ₗ[S] F) (f : M → F) (e : E) (hL : ∀ (y : F), (L y) e = y) : addConvolution L f ({0}.indicator fun (x : M) => e) = f

def DiscreteConvolution.ConvolutionExistsAt {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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 when the sum over the fiber is summable.

def DiscreteConvolution.AddConvolutionExistsAt {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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

Additive convolution exists at x when the fiber sum is summable.

def DiscreteConvolution.ConvolutionExists {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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 when it exists at every point.

def DiscreteConvolution.AddConvolutionExists {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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

Additive convolution exists when it exists at every point.

theorem DiscreteConvolution.ConvolutionExistsAt.distrib_add {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_10} [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_10} [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_10} [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_10} [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

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