OAI/Analysis/JiangSu/DimensionDrop/IteratedSpectrum.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.JiangSuConstruction.stageMultiplicities line 14
  2. def OAI.JiangSuConstruction.IteratedIndex line 17
  3. instance OAI.JiangSuConstruction.iteratedIndexFintype line 21
  4. instance OAI.JiangSuConstruction.iteratedIndexNonempty line 28
  5. def OAI.JiangSuConstruction.iteratedFamily line 39
  6. lemma OAI.JiangSuConstruction.spectralTransfer_sum line 43
  7. theorem OAI.JiangSuConstruction.scalarIterates_sum line 51
  8. lemma OAI.JiangSuConstruction.scalarIterates_sum_re line 71
  9. abbrev OAI.JiangSuCounting.I line 82
  10. def OAI.JiangSuCounting.falling line 84
  11. lemma OAI.JiangSuCounting.falling_nonneg line 87
  12. lemma OAI.JiangSuCounting.falling_le_one line 88
  13. lemma OAI.JiangSuCounting.falling_eq_one line 90
  14. lemma OAI.JiangSuCounting.falling_eq_zero line 95
  15. def OAI.JiangSuCounting.bump line 101
  16. lemma OAI.JiangSuCounting.bump_nonneg line 103
  17. lemma OAI.JiangSuCounting.bump_le_one line 105
  18. lemma OAI.JiangSuCounting.bump_zero_left line 112
  19. lemma OAI.JiangSuCounting.bump_zero_right line 114
  20. lemma OAI.JiangSuCounting.bump_one line 116
  21. lemma OAI.JiangSuCounting.falling_add_bump_le_one line 122
  22. def OAI.JiangSuCounting.complexify line 130
  23. lemma OAI.JiangSuCounting.complexify_re line 131
  24. def OAI.JiangSuCounting.cutoff line 133
  25. def OAI.JiangSuCounting.reserve line 134
  26. lemma OAI.JiangSuCounting.reserve_nonneg line 137
  27. lemma OAI.JiangSuCounting.reserve_positive line 138
  28. lemma OAI.JiangSuCounting.cutoff_source line 146
  29. lemma OAI.JiangSuCounting.cutoff_reserve_target line 155
  30. lemma OAI.JiangSuCounting.card_filter_le_of_sums line 166
  31. lemma OAI.JiangSuConstruction.cumulative_counts_near line 186
  32. theorem OAI.JiangSuConstruction.iterated_spectrum_shifted_counts line 214