FiniteFactorAmplification.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Dimension-free amplification on a separable finite factor

The controlled free lift is constructed from the published ultrapower and independence inputs. All word, row, recovery, and norm estimates are proved.

theorem OAI.KadisonKastler.finiteFactor_unitary_commutator_le line 46
Source documentation
The actual randomization gives the 282δ bound on every matrix unitary.
```
theorem finiteFactor_unitary_commutator_le
    (U : unitary (Algebra (matrixVonNeumann (ι := Fin n) M))) :
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.finiteFactor_matrix_commutator_le line 61
Source documentation
Four-unitary decomposition gives the manuscript's round 600δ bound on every element of a matrix amplification of size at least two.
```
theorem finiteFactor_matrix_commutator_le
    (a : Algebra (matrixVonNeumann (ι := Fin n) M)) :
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann