2.1 Weighted \(\ell ^1_\nu \) Banach Algebra (Section 7.4)

This section establishes the weighted \(\ell ^1_\nu \) space as a commutative Banach algebra under the Cauchy product. The algebraic structure is derived by connecting to PowerSeries multiplication, then the analytic properties (submultiplicativity) are proven using weight factorization.

2.1.1 Positive Reals and Scaled Spaces

Definition 2.1.1 Positive real numbers

✓

The type of positive real numbers: \(\texttt{PosReal} := \{ x : \mathbb {R} \mid 0 {\lt} x\} \).

Definition 2.1.2 Scaled real type

✓

For \(\nu {\gt} 0\) and \(n \in \mathbb {N}\), the type \(\texttt{ScaledReal}\ \nu \ n\) is \(\mathbb {R}\) equipped with the scaled norm \(\| x\| _n := |x| \cdot \nu ^n\).

2.1.2 Weighted \(\ell ^p\) Spaces

Definition 2.1.3 Weighted \(\ell ^p\) space

✓

The weighted \(\ell ^p_\nu \) space is realized as \(\texttt{lp}\ (\texttt{ScaledReal}\ \nu )\ p\). The norm is:

\begin{equation*} \| a\| _{p,\nu } := \left(\sum _{n=0}^\infty |a_n|^p \nu ^{pn}\right)^{1/p}. \end{equation*}

Definition 2.1.4 Weighted \(\ell ^1\) space

✓

Specialization of \(\ell ^p_\nu \) to \(p = 1\):

\begin{equation*} \ell ^1_\nu = \left\{ a : \mathbb {N} \rightarrow \mathbb {R} \; \middle |\; \| a\| _{1,\nu } := \sum _{n=0}^\infty |a_n| \nu ^n {\lt} \infty \right\} . \end{equation*}

Lemma 2.1.5 Completeness

✓

The space \(\ell ^p_\nu \) is complete (a Banach space) for \(p \geq 1\).

Lemma 2.1.6 Membership criterion

✓

A sequence \(a\) belongs to \(\ell ^1_\nu \) iff \(\sum _{n=0}^\infty |a_n| \nu ^n\) converges.

Lemma 2.1.7 Weight factorization

✓

For \(k + l = n\): \(\nu ^k \cdot \nu ^l = \nu ^n\). This is the key property enabling submultiplicativity.

2.1.3 Cauchy Product (Definition 7.4.2)

The Cauchy product (convolution) defines multiplication on sequence spaces.

Definition 2.1.8 Cauchy product

✓

The Cauchy product of sequences \(a, b : \mathbb {N} \rightarrow R\) is:

\begin{equation*} (a \star b)_n = \sum _{k+l=n} a_k b_l = \sum _{j=0}^{n} a_{n-j} b_j. \end{equation*}

Theorem 2.1.9 Connection to PowerSeries

✓

Let \(\texttt{toPowerSeries}(a) = \sum _n a_n X^n\). Then:

\begin{equation*} \texttt{toPowerSeries}(a \star b) = \texttt{toPowerSeries}(a) \cdot \texttt{toPowerSeries}(b). \end{equation*}

This bridge lets us transport all ring axioms from PowerSeries R.

Theorem 2.1.10 Associativity

✓

\((a \star b) \star c = a \star (b \star c)\).

Theorem 2.1.11 Commutativity

✓

\(a \star b = b \star a\) (when \(R\) is commutative).

Theorem 2.1.12 Left distributivity

✓

\(a \star (b + c) = a \star b + a \star c\).

Theorem 2.1.13 Right distributivity

✓

\((a + b) \star c = a \star c + b \star c\).

Definition 2.1.14 Identity sequence

✓

The identity element is the Kronecker delta:

\begin{equation*} e_n = \delta _{n,0} = \begin{cases} 1 & n = 0 \\ 0 & n \geq 1. \end{cases}\end{equation*}

Theorem 2.1.15 Left identity

✓

\(e \star a = a\).

Theorem 2.1.16 Right identity

✓

\(a \star e = a\).

2.1.4 Scalar-Sequence Compatibility

These lemmas establish compatibility between scalar multiplication and the Cauchy product. They are essential for the Fréchet derivative formula in Section 2.3.

Theorem 2.1.17 Left scalar multiplication

✓

Scalars pull out on the left: \((c \cdot a) \star b = c \cdot (a \star b)\).

Theorem 2.1.18 Right scalar multiplication

✓

Scalars pull out on the right: \(a \star (c \cdot b) = c \cdot (a \star b)\). Requires commutativity of the coefficient ring.

2.1.5 Banach Algebra Structure (Theorem 7.4.4)

Lemma 2.1.19 Closure under multiplication

✓

If \(a, b \in \ell ^1_\nu \), then \(a \star b \in \ell ^1_\nu \).

Proof ▶

By Mertens’ theorem and weight factorization:

\begin{align*} \sum _{n=0}^\infty |(a \star b)_n| \nu ^n & \leq \sum _{n=0}^\infty \sum _{k=0}^n |a_k| |b_{n-k}| \nu ^n \\ & = \sum _{n=0}^\infty \sum _{k=0}^n |a_k| \nu ^k \cdot |b_{n-k}| \nu ^{n-k} \\ & = \| a\| _{\ell ^1_\nu } \cdot \| b\| _{\ell ^1_\nu } {\lt} \infty . \end{align*}

