OAI/Combinatorics/EditApproximation/Numerics/ScalarAllocation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.bitPowerAllocation_le_work line 15
2. def OAI.EditApproximation.coarseDenominatorAllocation line 26
3. theorem OAI.EditApproximation.coarseDenominatorAllocation_le_work line 37
4. theorem OAI.EditApproximation.bitCeilDivAllocation_le_work line 57
5. theorem OAI.EditApproximation.arithmeticMapAllocation_le_work line 68

   Source documentation

   Map allocation includes one result spine cell for every callback.

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

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

6. theorem OAI.EditApproximation.BinaryFraction.invAllocation_le_work line 84
7. theorem OAI.EditApproximation.BinaryFraction.divAllocation_le_work line 94
8. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorAllocation_le_work line 104
9. theorem OAI.EditApproximation.BinaryFraction.naturalCeilingAllocation_le_work line 120