OAI/Analysis/Commutator/FreeNormalizedColumns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeBlocks.normalizedColumn line 33
2. lemma OAI.Kadison.FreeBlocks.normalizedColumn_apply line 45
3. lemma OAI.Kadison.FreeBlocks.repeatedOutput_orthogonal line 50
4. lemma OAI.Kadison.FreeBlocks.normalizedColumn_orthogonal line 56
5. lemma OAI.Kadison.FreeBlocks.normalizedColumn_error line 72
6. lemma OAI.Kadison.FreeBlocks.normalizedColumn_error_norm line 81
7. lemma OAI.Kadison.FreeBlocks.normalizedColumn_error_orthogonal line 91
8. lemma OAI.Kadison.FreeBlocks.norm_normalizedColumn_error_le line 102