OAI/Analysis/Commutator/PaulsenDilation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.Paulsen.extension line 26
  2. lemma OAI.Kadison.Paulsen.extension_one line 28
  3. lemma OAI.Kadison.Paulsen.extension_corner line 30
  4. abbrev OAI.Kadison.Paulsen.DilationSpace line 34
  5. def OAI.Kadison.Paulsen.dilationRepresentation line 36
  6. def OAI.Kadison.Paulsen.leftOperator line 39
  7. def OAI.Kadison.Paulsen.rightOperator line 42
  8. lemma OAI.Kadison.Paulsen.representation_upper line 46
  9. theorem OAI.Kadison.Paulsen.dilation_factorization line 54
  10. lemma OAI.Kadison.Paulsen.embedding_norm_le_one line 65
  11. lemma OAI.Kadison.Paulsen.leftOperator_norm_le_one line 71
  12. lemma OAI.Kadison.Paulsen.rightOperator_norm_le_one line 76