OAI/Analysis/Commutator/CbDilation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CbFactor.HasMatrixBound line 19
2. lemma OAI.Kadison.CbFactor.normalized_contracts line 22
3. abbrev OAI.Kadison.CbFactor.Space line 36
4. def OAI.Kadison.CbFactor.representation line 38
5. def OAI.Kadison.CbFactor.leftOperator line 41
6. def OAI.Kadison.CbFactor.rightOperator line 44
7. lemma OAI.Kadison.CbFactor.factorization line 47
8. lemma OAI.Kadison.CbFactor.leftOperator_norm_le line 56
9. lemma OAI.Kadison.CbFactor.rightOperator_norm_le line 59