OAI/Analysis/JiangSu/DimensionDrop/SpectralFamilies.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.JiangSuConstruction.SpectralIndex line 12
  2. def OAI.JiangSuConstruction.spectralFamily line 13
  3. def OAI.JiangSuConstruction.sumShuffle line 18
  4. def OAI.JiangSuConstruction.sumShuffleRight line 24
  5. def OAI.JiangSuConstruction.zeroCountEquiv line 27
  6. def OAI.JiangSuConstruction.upperCountEquiv line 30
  7. def OAI.JiangSuConstruction.oneCountEquiv line 33
  8. def OAI.JiangSuConstruction.lowerCountEquiv line 36
  9. def OAI.JiangSuConstruction.zeroBlockEquiv line 40
  10. def OAI.JiangSuConstruction.oneBlockEquiv line 44
  11. lemma OAI.JiangSuConstruction.spectralFamily_zero line 48
  12. lemma OAI.JiangSuConstruction.spectralFamily_one line 62
  13. lemma OAI.JiangSuConstruction.spectralFamily_surjective line 77
  14. lemma OAI.JiangSuConstruction.diagonalContinuousHom_injective line 94