OAI/Probability/SignedSweeps/PairTwirlLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.pairColorUnitaryHom line 15
  2. def OAI.SignedSweeps.pairWordUnitaryHom line 38
  3. lemma OAI.SignedSweeps.pairWordUnitaryHom_coe line 43
  4. lemma OAI.SignedSweeps.pair_tensor_conjugate line 48
  5. def OAI.SignedSweeps.pairTensorOrbitHull line 59
  6. lemma OAI.SignedSweeps.word_twirl_mem_closedConvexHull line 74
  7. def OAI.SignedSweeps.pairMatrixCompression line 87
  8. lemma OAI.SignedSweeps.pairMatrixCompression_orbit line 95
  9. lemma OAI.SignedSweeps.kronecker_twirl_mem_compression_hull line 111
  10. theorem OAI.SignedSweeps.exists_pair_twirl_lift line 131
  11. lemma OAI.SignedSweeps.matrix_twirl_entry_eq line 144
  12. lemma OAI.SignedSweeps.matrix_twirl_entry_zero line 158
  13. lemma OAI.SignedSweeps.pair_twirl_compression_eq line 171
  14. lemma OAI.SignedSweeps.pair_twirl_parity_off line 182