OAI/Analysis/Commutator/RectangularColumn.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.RectangularColumn.SumHilbert line 25
2. def OAI.Kadison.RectangularColumn.triangularMap line 27
3. lemma OAI.Kadison.RectangularColumn.triangularMap_apply line 36
4. lemma OAI.Kadison.RectangularColumn.derivation_one line 41
5. def OAI.Kadison.RectangularColumn.triangularHom line 50
6. lemma OAI.Kadison.RectangularColumn.triangularHom_apply line 80
7. lemma OAI.Kadison.RectangularColumn.triangularMap_norm_le line 84
8. lemma OAI.Kadison.RectangularColumn.normalized_column_sq line 113
9. theorem OAI.Kadison.RectangularColumn.column_sq line 130
10. theorem OAI.Kadison.RectangularColumn.column_bound line 161