OAI/Combinatorics/LowSpaceSubsetSum/Separators/ComputedSeparatorFamilies.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Separator families with computed integer loop bounds

The actual family generator uses the sample size and four counts returned by the integer preparation. Source rounded parameters only specify the seed type and supply the correspondence proof.

  1. structure OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.Parameters line 18
  2. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.Parameters.ext line 23
  3. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.source line 31
  4. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.ofData line 34
  5. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.Seed line 37
  6. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.execute line 40
  7. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.transport line 43
  8. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.execute_transport line 45
  9. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.ofData_eq line 50
  10. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.draw line 58
  11. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.draw_pair line 62
  12. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.rounded line 67
  13. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.rounded_eq line 73
  14. def OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.run line 79
  15. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.value line 91
  16. theorem OAI.LowSpaceSubsetSum.ComputedSeparatorFamilies.work line 99