OAI/Analysis/JiangSu/DimensionDrop/SortingNetwork.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JiangSuConstruction.liftNetwork line 13
  2. lemma OAI.JiangSuConstruction.networkCoordinateMap_append line 16
  3. lemma OAI.JiangSuConstruction.compareCoordinates_lift_zero line 25
  4. lemma OAI.JiangSuConstruction.compareCoordinates_lift_succ line 37
  5. lemma OAI.JiangSuConstruction.networkCoordinateMap_lift_zero line 43
  6. lemma OAI.JiangSuConstruction.networkCoordinateMap_lift_succ line 53
  7. lemma OAI.JiangSuConstruction.networkCoordinateMap_lower line 68
  8. def OAI.JiangSuConstruction.sortingNetwork line 84
  9. lemma OAI.JiangSuConstruction.monotone_of_head_tail line 90
  10. lemma OAI.JiangSuConstruction.sortingNetwork_sorts line 98
  11. lemma OAI.JiangSuConstruction.networkCoordinateMap_permutation line 136
  12. lemma OAI.JiangSuConstruction.sortingNetwork_eq_sort line 151
  13. theorem OAI.JiangSuConstruction.continuous_sort_unitary_control line 158
  14. lemma OAI.JiangSuConstruction.interval_sorted_displacement line 174
  15. def OAI.JiangSuConstruction.continuousMatchingUnitary line 197
  16. theorem OAI.JiangSuConstruction.continuous_matching_control line 202
  17. lemma OAI.JiangSuConstruction.continuous_finite_family_modulus line 244
  18. theorem OAI.JiangSuConstruction.exists_continuous_matching_finite line 257