OAI/Combinatorics/EditApproximation/Probability/RejectionMemoCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Literal rejection trials are charged only for source coordinates encountered by the shared memo execution. The accepted coordinates may influence the entire request list; failure counts remain independent.

  1. theorem OAI.EditApproximation.memo_selected_source_bits_le line 19
  2. theorem OAI.EditApproximation.memo_rejectionBits_expected_le line 45
  3. theorem OAI.EditApproximation.memo_rejectionBits_expected_le_real line 58