3.4.1 Alternative: Pietsch’s lifting identity
A second formalization of the Kolmogorov numbers, restricted to the Banach-space setting, lives in KolmogorovLifting.lean. It uses Pietsch’s identity
where \(a_n\) is the approximation number and \(Q_X : \ell ^1(B_X) \twoheadrightarrow X\) is the canonical summation surjection from the \(\ell ^1\) space indexed by the closed unit ball \(B_X\), given by
For every Banach space \(X\) and every \(S \in \mathcal{L}(X, Y)\), \(d_n(S) = a_n(S \circ Q_X)\), and \(d = (d_n)_n\) so defined is a strict s-number sequence: it satisfies (S1)–(S5) and (S5\('\)).
In this variant \(d_n(S)\) is defined as \(a_n(S \circ Q_X)\), so each axiom reduces to the corresponding fact for the approximation numbers (Theorem 3.2). Only the ideal property (S3) needs an extra construction: it factors as \((B \circ S \circ A) \circ Q_W = B \circ (S \circ Q_X) \circ T\) through a lift \(T : \ell ^1(B_W) \to \ell ^1(B_X)\) that sends the basis vector \(\delta _w\) to \(c \cdot \delta _{c^{-1} A w}\) for a scalar \(c\) with \(\| A\| {\lt} |c|\), so that \(\| T\| \le |c|\); letting \(|c| \searrow \| A\| \), using that the norm values of \(\mathbb {K}\) are dense, yields the bound \(\| B\| \, d_n(S) \, \| A\| \). The identification of this \(d_n\) with the canonical Kolmogorov number of Definition 3.7 is Pietsch’s identity (Theorem 3.10).
The lifting development assumes that \(\mathbb {K}\) is a densely normed field (for the rescaling \(|c| \searrow \| A\| \) in the ideal property (S3)) and that the source spaces \(X\), \(W\) are complete (so that \(Q_X(\alpha )\) converges as a series in \(X\)), in addition to completeness of \(\mathbb {K}\) for (S5\('\)). On Banach spaces the two formalisations agree, by Pietsch’s identity (Theorem 3.10).
For every Banach space \(X\) and every \(S \in \mathcal{L}(X, Y)\), the canonical Kolmogorov number equals the approximation number of the lift: \(d_n(S) = a_n(S \circ Q_X)\).
The inequality \(d_n(S) \le a_n(S \circ Q_X)\): for a rank-\(\le n\) approximant \(L\) of \(S \circ Q_X\), take \(V := \operatorname {range} L\); since every unit vector \(x\) is \(Q_X(\delta _x)\) and \(\pi _V \circ L = 0\), one gets \(\| \pi _V \circ S\| \le \| S \circ Q_X - L\| \). The reverse inequality: for an admissible \(V\) and \(\varepsilon {\gt} 0\), pick \(w_x \in V\) with \(\| S x - w_x\| {\lt} \| \pi _V \circ S\| + \varepsilon \) and lift to \(L(\alpha ) := \sum _x \alpha (x)\, w_x\) (a rank-\(\le n\) operator into the finite-dimensional \(V\)), so that \(\| S \circ Q_X - L\| \le \| \pi _V \circ S\| + \varepsilon \).