OAI/Combinatorics/EditApproximation/Probability/RejectionSelectedCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rejection counts are independent of all accepted values. Thus even an adaptive choice of coordinates incurs fewer than two word trials per selected coordinate in expectation. No unused source is charged.

  1. instance OAI.EditApproximation.rejectionAcceptedLaw_probability line 22
  2. instance OAI.EditApproximation.rejectionFailureLaw_probability line 28
  3. instance OAI.EditApproximation.rejectionRuntimeArrayLaw_probability line 36
  4. theorem OAI.EditApproximation.rejectionRuntimeArrayLaw_accepted line 40
  5. theorem OAI.EditApproximation.rejectionFailureArray_bits_integrable line 47
  6. theorem OAI.EditApproximation.rejectionSelectedBits_integrable line 56
  7. theorem OAI.EditApproximation.rejectionSelectedBits_expected_le line 65