OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedFamilyExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measured independent separator-family draws

The inner loop bounds are supplied as explicit integer parameters. The application wrapper obtains these integers from SeparatorParameterExecution.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.families line 17
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.familyUsing line 25
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.familiesUsing line 40
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.maskBudget line 47
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.fixedSize_budget line 50
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.families_bounded line 57
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.familiesUsing_bounded line 85