OAI/Combinatorics/EditApproximation/Coarse/CoarseAccessAllocation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.coarseSaturatingSubtractAllocation line 10

    Source documentation

    Comparisons and minimum reuse their input bit arrays.

    def coarseSaturatingSubtractAllocation (a b : ℕ) : ℕ :=
…
  2. theorem OAI.EditApproximation.coarseSaturatingSubtractAllocation_le_work line 14
  3. def OAI.EditApproximation.coarseDescriptorAllocation line 21
  4. theorem OAI.EditApproximation.coarseDescriptorAllocation_le_work line 25
  5. def OAI.EditApproximation.coarseChildOffsetAllocation line 33
  6. theorem OAI.EditApproximation.coarseChildOffsetAllocation_le_work line 38
  7. def OAI.EditApproximation.coarseFramedReadAllocation line 47
  8. theorem OAI.EditApproximation.coarseFramedReadAllocation_le_work line 54
  9. def OAI.EditApproximation.BinaryFraction.coarseReadShiftAllocation line 64
  10. theorem OAI.EditApproximation.BinaryFraction.coarseReadShiftAllocation_le_work line 72