OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorFamilyExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Constructing all four separator families from their bounded draws

The outer recursion has exactly four stages in the application. The returned row function contains stored arrays, and lookup traverses at most four tags.

  1. def OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.coupling line 18
  2. def OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.execution line 23
  3. def OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.run line 28
  4. theorem OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.value line 40
  5. theorem OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.work line 80
  6. def OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.Application.run line 98
  7. theorem OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.Application.value line 101
  8. theorem OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.Application.sizes line 113
  9. theorem OAI.LowSpaceSubsetSum.SeparatorFamilyExecution.Application.work line 120