OAI/Analysis/Pureness/Cuntz/MatrixStateAWPositive.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.matrixStateAWNontrivial line 16
2. abbrev OAI.CuntzPureness.matrixStateUltralimitPositive line 19
3. abbrev OAI.CuntzPureness.matrixStateUltralimitTriangle line 23
4. abbrev OAI.CuntzPureness.matrixStateUltralimitSqrt line 29
5. abbrev OAI.CuntzPureness.matrixStateAWPositive line 35
6. lemma OAI.CuntzPureness.matrixStateAWPositive_complex line 40
7. abbrev OAI.CuntzPureness.matrixStateAWPositive_triangle line 45
8. abbrev OAI.CuntzPureness.matrixStateAWPositive_sqrt line 49
9. def OAI.CuntzPureness.matrixStateFinOneAW line 53
10. abbrev OAI.CuntzPureness.regularizedStateNormalization line 56
11. lemma OAI.CuntzPureness.regularizedStateNormalization_pos line 61
12. lemma OAI.CuntzPureness.matrixStateFinOneAW_complex line 65
13. lemma OAI.CuntzPureness.matrixStateFinOneAW_positive line 86