OAI/Combinatorics/Chromatic/Walls/FiniteReorderingEnergy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.card_fibres_injective_regrade line 12
  2. def OAI.ElementaryPositivity.RawShuffle.stringBlockEnergy line 34
  3. lemma OAI.ElementaryPositivity.RawShuffle.stringBlockEnergy_normalized line 37
  4. def OAI.ElementaryPositivity.RawShuffle.hnStringEnergy line 43
  5. lemma OAI.ElementaryPositivity.RawShuffle.hnStringEnergy_normalized line 48
  6. lemma OAI.ElementaryPositivity.RawShuffle.normalizedEnergy_injective line 60
  7. abbrev OAI.ElementaryPositivity.RawShuffle.OutputEnergyCoefficient line 65
  8. theorem OAI.ElementaryPositivity.RawShuffle.finiteReordering_energyCoefficient line 68
  9. lemma OAI.ElementaryPositivity.RawShuffle.finite_injective_regrade line 93
  10. lemma OAI.ElementaryPositivity.RawShuffle.sortedPackDegree_finite line 112
  11. lemma OAI.ElementaryPositivity.RawShuffle.inputEnergy_admissible line 119
  12. lemma OAI.ElementaryPositivity.RawShuffle.hnStringDegree_nonneg line 139
  13. lemma OAI.ElementaryPositivity.RawShuffle.outputEnergy_admissible line 157
  14. def OAI.ElementaryPositivity.RawShuffle.inputReorderingSeries line 179
  15. def OAI.ElementaryPositivity.RawShuffle.outputReorderingSeries line 183
  16. theorem OAI.ElementaryPositivity.RawShuffle.finiteReordering_laurent line 189