OAI/Analysis/Pureness/Quasitrace/QuasitraceNormBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.twoSize line 11
2. lemma OAI.CuntzPureness.PositiveQuasitrace.twoSize_nonneg line 13
3. lemma OAI.CuntzPureness.PositiveQuasitrace.twoSize_sq line 14
4. lemma OAI.CuntzPureness.PositiveQuasitrace.twoSize_star line 16
5. lemma OAI.CuntzPureness.PositiveQuasitrace.squareValue_mul_le_left line 21
6. lemma OAI.CuntzPureness.PositiveQuasitrace.twoSize_mul_le_left line 32
7. lemma OAI.CuntzPureness.PositiveQuasitrace.twoSize_mul_le_right line 37