Cauchy Product (Convolution) of Sequences

The Cauchy product of sequences a, b : ℕ → R is defined as:

(a ⋆ b)ₙ = Σₖ₊ₗ₌ₙ aₖ bₗ

Design Philosophy: Transport from PowerSeries

This file establishes ring axioms for the Cauchy product by transporting them from PowerSeries R, rather than proving them directly via sum manipulations.

The Key Insight

The Cauchy product (a ⋆ b)ₙ is exactly the coefficient of Xⁿ in the product of formal power series (Σ aₖ Xᵏ) · (Σ bₗ Xˡ). This is formalized as:

toPowerSeries (a ⋆ b) = toPowerSeries a * toPowerSeries b

Since Mathlib already proves CommSemiring (PowerSeries R), we get all ring axioms (associativity, distributivity, identity, commutativity) for free.

Why This Matters

Without this approach, proving associativity requires manipulating triple sums:

  ((a ⋆ b) ⋆ c)ₙ = Σᵢ₊ⱼ₌ₙ (Σₖ₊ₗ₌ᵢ aₖ bₗ) cⱼ
                = Σᵢ₊ⱼ₌ₙ Σₖ₊ₗ₌ᵢ aₖ bₗ cⱼ
                = ... (tedious reindexing) ...
                = (a ⋆ (b ⋆ c))ₙ

With this approach, associativity is a one-liner:

theorem assoc (a b c : ℕ → R) : (a ⋆ b) ⋆ c = a ⋆ (b ⋆ c) := by
  -- Transport mul_assoc from PowerSeries
  have h := mul_assoc (toPowerSeries a) (toPowerSeries b) (toPowerSeries c)
  ...

Architectural Role

This file is purely algebraic — it knows nothing about norms or analysis. The separation of concerns is:

┌──────────────────────────────────────────────────────────────────────────┐
│ CauchyProduct.lean (this file)                                           │
│ ════════════════════════════════                                         │
│ Pure algebra: ring axioms for sequences under Cauchy product             │
│ • Depends only on: PowerSeries.Basic, NatAntidiagonal                    │
│ • Provides: assoc, comm, left_distrib, right_distrib, one_mul, mul_one   │
│ • Also: smul_mul, mul_smul (scalar-sequence compatibility)               │
└──────────────────────────────────────────────────────────────────────────┘
                                    ↓
                         Used by (no norm proofs needed)
                                    ↓
┌──────────────────────────────────────────────────────────────────────────┐
│ lpWeighted.lean                                                          │
│ ═══════════════                                                          │
│ Analysis: weighted norms, membership, submultiplicativity                │
│ • Lifts ring axioms to l1Weighted via thin wrappers                      │
│ • Proves analytic properties: mem, norm_mul_le, norm_one                 │
│ • Registers typeclass instances: Ring, CommRing, NormedRing              │
└──────────────────────────────────────────────────────────────────────────┘
                                    ↓
                         Enables (ring tactic works)
                                    ↓
┌──────────────────────────────────────────────────────────────────────────┐
│ FrechetCauchyProduct.lean                                                │
│ ═════════════════════════                                                │
│ Calculus: Fréchet derivatives using CommRing structure                   │
│ • Key identity (a+h)² - a² - 2ah = h² proved via `ring` tactic           │
│ • No sum manipulations needed — algebra is inherited                     │
└──────────────────────────────────────────────────────────────────────────┘

Scalar Compatibility

The instances SMulCommClass and IsScalarTower in lpWeighted.lean rely on:

• smul_mul: (c • a) ⋆ b = c • (a ⋆ b) (works in any Semiring)
• mul_smul: a ⋆ (c • b) = c • (a ⋆ b) (requires CommSemiring)

These enable smul_mul_assoc and smul_comm for the derivative formula in FrechetCauchyProduct.lean.

Main Results

PowerSeries Connection

• toPowerSeries_mul: toPowerSeries (a ⋆ b) = toPowerSeries a * toPowerSeries b

Ring Axioms (Transported)

• assoc: (a ⋆ b) ⋆ c = a ⋆ (b ⋆ c)
• comm: a ⋆ b = b ⋆ a (requires CommSemiring)
• left_distrib, right_distrib: Distributivity
• one_mul, mul_one: Identity element

Scalar Compatibility

• smul_mul: (c • a) ⋆ b = c • (a ⋆ b)
• mul_smul: a ⋆ (c • b) = c • (a ⋆ b) (requires CommSemiring)

Implementation Notes

Why CauchyProduct.apply is not @[simp]

We deliberately do NOT mark apply as @[simp]. Keeping the ⋆ notation abstract prevents issues where:

