OAI/Combinatorics/EditApproximation/Queries/QuerySourceGatherCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.source_read_sum_bound line 11
2. def OAI.EditApproximation.BinaryFraction.queryGroupGatherBitBudget line 23
3. def OAI.EditApproximation.BinaryFraction.queryOnlineGatherBitBudget line 27
4. theorem OAI.EditApproximation.queryGroupSourceGather_work_bound line 35
5. theorem OAI.EditApproximation.queryOnlineSourceGather_work_bound line 65