OAI/Combinatorics/LowSpaceSubsetSum/Separators/PreparedSeparatorExpectation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The measured checker under the actual independent family law

The ideal subset draws are identified with their stored bit codes. Decoding these codes preserves every sampled occurrence, so the existing scan expectation applies to the measured checker without changing its law.

  1. instance OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.sampleNonempty line 21
  2. def OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.codes line 26
  3. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.codes_size line 29
  4. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.codes_decode line 33
  5. def OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.prepare line 43
  6. def OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.check line 47
  7. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.acceptance line 52
  8. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.check_work line 65
  9. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.prepare_work line 80
  10. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorExpectation.mean_check_work line 87