OAI/Combinatorics/Chromatic/Shuffle/HNThreshold.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.HNWord line 18
  2. abbrev OAI.ElementaryPositivity.RawShuffle.HighHNWord line 20
  3. abbrev OAI.ElementaryPositivity.RawShuffle.LowHNWord line 22
  4. lemma OAI.ElementaryPositivity.RawShuffle.hnOrdered_map_iff line 25
  5. def OAI.ElementaryPositivity.RawShuffle.hnWordEquiv line 30
  6. abbrev OAI.ElementaryPositivity.RawShuffle.HighHNIndex line 37
  7. abbrev OAI.ElementaryPositivity.RawShuffle.LowHNIndex line 39
  8. def OAI.ElementaryPositivity.RawShuffle.splitHNWord line 42
  9. lemma OAI.ElementaryPositivity.RawShuffle.splitHNWord_dimension line 45
  10. def OAI.ElementaryPositivity.RawShuffle.thresholdIndexEquiv line 53
  11. lemma OAI.ElementaryPositivity.RawShuffle.thresholdIndexEquiv_symm_energy line 60
  12. lemma OAI.ElementaryPositivity.RawShuffle.thresholdIndexEquiv_energy line 69
  13. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_injective line 85
  14. abbrev OAI.ElementaryPositivity.RawShuffle.highEnergy line 108
  15. abbrev OAI.ElementaryPositivity.RawShuffle.lowEnergy line 110
  16. def OAI.ElementaryPositivity.RawShuffle.highDecorated line 113
  17. def OAI.ElementaryPositivity.RawShuffle.lowDecorated line 115
  18. lemma OAI.ElementaryPositivity.RawShuffle.highEnergy_admissible line 118
  19. lemma OAI.ElementaryPositivity.RawShuffle.lowEnergy_admissible line 121
  20. def OAI.ElementaryPositivity.RawShuffle.highSeries line 125
  21. def OAI.ElementaryPositivity.RawShuffle.lowSeries line 127
  22. def OAI.ElementaryPositivity.RawShuffle.hnSeries line 129
  23. lemma OAI.ElementaryPositivity.RawShuffle.hnSeries_threshold line 133