OAI/Analysis/Commutator/HilbertPadding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.HilbertPadding.extend line 23
  2. lemma OAI.Kadison.HilbertPadding.norm_extend_le line 26
  3. lemma OAI.Kadison.HilbertPadding.compress_extend line 37
  4. lemma OAI.Kadison.HilbertPadding.norm_extend line 43
  5. lemma OAI.Kadison.HilbertPadding.extend_commutator line 47
  6. lemma OAI.Kadison.HilbertPadding.norm_extend_commutator line 55
  7. def OAI.Kadison.HilbertPadding.leftCopies line 65
  8. lemma OAI.Kadison.HilbertPadding.leftCopies_inl line 74
  9. lemma OAI.Kadison.HilbertPadding.leftCopies_inr line 78
  10. lemma OAI.Kadison.HilbertPadding.leftCopies_diagonal line 85
  11. lemma OAI.Kadison.HilbertPadding.adjoint_leftCopies_diagonal line 91
  12. theorem OAI.Kadison.HilbertPadding.copy_padding_commutator_norm line 97