OAI/Probability/SignedSweeps/MatrixTwirl.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.MatrixHilbert line 12
  2. def OAI.SignedSweeps.matrixHilbertEquiv line 14
  3. lemma OAI.SignedSweeps.matrixHilbert_inner line 23
  4. lemma OAI.SignedSweeps.matrixHilbert_conj_inner line 31
  5. def OAI.SignedSweeps.matrixConjugationIsometry line 50
  6. lemma OAI.SignedSweeps.matrixConjugationIsometry_apply line 68
  7. def OAI.SignedSweeps.matrixConjugationAction line 73
  8. theorem OAI.SignedSweeps.exists_matrix_twirl line 89
  9. lemma OAI.SignedSweeps.matrix_twirl_mem line 103
  10. lemma OAI.SignedSweeps.isClosed_positive_matrices line 118
  11. lemma OAI.SignedSweeps.convex_positive_matrices line 129
  12. lemma OAI.SignedSweeps.matrix_twirl_positive line 134
  13. lemma OAI.SignedSweeps.matrix_twirl_trace line 144
  14. lemma OAI.SignedSweeps.matrix_twirl_submodule line 171