OAI/Combinatorics/EditApproximation/Coarse/CoarseFirstRequestCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

First-request work for a complete independent coarse source. The query is adaptive; each entry is charged only on its first appearance. No conditioning on seed correctness occurs in this estimate.

  1. def OAI.EditApproximation.coarseFirstRequestWork line 21
  2. theorem OAI.EditApproximation.coarseFirstRequestWork_expected_le line 26