OAI/Analysis/Commutator/ProjectionBlocks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ProjectionBlocks.space line 21
2. instance OAI.Kadison.ProjectionBlocks.space_complete line 24
3. def OAI.Kadison.ProjectionBlocks.finiteSum line 27
4. lemma OAI.Kadison.ProjectionBlocks.generator_mem line 30
5. lemma OAI.Kadison.ProjectionBlocks.finiteSum_projection line 34
6. lemma OAI.Kadison.ProjectionBlocks.finiteSum_mul line 50
7. lemma OAI.Kadison.ProjectionBlocks.finiteSum_tendsto_space line 58
8. lemma OAI.Kadison.ProjectionBlocks.projection_left line 81
9. lemma OAI.Kadison.ProjectionBlocks.projection_right line 86
10. lemma OAI.Kadison.ProjectionBlocks.finiteSum_tendsto line 92
11. lemma OAI.Kadison.ProjectionBlocks.invariant line 103
12. lemma OAI.Kadison.ProjectionBlocks.projection_commutes line 115
13. lemma OAI.Kadison.ProjectionBlocks.inner_blocks line 124
14. lemma OAI.Kadison.ProjectionBlocks.norm_sum_sq line 131
15. theorem OAI.Kadison.ProjectionBlocks.norm_le_of_blocks line 147