OAI/Analysis/Commutator/ProperlyInfiniteBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.isometry_column_error_eq line 22
2. lemma OAI.Kadison.isometry_column_error_bound line 35
3. lemma OAI.Kadison.isometry_row_error_bound line 43
4. lemma OAI.Kadison.row_matrix_row_adjoint line 54
5. lemma OAI.Kadison.row_matrix_row_adjoint_mem line 65
6. lemma OAI.Kadison.isometry_commutator_identity line 74
7. lemma OAI.Kadison.norm_comp_contractions line 87
8. lemma OAI.Kadison.norm_contractive_sandwich line 93
9. lemma OAI.Kadison.isometry_commutator_norm_bound line 104
10. theorem OAI.Kadison.uniform_commutator_of_isometries line 131