CoarseBinaryEvaluation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.BinaryFraction.coarseBinaryChildren line 12

Source documentation

Shared evaluation of each child, followed by its exact two-pass penalty transform, threshold contribution and fixed-grid addition.

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

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

def OAI.EditApproximation.BinaryFraction.coarseBinaryEval line 32
Source documentation
Binary implementation of the pruning-stopped shared-array evaluator. The complete tree is a semantic indexed source; visited child descriptors carry their source offset and length, charged in coarseBinaryChildren.
```
def coarseBinaryEval {B : ℕ} {α : Type*} [DecidableEq α]
    (k q L : ℕ) (frame : List (Option α)) (two : BinaryFraction) :
    {d : ℕ} → CoarseSourceTree B α d → CoarseThresholdDraws B d → BinaryFraction → ℕ →
      CoarseBinaryArray × ℕ
  | _, tree, draws, allowance, start =>
    let prune := leWithWork (nat tree.word.length) allowance
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.leWithWork, OAI.EditApproximation.BinaryFraction.nat