OAI/Combinatorics/LowSpaceSubsetSum/Storage/CanonicalPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Canonical consecutive labels for representation partitions

The base labeling is determined by the sorted mixer domain. Randomly permuting these labels gives the analyzed uniform balanced partition, with no choice of an arbitrary initial coloring required by the runtime.

  1. def OAI.LowSpaceSubsetSum.CanonicalPartition.rankFiber line 16
  2. theorem OAI.LowSpaceSubsetSum.CanonicalPartition.size_eq line 31
  3. def OAI.LowSpaceSubsetSum.CanonicalPartition.ranks line 36
  4. def OAI.LowSpaceSubsetSum.CanonicalPartition.labels line 40
  5. def OAI.LowSpaceSubsetSum.CanonicalPartition.labelFiber line 44
  6. def OAI.LowSpaceSubsetSum.CanonicalPartition.base line 51
  7. def OAI.LowSpaceSubsetSum.CanonicalPartition.coupling line 57
  8. theorem OAI.LowSpaceSubsetSum.CanonicalPartition.coupling_uniform line 62
  9. theorem OAI.LowSpaceSubsetSum.CanonicalPartition.coupling_failure line 68
  10. def OAI.LowSpaceSubsetSum.CanonicalPartition.execution line 80
  11. theorem OAI.LowSpaceSubsetSum.CanonicalPartition.execution_bounded line 89