Halmos one-step unitary dilation

Every contraction T on a complex Hilbert space is the compression of a unitary operator on the Hilbert direct sum of two copies of the space. The construction below packages the Halmos two-by-two argument through continuous functional calculus: the off-diagonal self-adjoint contraction (x, y) ↦ (T y, T† x) gives a unitary after adjoining its defect square root.

theorem exists_halmos_unitary_dilation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) : ∃ U ∈ unitary (WithLp 2 (E × E) →L[ℂ] WithLp 2 (E × E)), ∀ (x : E), (U (WithLp.toLp 2 (x, 0))).fst = T x

Every contraction has a unitary extension on the Hilbert direct sum of two copies of its space, whose compression to the first summand is the original operator.