OAI/Analysis/Pureness/Quasitrace/ComplexQuasitraceBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.ComplexQuasitrace.nonneg line 13
2. def OAI.CuntzPureness.ComplexQuasitrace.subalgebraLinear line 17
3. lemma OAI.CuntzPureness.ComplexQuasitrace.subalgebraLinear_apply line 21
4. def OAI.CuntzPureness.ComplexQuasitrace.subalgebraPositiveLinear line 25
5. lemma OAI.CuntzPureness.ComplexQuasitrace.subalgebraPositiveLinear_apply line 37
6. lemma OAI.CuntzPureness.ComplexQuasitrace.map_zero line 42
7. lemma OAI.CuntzPureness.ComplexQuasitrace.norm_apply_le_of_normal line 47
8. theorem OAI.CuntzPureness.ComplexQuasitrace.norm_apply_le line 72