OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSeparatorJoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint survival and acceptance for the actual separator trial

The surviving representation is retained in the probability event so that its designated lifted residue can be located in the input-only schedule.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketTrial_joint_acceptance_probability line 17