OAI/Combinatorics/EditApproximation/Coarse/CoarseArrayAllocation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.arithmeticMapAllocation_le_twice_work line 9

   Source documentation

   The same map trace, allowing a uniform factor two for callback allocation.

   theorem arithmeticMapAllocation_le_twice_work {α β : Type*} (f : α → β × ℕ)
       (allocation : α → ℕ) (values : List α)
       (h : ∀ a ∈ values, allocation a ≤ 2 * (f a).2) :
       arithmeticMapAllocation allocation values ≤ 2 * (arithmeticMapWithWork f values).2 := by
   …

   Mentions: OAI.EditApproximation.arithmeticMapAllocation, OAI.EditApproximation.arithmeticMapWithWork

2. def OAI.EditApproximation.BinaryFraction.coarseGridScanAllocation line 23
3. theorem OAI.EditApproximation.BinaryFraction.coarseGridScanAllocation_le_work line 31
4. def OAI.EditApproximation.BinaryFraction.coarseGridLeftAllocation line 43
5. theorem OAI.EditApproximation.BinaryFraction.coarseGridLeftAllocation_le_work line 47
6. theorem OAI.EditApproximation.BinaryFraction.coarseGridLeftWithWork_length line 56
7. def OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumAllocation line 67
8. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumAllocation_le_work line 71
9. def OAI.EditApproximation.BinaryFraction.coarseGridPenaltyAllocation line 86

   Source documentation

   Both reverse operations allocate their list spines; the element words are shared. Includes both sweeps, their discarded arrays and the final zip.

   def coarseGridPenaltyAllocation (two : BinaryFraction) (source : List BinaryFraction) : ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction

10. theorem OAI.EditApproximation.BinaryFraction.coarseGridPenaltyAllocation_le_work line 92
11. def OAI.EditApproximation.BinaryFraction.coarseGridZipAddAllocation line 105
12. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddAllocation_le_work line 109
13. def OAI.EditApproximation.BinaryFraction.coarseBinaryAddAllocation line 122
14. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryAddAllocation_le_work line 126
15. def OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyAllocation line 131
16. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyAllocation_le_work line 135
17. def OAI.EditApproximation.BinaryFraction.coarseBinaryMapAllocation line 141
18. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryMapAllocation_le_work line 145