OAI/Combinatorics/EditApproximation/Coarse/CoarseArrayHistory.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseChildrenArrayHistory line 11

   Source documentation

   Sum the stored bits of the four array results at each child step, including every recursive child's array history. This allows all these arrays to remain allocated instead of assuming prompt reclamation.

   def coarseChildrenArrayHistory {B d : ℕ} {α : Type*} (k q L : ℕ) (two : BinaryFraction)
       (evaluate : CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ →
         CoarseBinaryArray × ℕ)
       (history : CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ → ℕ)
       (allowance : BinaryFraction) :
       List (CoarseSourceTree B α d × Fin B × CoarseThresholdDraws B d) → ℕ → ℕ
     | [], _ => 0
     | (child, draw, below) :: rest, start =>
       let threshold := (coarseChildThresholdWithWork B q allowance draw).1
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork

2. def OAI.EditApproximation.BinaryFraction.coarseBinaryArrayHistory line 32
3. theorem OAI.EditApproximation.BinaryFraction.coarseChildrenArrayHistory_bound line 47