OAI/Combinatorics/EditApproximation/Coarse/CoarseScalarAllocation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseGridNatAllocation line 10

   Source documentation

   Arithmetic-only allocation; the caller owns the input words.

   def coarseGridNatAllocation (denominator : List Bool)
       (hden : 0 < bitWordValue denominator) (n : ℕ) : ℕ :=
   …

   Mentions: OAI.EditApproximation.bitWordValue

2. theorem OAI.EditApproximation.BinaryFraction.coarseGridNatAllocation_le_work line 16
3. def OAI.EditApproximation.BinaryFraction.coarseGridAddAllocation line 26
4. theorem OAI.EditApproximation.BinaryFraction.coarseGridAddAllocation_le_work line 30
5. def OAI.EditApproximation.BinaryFraction.coarseDivideAllocation line 39
6. theorem OAI.EditApproximation.BinaryFraction.coarseDivideAllocation_le_work line 43
7. def OAI.EditApproximation.BinaryFraction.coarseContributionAllocation line 52
8. theorem OAI.EditApproximation.BinaryFraction.coarseContributionAllocation_le_work line 57
9. def OAI.EditApproximation.BinaryFraction.coarseChildThresholdAllocation line 67

   Source documentation

   Includes all three natural literal numerators and their unit denominators.

   def coarseChildThresholdAllocation (B q : ℕ) (allowance : BinaryFraction) (draw : Fin B) : ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction

10. theorem OAI.EditApproximation.BinaryFraction.coarseChildThresholdAllocation_le_work line 74
11. def OAI.EditApproximation.BinaryFraction.coarseChildAllowanceAllocation line 86
12. theorem OAI.EditApproximation.BinaryFraction.coarseChildAllowanceAllocation_le_work line 89