OAI/Analysis/JiangSu/DimensionDrop/ContinuousBlockSort.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.blockDiagonal_dist line 13
  2. lemma OAI.JiangSuConstruction.block_swap_distance line 21
  3. def OAI.JiangSuConstruction.blockSortUnitary line 33
  4. lemma OAI.JiangSuConstruction.blockSortUnitary_left line 41
  5. lemma OAI.JiangSuConstruction.blockSortUnitary_right line 48
  6. theorem OAI.JiangSuConstruction.continuous_block_sort line 56
  7. def OAI.JiangSuConstruction.compareCoordinates line 97
  8. lemma OAI.JiangSuConstruction.compareCoordinates_eq line 100
  9. def OAI.JiangSuConstruction.compareCoordinateMap line 120
  10. lemma OAI.JiangSuConstruction.compareCoordinateMap_control line 128
  11. def OAI.JiangSuConstruction.networkCoordinateMap line 138
  12. def OAI.JiangSuConstruction.networkUnitary line 143
  13. lemma OAI.JiangSuConstruction.unitaryConjugation_mul line 149
  14. theorem OAI.JiangSuConstruction.networkUnitary_control line 155