1 Setting and prerequisites

Throughout the blueprint, \(\mathbb {K}\) denotes a non-trivially normed field (in practice \(\mathbb {R}\) or \(\mathbb {C}\)), and \(X, Y, Z, W\) are normed spaces over \(\mathbb {K}\); a statement that needs completeness of the field or of a space says so. We write \(\mathcal{L}(X, Y)\) for the space of bounded linear operators \(X \to Y\) with the operator norm, and \(\mathbb {N}_0 = \{ 0, 1, 2, \dots \} \); all sequences are indexed starting from \(0\).

Each statement is accompanied by the name of the Lean declaration that formalises it. Every numbered statement and every proof here is formalised: the project compiles without sorry, so each result is verified by the Lean kernel. The few remarks without a Lean name say so.