OAI/Analysis/JiangSu/DimensionDrop/DimensionDropSquareDensity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.dropFiber_zero line 16
  2. lemma OAI.JiangSuConstruction.dropFiber_one line 18
  3. def OAI.JiangSuConstruction.cutoffFiber line 25
  4. lemma OAI.JiangSuConstruction.tensor_cutoff_apply line 51
  5. lemma OAI.JiangSuConstruction.convex_sum_error line 67
  6. theorem OAI.JiangSuConstruction.squareTensorMap_dense line 88
  7. lemma OAI.JiangSuConstruction.leftAmplification_eq line 144
  8. lemma OAI.JiangSuConstruction.rightAmplification_eq line 145
  9. def OAI.JiangSuConstruction.rightUnitary line 147
  10. lemma OAI.JiangSuConstruction.rightUnitary_continuous line 149
  11. lemma OAI.JiangSuConstruction.rightUnitary_one line 151
  12. def OAI.JiangSuConstruction.surgerySection line 161
  13. lemma OAI.JiangSuConstruction.surgerySection_left_zero line 177
  14. lemma OAI.JiangSuConstruction.surgerySection_left_one line 183
  15. lemma OAI.JiangSuConstruction.surgerySection_right_zero line 190
  16. lemma OAI.JiangSuConstruction.surgerySection_right_one line 197
  17. lemma OAI.JiangSuConstruction.q_right_mem line 204
  18. lemma OAI.JiangSuConstruction.p_right_mem line 209
  19. lemma OAI.JiangSuConstruction.surgerySection_mem line 217
  20. def OAI.JiangSuConstruction.squareUnitary line 281
  21. def OAI.JiangSuConstruction.surgeryUnitary line 295