OAI/Analysis/Commutator/FreeStageHankel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeBlocks.compressed_commutator_eq line 25
2. lemma OAI.Kadison.FreeBlocks.adjoint_commutes_representation line 44
3. lemma OAI.Kadison.FreeBlocks.adjoint_corner_bound line 56
4. lemma OAI.Kadison.FreeBlocks.base_block_intertwines line 84
5. lemma OAI.Kadison.FreeBlocks.base_block_compression line 98
6. theorem OAI.Kadison.FreeBlocks.stage_hankel_bound line 171