OAI/Analysis/KadisonKastler/RealNestDistanceConstruction.lean

The required real-nest distance theorem

Arveson's distance formula is proved here in the precise approximation form used by the application. Finite contractive block completions and weak operator compactness supply a correction with norm at most the nest defect. No nest-distance theorem is assumed.