OAI/Analysis/JiangSu/DimensionDrop/PointwiseMatching.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.JiangSuConstruction.interval_matching_of_cumulative line 18
  2. theorem OAI.JiangSuConstruction.pointwise_unitary_matching line 27
  3. theorem OAI.JiangSuConstruction.finite_matrix_tensor_flip line 49
  4. lemma OAI.JiangSuConstruction.conjugation_near_commuting line 64
  5. lemma OAI.JiangSuConstruction.amplification_commute line 81
  6. lemma OAI.JiangSuConstruction.blockDiagonal_constant line 90
  7. def OAI.JiangSuConstruction.amplifiedUnitary line 99
  8. lemma OAI.JiangSuConstruction.amplifiedUnitary_continuous line 102
  9. theorem OAI.JiangSuConstruction.cluster_path_control line 105
  10. lemma OAI.JiangSuConstruction.unitary_star_commute line 131
  11. lemma OAI.JiangSuConstruction.unitary_argument_commute line 142
  12. def OAI.JiangSuConstruction.finiteSpectrumLogPath line 148
  13. lemma OAI.JiangSuConstruction.finiteSpectrumLogPath_commute line 155
  14. theorem OAI.JiangSuConstruction.finiteSpectrumLogPath_control line 163