Documentation

TauCeti.RingTheory.MvPowerSeries.Convolution

Convolution of power series with coefficient families #

Let R be a semiring and E an R-module. A formal power series f : MvPowerSeries σ R acts on a coefficient family a : (σ →₀ ℕ) → E by convolution,

(f • a) t = ∑_{p + q = t} f_p • a_q.

This file defines the convolution MvPowerSeries.convSMul and proves its module laws: it is additive in both arguments, constant series act through their constants, and it is compatible with multiplication of series. For E = R it is the coefficient family of the product (MvPowerSeries.convSMul_coeff), and linear maps of coefficient modules commute with it (MvPowerSeries.convSMul_comp). No norm or topology is needed.

Implementation notes #

The reindexing bijection in MvPowerSeries.mul_convSMul is the one Mathlib uses to prove associativity of multiplication, MvPowerSeries.mul_assoc.

source
noncomputable def MvPowerSeries.convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (f : MvPowerSeries σ R) (a : (σ →₀ ℕ) → E) :
(σ →₀ ℕ) → E

The convolution action of a formal power series f on a coefficient family a: the coefficient of f • a at t is ∑_{p + q = t} f_p • a_q. For E = R this is the coefficient family of the product (MvPowerSeries.convSMul_coeff).

Instances For
    source
    theorem MvPowerSeries.convSMul_apply {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [DecidableEq σ] (f : MvPowerSeries σ R) (a : (σ →₀ ℕ) → E) (t : σ →₀ ℕ) :
    f.convSMul a t = ∑ p ∈ Finset.antidiagonal t, (coeff p.1) f • a p.2
    source
    @[simp]
    theorem MvPowerSeries.zero_convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (a : (σ →₀ ℕ) → E) :
    convSMul 0 a = 0
    source
    @[simp]
    theorem MvPowerSeries.convSMul_zero {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (f : MvPowerSeries σ R) :
    f.convSMul 0 = 0
    source
    theorem MvPowerSeries.add_convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (f g : MvPowerSeries σ R) (a : (σ →₀ ℕ) → E) :
    (f + g).convSMul a = f.convSMul a + g.convSMul a
    source
    theorem MvPowerSeries.convSMul_add {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (f : MvPowerSeries σ R) (a b : (σ →₀ ℕ) → E) :
    f.convSMul (a + b) = f.convSMul a + f.convSMul b
    source
    @[simp]
    theorem MvPowerSeries.C_convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (r : R) (a : (σ →₀ ℕ) → E) :
    (C r).convSMul a = r • a

    A constant series acts on coefficient families through its constant.

    source
    @[simp]
    theorem MvPowerSeries.one_convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (a : (σ →₀ ℕ) → E) :
    convSMul 1 a = a
    source
    theorem MvPowerSeries.mul_convSMul {σ : Type u_1} {R : Type u_2} {E : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] (f g : MvPowerSeries σ R) (a : (σ →₀ ℕ) → E) :
    (f * g).convSMul a = f.convSMul (g.convSMul a)

    Convolution is compatible with multiplication of series.

    source
    theorem MvPowerSeries.convSMul_comp {σ : Type u_1} {R : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (φ : E →ₗ[R] F) (f : MvPowerSeries σ R) (a : (σ →₀ ℕ) → E) :
    f.convSMul (⇑φ ∘ a) = ⇑φ ∘ f.convSMul a

    An R-linear map of coefficient modules commutes with convolution.

    source
    theorem MvPowerSeries.convSMul_coeff {σ : Type u_1} {R : Type u_2} [Semiring R] (f g : MvPowerSeries σ R) :
    (f.convSMul fun (t : σ →₀ ℕ) => (coeff t) g) = fun (t : σ →₀ ℕ) => (coeff t) (f * g)

    For coefficients in the ring itself, convolution with the coefficients of g gives the coefficients of the product f * g.