OAI/Analysis/Commutator/TwoByTwoPositive.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CStarBlock.block line 20
2. lemma OAI.Kadison.CStarBlock.block00 line 23
3. lemma OAI.Kadison.CStarBlock.block01 line 25
4. lemma OAI.Kadison.CStarBlock.block10 line 27
5. lemma OAI.Kadison.CStarBlock.block11 line 29
6. lemma OAI.Kadison.CStarBlock.block_mul line 33
7. lemma OAI.Kadison.CStarBlock.star_block line 38
8. lemma OAI.Kadison.CStarBlock.diagonal_nonneg line 44
9. lemma OAI.Kadison.CStarBlock.contraction_block_nonneg line 56
10. lemma OAI.Kadison.CStarBlock.contraction_of_block_nonneg line 67