Commit 2023-05-19 22:52 bf7ef0e8

View on Github →

feat(combinatorics/simple_graph/regularity): Increment partition (#19051) Define the increment partition and prove its two crucial properties:

  • It has size depending only on the size of the original partition
  • It increases the energy by a fixed amount This is all internal to the proof of SRL, so I made most lemmas private.

Estimated changes