OAI/Combinatorics/Chromatic/Shuffle/HNSlope.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.slopeValue line 18
  2. lemma OAI.ElementaryPositivity.RawShuffle.slopeValue_zero line 19
  3. lemma OAI.ElementaryPositivity.RawShuffle.slopeValue_add line 20
  4. lemma OAI.ElementaryPositivity.RawShuffle.slopeValue_pos_iff line 25
  5. lemma OAI.ElementaryPositivity.RawShuffle.slopeValue_nonpos_iff line 29
  6. lemma OAI.ElementaryPositivity.RawShuffle.decorated_zero_empty line 35
  7. def OAI.ElementaryPositivity.RawShuffle.highEmpty line 40
  8. def OAI.ElementaryPositivity.RawShuffle.lowEmpty line 42
  9. lemma OAI.ElementaryPositivity.RawShuffle.high_zero_unique line 45
  10. lemma OAI.ElementaryPositivity.RawShuffle.low_zero_unique line 50
  11. lemma OAI.ElementaryPositivity.RawShuffle.highSeries_zero line 56
  12. lemma OAI.ElementaryPositivity.RawShuffle.lowSeries_zero line 62
  13. lemma OAI.ElementaryPositivity.RawShuffle.decorated_value_nonpos line 69
  14. lemma OAI.ElementaryPositivity.RawShuffle.decorated_value_pos line 79
  15. lemma OAI.ElementaryPositivity.RawShuffle.highIndex_sign line 93
  16. lemma OAI.ElementaryPositivity.RawShuffle.lowIndex_sign line 103
  17. def OAI.ElementaryPositivity.RawShuffle.inputUnitEquiv line 121
  18. lemma OAI.ElementaryPositivity.RawShuffle.inputUnit_energy line 126
  19. def OAI.ElementaryPositivity.RawShuffle.literalInputCoefficient line 137
  20. theorem OAI.ElementaryPositivity.RawShuffle.literalInputCoefficient_eq line 141