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 Banach spaces over \(\mathbb {K}\). 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 statement and every proof here is formalised: the project compiles without sorry, so each result is verified by the Lean kernel.