KirchbergEndgame.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Haagerup's finite cyclic reduction completes Kirchberg's Proposition 1. Each finite matrix test vector generates an invariant subspace on which the representation is similar. The uniform bound on these restrictions therefore bounds every amplification of the original bounded homomorphism.

theorem OAI.KadisonSimilarity.completeBound_of_uniformCommutator line 18
theorem OAI.KadisonSimilarity.similarity_of_uniformCommutator line 67
Source documentation
Uniform commutator control implies similarity for every bounded unital homomorphism, including those not initially known to be completely bounded.
```
theorem similarity_of_uniformCommutator {C : ℝ} (hC : 0 ≤ C)
    (estimate : UniformCommutatorEstimate.{v} C) (π : BoundedUnitalHom A H) :
    SimilarToStar A H π := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar