OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorCharge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial charge bound for the composed separator traversal

  1. def OAI.LowSpaceSubsetSum.SeparatorBlocks.coefficient line 13
  2. def OAI.LowSpaceSubsetSum.SeparatorBlocks.multiplicityLeft line 16
  3. def OAI.LowSpaceSubsetSum.SeparatorBlocks.multiplicityRight line 19
  4. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.chargeLeft_le line 22
  5. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.chargeRight_le line 53
  6. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.scans_le_multiplicities line 84