OAI/Combinatorics/Chromatic/Shuffle/InputTorusEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.crossInteraction line 12
  2. def OAI.ElementaryPositivity.RawShuffle.staircaseShift line 15
  3. def OAI.ElementaryPositivity.RawShuffle.inputLinearEnergy line 18
  4. lemma OAI.ElementaryPositivity.RawShuffle.normalization_diagonal line 21
  5. lemma OAI.ElementaryPositivity.RawShuffle.crossInteraction_offdiagonal line 33
  6. def OAI.ElementaryPositivity.RawShuffle.inputTorusEnergy line 51
  7. theorem OAI.ElementaryPositivity.RawShuffle.inputListEnergy_normalized line 55
  8. abbrev OAI.ElementaryPositivity.RawShuffle.OutputStart line 79
  9. def OAI.ElementaryPositivity.RawShuffle.outputParameter line 81
  10. lemma OAI.ElementaryPositivity.RawShuffle.outputParameter_upper line 85
  11. lemma OAI.ElementaryPositivity.RawShuffle.finite_nonzero_dimensions_le line 91
  12. theorem OAI.ElementaryPositivity.RawShuffle.outputStarts_bounded_finite line 95
  13. lemma OAI.ElementaryPositivity.RawShuffle.euler_skew_sum line 126
  14. lemma OAI.ElementaryPositivity.RawShuffle.euler_skew_plane line 140
  15. theorem OAI.ElementaryPositivity.RawShuffle.slopeEulerSymmetric_of_plane line 161