OAI/Analysis/Commutator/HilbertBlocks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.HilbertSum.space line 19
2. def OAI.Kadison.HilbertSum.insert line 21
3. def OAI.Kadison.HilbertSum.project line 23
4. lemma OAI.Kadison.HilbertSum.insert_apply line 26
5. lemma OAI.Kadison.HilbertSum.project_apply line 29
6. lemma OAI.Kadison.HilbertSum.inner_insert line 32
7. lemma OAI.Kadison.HilbertSum.adjoint_insert line 35
8. lemma OAI.Kadison.HilbertSum.adjoint_project line 41
9. lemma OAI.Kadison.HilbertSum.norm_insert_apply line 45
10. lemma OAI.Kadison.HilbertSum.norm_project_apply_le line 49
11. lemma OAI.Kadison.HilbertSum.project_insert line 53
12. lemma OAI.Kadison.HilbertSum.project_insert_ne line 59
13. def OAI.Kadison.HilbertSum.block line 64
14. lemma OAI.Kadison.HilbertSum.block_apply line 68
15. lemma OAI.Kadison.HilbertSum.norm_block_le line 71
16. lemma OAI.Kadison.HilbertSum.block_adjoint line 77
17. lemma OAI.Kadison.HilbertSum.reduces_of_offdiagonal line 82
18. lemma OAI.Kadison.HilbertSum.adjoint_reduces_of_offdiagonal line 93
19. lemma OAI.Kadison.HilbertSum.block_covariant line 102
20. lemma OAI.Kadison.HilbertSum.project_covariant_of_adjoint line 111