OAI/Analysis/Pureness/Comparison/MatrixTraceValues.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.TracialState.cornerTraceValue line 11
2. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_nonneg_re line 14
3. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_monotone line 18
4. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_continuous line 22
5. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_zero line 26
6. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_add line 31
7. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_smul line 38
8. def OAI.CuntzComparison.TracialState.matrixTraceValue line 47
9. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_lowerSemicontinuous line 50
10. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_zero line 53
11. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_add line 56
12. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_smul line 61
13. lemma OAI.CuntzComparison.TracialState.cornerTraceValue_stage_large line 65
14. theorem OAI.CuntzComparison.TracialState.matrixTraceValue_stage line 73