CoarseLabelWork.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.coarseLabelChildren_le line 16

Source documentation

Only expanded internal nodes request their child thresholds. The full product seed is a specification; labels below a pruned node are never read.

private theorem coarseLabelChildren_le {B d : ℕ} {α : Type*} (Q lam allowance : ℚ)
    (labels arrays : CoarseSourceTree B α d → CoarseThresholdDraws B d → ℚ → ℕ)
    (children : List (CoarseSourceTree B α d × Fin B × CoarseThresholdDraws B d))
    (hle : ∀ child draw below, (child, draw, below) ∈ children → ∀ a, labels child below a ≤ arrays child below a) :
    coarseLabelChildren Q lam allowance labels children ≤
      coarseActiveChildrenWork Q lam allowance arrays children := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseLabelChildren, OAI.EditApproximation.coarseActiveChildrenWork

theorem OAI.EditApproximation.coarseLabelCount_le_arrayWork line 29
def OAI.EditApproximation.coarseThresholdBitWork line 54
Source documentation
Power-of-two threshold sampling consumes exactly the fixed word length per used label. binaryWord_uniform proves the output law of every draw.
```
def coarseThresholdBitWork {d : ℕ} {α : Type*} (r : ℕ) (Q lam : ℚ)
    (tree : CoarseSourceTree (2 ^ r) α d) (draws : CoarseThresholdDraws (2 ^ r) d)
    (allowance : ℚ) : ℕ := r * coarseLabelCount Q lam tree draws allowance
```
Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseLabelCount
theorem OAI.EditApproximation.coarseThresholdBitWork_le line 58