OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSamplerCoupling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The bounded samplers for the actual dependent representation history

  1. def OAI.LowSpaceSubsetSum.bitArrayCoupling line 18
  2. theorem OAI.LowSpaceSubsetSum.bitArrayCoupling_uniform line 26
  3. theorem OAI.LowSpaceSubsetSum.bitArrayCoupling_failure line 32
  4. def OAI.LowSpaceSubsetSum.bitsSubsetEquiv line 35
  5. def OAI.LowSpaceSubsetSum.signCoupling line 41
  6. theorem OAI.LowSpaceSubsetSum.signCoupling_uniform line 44
  7. theorem OAI.LowSpaceSubsetSum.signCoupling_failure line 49
  8. def OAI.LowSpaceSubsetSum.initialSubset line 52
  9. theorem OAI.LowSpaceSubsetSum.initialSubset_card line 55
  10. def OAI.LowSpaceSubsetSum.initialSubsetEquiv line 58
  11. def OAI.LowSpaceSubsetSum.fixedSizeCoupling line 66
  12. theorem OAI.LowSpaceSubsetSum.fixedSizeCoupling_uniform line 70
  13. theorem OAI.LowSpaceSubsetSum.fixedSizeCoupling_failure line 84
  14. instance OAI.LowSpaceSubsetSum.RepresentationSetup.guessNonempty line 93

    Also declared: OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSamplerExecution.lean:102 (same declaration text).

  15. def OAI.LowSpaceSubsetSum.RepresentationSetup.layoutCoupling line 96
  16. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.layoutCoupling_uniform line 99
  17. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.layoutCoupling_failure line 103
  18. def OAI.LowSpaceSubsetSum.RepresentationSetup.guessesCoupling line 107
  19. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessesCoupling_uniform line 110
  20. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessesCoupling_failure line 113
  21. def OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsCoupling line 122
  22. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsCoupling_uniform line 126
  23. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsCoupling_failure line 131
  24. def OAI.LowSpaceSubsetSum.RepresentationSetup.guessHistoryCoupling line 142
  25. def OAI.LowSpaceSubsetSum.RepresentationSetup.partitionHistoryCoupling line 145
  26. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessHistoryCoupling_uniform line 149
  27. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.partitionHistoryCoupling_uniform line 153