Unitary dilation and the Crouzeix–Palencia bound

Source: url:https://github.com/savarin/lean-operator-theory Authors: Ezzeri Esa Status: verified Main declarations: PalomarCrouzeixPalencia.crouzeix_palencia Tags: operator-theory, functional-analysis, spectral-theory MSC: 47A12, 47A20, 47A25