OAI/Analysis/Commutator/GNSVectorEmbedding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.VectorGNS.preMap line 25
2. lemma OAI.Kadison.VectorGNS.inner_preMap line 31
3. def OAI.Kadison.VectorGNS.preIsometry line 38
4. def OAI.Kadison.VectorGNS.embedding line 41
5. lemma OAI.Kadison.VectorGNS.embedding_coe line 54
6. lemma OAI.Kadison.VectorGNS.embedding_vacuum line 62
7. lemma OAI.Kadison.VectorGNS.intertwines line 66
8. lemma OAI.Kadison.VectorGNS.adjoint_intertwines line 79
9. def OAI.Kadison.VectorGNS.compression line 85
10. lemma OAI.Kadison.VectorGNS.compression_commutator line 88
11. lemma OAI.Kadison.VectorGNS.norm_commutator_compression_le line 98
12. lemma OAI.Kadison.VectorGNS.compression_on_preserved line 104