OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineSourceSpace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.reduceOnlineIntegerAllocation_le_work line 14
2. theorem OAI.EditApproximation.filterMapAllocation_le_three_work line 23

   Source documentation

   The only multiplicative allowance needed by the labeled optimizer.

   theorem filterMapAllocation_le_three_work {α β : Type*} (f : α → Option β × ℕ)
       (allocation : α → ℕ) (xs : List α) (h : ∀ x ∈ xs, allocation x ≤ 3 * (f x).2) :
       filterMapAllocation f allocation xs ≤ 3 * (filterMapWithWork f xs).2 := by
   …

   Mentions: OAI.EditApproximation.filterMapAllocation, OAI.EditApproximation.filterMapWithWork

3. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadAllocation line 45
4. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineReadAllocation_le_work line 63