OAI/Analysis/Commutator/ReducingCompression.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.ReducingRepresentation.inclusion_intertwines line 25
2. lemma OAI.Kadison.ReducingRepresentation.projection_intertwines line 28
3. def OAI.Kadison.ReducingRepresentation.compression line 33
4. lemma OAI.Kadison.ReducingRepresentation.compression_eq line 36
5. lemma OAI.Kadison.ReducingRepresentation.norm_compression_le line 42
6. lemma OAI.Kadison.ReducingRepresentation.compression_left line 46
7. lemma OAI.Kadison.ReducingRepresentation.compression_right line 51
8. lemma OAI.Kadison.ReducingRepresentation.compression_sub line 57
9. lemma OAI.Kadison.ReducingRepresentation.compression_commutator line 60
10. lemma OAI.Kadison.ReducingRepresentation.norm_commutator_compression_le line 65