OAI/Analysis/JiangSu/DimensionDrop/ConnectingTraces.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.matrixTrace_mul_comm line 18
  2. lemma OAI.JiangSuConstruction.matrixTrace_unitary line 21
  3. lemma OAI.JiangSuConstruction.matrixTrace_reindex line 27
  4. lemma OAI.JiangSuConstruction.matrixTrace_blockDiagonal line 32
  5. lemma OAI.JiangSuConstruction.normalizedTrace_connecting line 42
  6. lemma OAI.JiangSuConstruction.spectralIndex_card line 59
  7. def OAI.JiangSuConstruction.spectralTransfer line 62
  8. lemma OAI.JiangSuConstruction.normalizedTrace_concreteStep line 68
  9. lemma OAI.JiangSuConstruction.lowerEigenvalue_dist line 83
  10. lemma OAI.JiangSuConstruction.upperEigenvalue_dist line 87
  11. lemma OAI.JiangSuConstruction.spectralTransfer_difference_bound line 93
  12. theorem OAI.JiangSuConstruction.spectralTransfer_affine_modulus line 115
  13. theorem OAI.JiangSuConstruction.continuous_affine_modulus line 145
  14. def OAI.JiangSuConstruction.scalarIterates line 175
  15. lemma OAI.JiangSuConstruction.normalizedTrace_stageStep line 180
  16. lemma OAI.JiangSuConstruction.normalizedTrace_sequence line 186
  17. lemma OAI.JiangSuConstruction.scalarIterates_affine_modulus line 202
  18. lemma OAI.JiangSuConstruction.interval_dist_le_one line 214
  19. theorem OAI.JiangSuConstruction.scalarIterates_oscillation line 219