OAI/Analysis/Commutator/FreeCompressionNorm.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeCorner.three_block_bound line 19
2. lemma OAI.Kadison.FreeCreation.gns_injective line 72
3. lemma OAI.Kadison.FreeCreation.norm_gns line 81
4. lemma OAI.Kadison.FreeCreation.norm_preGNS_projection line 84
5. lemma OAI.Kadison.FreeCreation.norm_preGNS_projection_sq line 90
6. lemma OAI.Kadison.FreeCreation.one_sub_headProjection line 99
7. lemma OAI.Kadison.FreeCreation.norm_left_headProjection line 107
8. lemma OAI.Kadison.FreeCreation.norm_right_headProjection line 119
9. lemma OAI.Kadison.FreeCreation.norm_creation line 131
10. lemma OAI.Kadison.FreeCreation.norm_annihilation line 142
11. lemma OAI.Kadison.FreeCreation.creation_zero_block line 153
12. theorem OAI.Kadison.FreeCreation.free_compression_norm line 165
13. def OAI.Kadison.FreeMoments.liftLetter line 198
14. lemma OAI.Kadison.FreeMoments.liftLetter_color line 201
15. lemma OAI.Kadison.FreeMoments.liftLetter_val line 203
16. lemma OAI.Kadison.FreeMoments.word_liftLetter line 205
17. lemma OAI.Kadison.FreeMoments.Free.comap line 211
18. def OAI.Kadison.FreeWordTensor.restrictedState line 231
19. theorem OAI.Kadison.FreeCreation.free_compression_norm_intrinsic line 260