OAI/Analysis/Commutator/ProperlyInfinite.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.commutatorSeminorm_star_le line 22
  2. lemma OAI.Kadison.commutatorSeminorm_star line 34
  3. def OAI.Kadison.operatorColumn line 39
  4. def OAI.Kadison.operatorRow line 44
  5. lemma OAI.Kadison.operatorColumn_apply line 49
  6. lemma OAI.Kadison.operatorRow_apply line 53
  7. lemma OAI.Kadison.operatorRow_adjoint line 57
  8. lemma OAI.Kadison.commutator_column_bound line 65
  9. lemma OAI.Kadison.isometry_range_sum_projection line 92
  10. lemma OAI.Kadison.isometry_star_columnNorm_le line 107
  11. lemma OAI.Kadison.isometry_row_adjoint_comp line 114
  12. lemma OAI.Kadison.isometry_row_norm_le line 136