OAI/Combinatorics/EditApproximation/Coarse/CoarseReadCore.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseReadShiftCost line 9
2. theorem OAI.EditApproximation.BinaryFraction.coarseReadShiftCost_eq line 15
3. def OAI.EditApproximation.BinaryFraction.coarseReadCore line 28

   Source documentation

   Core arithmetic over source descriptors. The separate descriptor/read counter charges address arithmetic and original-array accesses.

   def coarseReadCore {B : ℕ} {α : Type*} [DecidableEq α]
       (k q L n : ℕ) (source target : List α) (two : BinaryFraction) :
       (d : ℕ) → (offset : ℕ) → CoarseThresholdDraws B d → BinaryFraction → ℕ →
         CoarseBinaryArray × ℕ
     | 0, offset, _, allowance, start =>
       let size := coarseDescriptorLength B 0 n offset
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.coarseDescriptorLength