1. A hypothesis h : (a ⋆ b) n = 0 uses folded notation
2. The goal ∑ kl ∈ antidiagonal n, a kl.1 * b kl.2 = 0 is unfolded
3. The simp tactic fails to match them

Use rw [CauchyProduct.apply] to explicitly unfold when needed.

References

• Definition 7.4.2: Cauchy product definition
• Theorem 7.4.4: Ring axioms for Cauchy product
• Corollary 7.4.5: Commutativity for commutative coefficient rings

def CauchyProduct {R : Type u_1} [Semiring R] (a b : ℕ → R) : ℕ → R

Cauchy product (convolution) of sequences.

(a ⋆ b)ₙ = Σₖ₊ₗ₌ₙ aₖ bₗ

This is Definition 7.4.2, written using the antidiagonal formulation.

Equations

• (a ⋆ b) n = ∑ kl ∈ Finset.antidiagonal n, a kl.1 * b kl.2

def «term_⋆_» : Lean.TrailingParserDescr

Equations

• «term_⋆_» = Lean.ParserDescr.trailingNode `«term_⋆_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 71))

Semiring Section

Results that only require Semiring R. This includes most ring axioms except commutativity and right scalar multiplication.

Basic API

theorem CauchyProduct.apply {R : Type u_1} [Semiring R] (a b : ℕ → R) (n : ℕ) : (a ⋆ b) n = ∑ kl ∈ Finset.antidiagonal n, a kl.1 * b kl.2

The Cauchy product evaluated at index n.

Note: Deliberately NOT marked @[simp] to keep the ⋆ notation abstract. This prevents simp from unfolding in ways that break hypothesis matching. Use rw [CauchyProduct.apply] to explicitly unfold when needed.

theorem CauchyProduct.apply_range {R : Type u_1} [Semiring R] (a b : ℕ → R) (n : ℕ) : (a ⋆ b) n = ∑ j ∈ Finset.range (n + 1), a (n - j) * b j

Alternative form using range, matching Definition 7.4.2 exactly: (a ⋆ b)ₙ = Σⱼ₌₀ⁿ aₙ₋ⱼ bⱼ

Connection to PowerSeries

This is the heart of the "transport from PowerSeries" approach. We show that CauchyProduct is definitionally the same as PowerSeries multiplication, then use this to import all ring axioms.

def CauchyProduct.toPowerSeries {R : Type u_1} (a : ℕ → R) : PowerSeries R

Convert a sequence to a formal power series.

This is the bridge between our sequence-based formulation and Mathlib's PowerSeries which has a verified CommSemiring instance.

Equations

• CauchyProduct.toPowerSeries a = PowerSeries.mk a

@[simp]

theorem CauchyProduct.coeff_toPowerSeries {R : Type u_1} [Semiring R] (a : ℕ → R) (n : ℕ) : (PowerSeries.coeff n) (toPowerSeries a) = a n

theorem CauchyProduct.toPowerSeries_mul {R : Type u_1} [Semiring R] (a b : ℕ → R) : toPowerSeries (a ⋆ b) = toPowerSeries a * toPowerSeries b

Key theorem: Cauchy product equals PowerSeries multiplication.

This is the bridge that lets us transport all ring axioms from CommSemiring (PowerSeries R) without reproving them.

Proof: Both are defined as Σₖ₊ₗ₌ₙ aₖ bₗ.

theorem CauchyProduct.eq_coeff_mul {R : Type u_1} [Semiring R] (a b : ℕ → R) (n : ℕ) : (a ⋆ b) n = (PowerSeries.coeff n) (toPowerSeries a * toPowerSeries b)

Coefficient form of toPowerSeries_mul.

Ring Axioms (Transported from PowerSeries)

Each axiom follows the same pattern:

1. State the property for PowerSeries (which Mathlib proves)
2. Convert both sides using toPowerSeries_mul
3. Extract coefficients to get the sequence equality

This is more maintainable than direct sum manipulation proofs.

theorem CauchyProduct.assoc {R : Type u_1} [Semiring R] (a b c : ℕ → R) : a ⋆ b ⋆ c = a ⋆ (b ⋆ c)

Associativity: (a ⋆ b) ⋆ c = a ⋆ (b ⋆ c)

Transported from mul_assoc on PowerSeries R.

theorem CauchyProduct.left_distrib {R : Type u_1} [Semiring R] (a b c : ℕ → R) : a ⋆ (b + c) = a ⋆ b + a ⋆ c

Left distributivity: a ⋆ (b + c) = a ⋆ b + a ⋆ c

Direct proof via sum distribution (no PowerSeries needed).

theorem CauchyProduct.right_distrib {R : Type u_1} [Semiring R] (a b c : ℕ → R) : (a + b) ⋆ c = a ⋆ c + b ⋆ c

Right distributivity: (a + b) ⋆ c = a ⋆ c + b ⋆ c

Direct proof via sum distribution (no PowerSeries needed).

theorem CauchyProduct.zero_mul {R : Type u_1} [Semiring R] (a : ℕ → R) : 0 ⋆ a = 0

Zero absorbs on the left: 0 ⋆ a = 0

theorem CauchyProduct.mul_zero {R : Type u_1} [Semiring R] (a : ℕ → R) : a ⋆ 0 = 0

Zero absorbs on the right: a ⋆ 0 = 0

Identity Element

The multiplicative identity is the Kronecker delta: e₀ = 1, eₙ = 0 for n ≥ 1.

This corresponds to the power series 1 = 1 + 0·X + 0·X² + .... See Theorem 7.4.6: "the sequence e defined by eₙ := δₙ,₀ is the identity element"

def CauchyProduct.one {R : Type u_1} [Semiring R] : ℕ → R

The multiplicative identity sequence: e₀ = 1, eₙ = 0 for n ≥ 1.

Equations

• CauchyProduct.one n = if n = 0 then 1 else 0

@[simp]

theorem CauchyProduct.one_zero {R : Type u_1} [Semiring R] : one 0 = 1

@[simp]

theorem CauchyProduct.one_succ {R : Type u_1} [Semiring R] (n : ℕ) : one (n + 1) = 0

theorem CauchyProduct.toPowerSeries_one {R : Type u_1} [Semiring R] : toPowerSeries one = 1

theorem CauchyProduct.one_mul {R : Type u_1} [Semiring R] (a : ℕ → R) : one ⋆ a = a

Left identity: one ⋆ a = a

Transported from one_mul on PowerSeries R.

theorem CauchyProduct.mul_one {R : Type u_1} [Semiring R] (a : ℕ → R) : a ⋆ one = a

Right identity: a ⋆ one = a

Transported from mul_one on PowerSeries R.

Scalar Multiplication (Semiring Case)

Scalar multiplication by ring elements pulls out on the left. This is used for IsScalarTower in lpWeighted.lean.

For pulling out on the right, see mul_smul which requires CommSemiring.

theorem CauchyProduct.smul_mul {R : Type u_1} [Semiring R] (c : R) (a b : ℕ → R) : c • a ⋆ b = c • (a ⋆ b)

Scalars pull out on the left: (c • a) ⋆ b = c • (a ⋆ b)

This enables IsScalarTower ℝ (l1Weighted ν) (l1Weighted ν).

Support Lemmas

Lemmas about sequences with finite support, useful for polynomial computations.

theorem CauchyProduct.zero_of_support {R : Type u_1} [Semiring R] {a b : ℕ → R} {M : ℕ} (ha : ∀ (n : ℕ), M < n → a n = 0) (hb : ∀ (n : ℕ), M < n → b n = 0) (n : ℕ) (hn : 2 * M < n) : (a ⋆ b) n = 0

If both sequences vanish beyond M, their Cauchy product vanishes beyond 2M.

theorem CauchyProduct.apply_of_support_le_split {R : Type u_1} [Semiring R] {a h : ℕ → R} {N n : ℕ} (ha : ∀ (k : ℕ), N < k → a k = 0) (hn : N < n) : (a ⋆ h) n = a 0 * h n + ∑ k ∈ Finset.Icc 1 N, a k * h (n - k)

Cauchy product split when first sequence has support in [0, N] and n > N: (a ⋆ h)ₙ = a₀ hₙ + Σₖ₌₁ᴺ aₖ hₙ₋ₖ

Useful for fixed-point iterations where a is a finite polynomial.

CommSemiring Section

Results requiring commutativity of the coefficient ring. This includes commutativity of the Cauchy product and right scalar multiplication.

theorem CauchyProduct.comm {R : Type u_1} [CommSemiring R] (a b : ℕ → R) : a ⋆ b = b ⋆ a

Commutativity: a ⋆ b = b ⋆ a

Transported from mul_comm on PowerSeries R. This is what makes ℓ¹_ν a commutative Banach algebra (Corollary 7.4.5).

theorem CauchyProduct.mul_smul {R : Type u_1} [CommSemiring R] (c : R) (a b : ℕ → R) : a ⋆ c • b = c • (a ⋆ b)

Scalars pull out on the right: a ⋆ (c • b) = c • (a ⋆ b)

Requires commutativity since we need aₖ * (c * bₗ) = c * (aₖ * bₗ). This enables SMulCommClass ℝ (l1Weighted ν) (l1Weighted ν).