OAI/Analysis/JiangSu/DimensionDrop/SoftSwap.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.amplified_permutation line 13
  2. lemma OAI.JiangSuConstruction.amplified_permutation_conjugation line 25
  3. def OAI.JiangSuConstruction.softParameter line 31
  4. lemma OAI.JiangSuConstruction.softParameter_continuous line 34
  5. lemma OAI.JiangSuConstruction.softParameter_zero line 39
  6. lemma OAI.JiangSuConstruction.softParameter_one line 46
  7. def OAI.JiangSuConstruction.mergeBlocks line 59
  8. lemma OAI.JiangSuConstruction.mergeBlocks_swap line 62
  9. lemma OAI.JiangSuConstruction.mergeBlocks_dist line 72
  10. lemma OAI.JiangSuConstruction.commute_of_unitaryConjugation_eq line 84
  11. lemma OAI.JiangSuConstruction.mergeBlocks_commute line 91
  12. def OAI.JiangSuConstruction.blockSwapPath line 100
  13. theorem OAI.JiangSuConstruction.blockSwapPath_control line 104
  14. def OAI.JiangSuConstruction.pairBlocks line 117
  15. lemma OAI.JiangSuConstruction.pairBlocks_dist line 120
  16. lemma OAI.JiangSuConstruction.pairBlocks_swap line 131
  17. lemma OAI.JiangSuConstruction.amplifiedUnitary_one line 140
  18. lemma OAI.JiangSuConstruction.unitaryConjugation_one line 144
  19. abbrev OAI.JiangSuConstruction.PairSortPath line 149
  20. def OAI.JiangSuConstruction.pairSortUnitary line 153
  21. lemma OAI.JiangSuConstruction.pairSortUnitary_left line 160
  22. lemma OAI.JiangSuConstruction.pairSortUnitary_right line 166
  23. lemma OAI.JiangSuConstruction.pair_sort_error line 174
  24. lemma OAI.JiangSuConstruction.pairBlocks_self line 207
  25. lemma OAI.JiangSuConstruction.pair_cluster_control line 215
  26. lemma OAI.JiangSuConstruction.exists_pair_sort_path line 225
  27. theorem OAI.JiangSuConstruction.continuous_pair_sort line 237