Definition 2.1.20 Multiplication on \(\ell ^1_\nu \)

✓

\(\texttt{mul}(a, b) := a \star b\) lifted to \(\ell ^1_\nu \).

Theorem 2.1.21 Submultiplicativity

✓

\(\| a \star b\| _{1,\nu } \leq \| a\| _{1,\nu } \cdot \| b\| _{1,\nu }\).

This is axiom (4) of Definition 7.4.1, the key analytic property. The proof uses Mertens’ theorem and weight factorization \(\nu ^n = \nu ^k \cdot \nu ^l\).

Definition 2.1.22 Identity element

✓

The identity \(e \in \ell ^1_\nu \) with \(e_0 = 1\), \(e_n = 0\) for \(n \geq 1\).

Lemma 2.1.23 Norm of identity

✓

\(\| e\| _{1,\nu } = 1\).

2.1.6 Typeclass Instances (Corollary 7.4.5)

Theorem 2.1.24 Ring instance

✓

\(\ell ^1_\nu \) is a ring under Cauchy product multiplication.

Theorem 2.1.25 Commutative ring instance

✓

\(\ell ^1_\nu \) is a commutative ring.

Theorem 2.1.26 Normed ring instance

✓

\(\ell ^1_\nu \) is a normed ring (submultiplicativity holds).

Theorem 2.1.27 Norm one class

✓

\(\| 1\| = 1\) in \(\ell ^1_\nu \).

2.1.7 Algebra Structure

These instances establish that \(\ell ^1_\nu \) is an \(\mathbb {R}\)-algebra, meaning scalar multiplication is compatible with ring multiplication. This is essential for the Fréchet derivative formula \(D[\mathrm{sq}](a) h = 2(a \star h)\), where the scalar \(2\) must commute with the multiplication.

Theorem 2.1.28 Scalar commutes with multiplication

✓

For \(c \in \mathbb {R}\) and \(a, b \in \ell ^1_\nu \):

\begin{equation*} c \cdot (a \star b) = a \star (c \cdot b). \end{equation*}

This is the SMulCommClass instance.

Theorem 2.1.29 Scalar tower property

✓

For \(c \in \mathbb {R}\) and \(a, b \in \ell ^1_\nu \):

\begin{equation*} (c \cdot a) \star b = c \cdot (a \star b). \end{equation*}

This is the IsScalarTower instance.

Theorem 2.1.30 \(\mathbb {R}\)-Algebra instance

✓

\(\ell ^1_\nu \) is an \(\mathbb {R}\)-algebra. The algebra map \(\mathbb {R} \rightarrow \ell ^1_\nu \) sends \(r\) to \(r \cdot e\) where \(e\) is the identity sequence.

Lemma 2.1.31 Norm of scalar multiplication

For \(c \in \mathbb {R}\) and \(a \in \ell ^1_\nu \):

\begin{equation*} \| c \cdot a\| _{1,\nu } = |c| \cdot \| a\| _{1,\nu }. \end{equation*}

Proof ▶

Direct computation: \(\| c \cdot a\| = \sum _n |c \cdot a_n| \nu ^n = |c| \sum _n |a_n| \nu ^n = |c| \cdot \| a\| \).

Theorem 2.1.32 Normed \(\mathbb {R}\)-Algebra instance

✓

\(\ell ^1_\nu \) is a normed \(\mathbb {R}\)-algebra, satisfying \(\| c \cdot a\| \leq |c| \cdot \| a\| \). (In fact, equality holds.)

Lemma 2.1.33 Norm bound for powers

✓

For \(a \in \ell ^1_\nu \) and \(n \in \mathbb {N}\):

\begin{equation*} \| a^n\| _{1,\nu } \leq \| a\| _{1,\nu }^n. \end{equation*}

Proof ▶

By induction on \(n\). The base case \(n = 0\) gives \(\| 1\| = 1 = \| a\| ^0\). For the inductive step, submultiplicativity gives \(\| a^{n+1}\| = \| a \cdot a^n\| \leq \| a\| \cdot \| a^n\| \leq \| a\| \cdot \| a\| ^n = \| a\| ^{n+1}\).

Corollary 2.1.34 Commutative Banach algebra

✓

\(\ell ^1_\nu \) is a commutative Banach algebra over \(\mathbb {R}\):

Complete normed space (Banach)
Commutative ring under \(\star \)
\(\mathbb {R}\)-algebra with compatible scalar multiplication
Submultiplicative: \(\| a \star b\| \leq \| a\| \cdot \| b\| \)
Scalar-norm compatibility: \(\| c \cdot a\| = |c| \cdot \| a\| \)
\(\| 1\| = 1\)

This is the full Mathlib NormedAlgebra + CompleteSpace structure.

2.1.8 Architecture Summary

The formalization separates concerns into layers:

File	Contents	Dependencies
CauchyProduct.lean	Ring axioms, scalar compat	PowerSeries.Basic
lpWeighted.lean	Banach structure, instances	CauchyProduct, lpSpace
FrechetCauchyProduct.lean	Fréchet derivatives	Ring instances

Key insight: Ring axioms are transported from PowerSeries via toPowerSeries_mul, avoiding manual verification of associativity/distributivity. The SMulCommClass and IsScalarTower instances similarly lift scalar compatibility from CauchyProduct.