Blueprint:
s-Numbers of Bounded Linear Operators
between Banach Spaces

8.3 The inclusion \(\ell _1 \to \ell _\infty \)

This section computes both sides of the maximal difference theorem for the natural inclusion

\[ I \colon \ell _1 \to \ell _\infty , \qquad (x_j)_j \mapsto (x_j)_j , \]

a contraction which is not compact. Everything here is formalised in IdentityL1Linfty.lean, with the two little Grothendieck bounds in LittleGrothendieck.lean and the product estimate, a general Hilbert-space result, in SVD.lean.