BlockCommutantConstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Commutant distance for paired representations

This is the exact two-by-two specialization used by the stability proof. The general represented estimate is transported through the faithful finite Hilbert-sum matrix representation, preserving its constant.

theorem OAI.KadisonKastler.publishedBlockCommutantApproximation line 24
Source documentation
Arveson--Christensen commutant distance for a pair of representations.
```
theorem publishedBlockCommutantApproximation : PublishedBlockCommutantApproximation A K := by
…
```
Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation