CoarseArrayEval.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Shared coarse array evaluation

A missing array is a constant-zero marker. An expanded child is evaluated once, then transformed by the two linear sweeps, thresholded, and added to its siblings. The instrumented counter charges rational arithmetic and comparisons; allocation, source-width preprocessing and integer addressing are separate parts of the machine implementation.

abbrev OAI.EditApproximation.CoarseStoredArray line 23
Source documentation
Stored cells have the complete shift-domain length; none is zero.
```
abbrev CoarseStoredArray (n : ℕ) := Option {cells : List ℚ // cells.length = n}
```
def OAI.EditApproximation.coarseStoredRead line 25
def OAI.EditApproximation.coarseStoredOfFn line 30
theorem OAI.EditApproximation.coarseStoredRead_ofFn line 33
def OAI.EditApproximation.coarseStoredMap line 37
theorem OAI.EditApproximation.coarseStoredMap_read line 41
theorem OAI.EditApproximation.coarseStoredMap_cost line 48
def OAI.EditApproximation.coarseStoredAdd line 52
theorem OAI.EditApproximation.coarseStoredAdd_read line 59
theorem OAI.EditApproximation.coarseStoredAdd_cost line 69
def OAI.EditApproximation.coarseStoredPenalty line 74
Source documentation
The costed linear sweeps operate on the stored cells.
```
def coarseStoredPenalty {n : ℕ} : CoarseStoredArray n → CoarseStoredArray n × ℕ
  | none => (none, 0)
  | some cells =>
    let result := coarseCostedPenaltyTransform cells.1
…
```
Mentions: OAI.EditApproximation.CoarseStoredArray, OAI.EditApproximation.coarseCostedPenaltyTransform
theorem OAI.EditApproximation.coarseStoredPenalty_cost line 81
theorem OAI.EditApproximation.coarseStoredPenalty_read line 88

def OAI.EditApproximation.coarseArrayEvalChildren line 110

Source documentation

Each list member is evaluated once and its whole array is reused.

def coarseArrayEvalChildren {B D : ℕ} {α : Type u}
    (k : ℕ) (Q lam : ℚ)
    (evaluate : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ →
      CoarseStoredArray (2 * k + 1) × ℕ) (allowance : ℚ) :
    List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D) → ℕ →
      CoarseStoredArray (2 * k + 1) × ℕ
  | [], _ => (none, 0)
  | (child, draw, below) :: rest, start =>
    let threshold := coarseChildThreshold B Q allowance draw
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseStoredArray, OAI.EditApproximation.coarseChildThreshold

def OAI.EditApproximation.coarseArrayEval line 130

Source documentation

Actual shared-array recursion. Pruning creates a zero marker and does not traverse any descendants.

def coarseArrayEval {B : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α)) :
    {D : ℕ} → CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ →
      CoarseStoredArray (2 * k + 1) × ℕ
  | _, tree, draws, allowance, start =>
    if (tree.word.length : ℚ) ≤ allowance then (none, 1) else
    match tree, draws with
    | .leaf letter, _ =>
      (coarseStoredOfFn (fun shift =>
        (coarseShiftCost k frame (.leaf (B := B) letter) start shift : ℚ)),
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseStoredArray, OAI.EditApproximation.coarseStoredOfFn, OAI.EditApproximation.coarseShiftCost

theorem OAI.EditApproximation.coarseArrayEvalChildren_read line 147
theorem OAI.EditApproximation.coarseArrayEval_read line 177

theorem OAI.EditApproximation.coarseArrayEvalChildren_cost line 203

Source documentation

The instrumented child traversal charges the once-evaluated child plus at most sixteen parent shift-array units for each list member.

theorem coarseArrayEvalChildren_cost {B D : ℕ} {α : Type u}
    (k : ℕ) (Q lam : ℚ)
    (evaluate : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ →
      CoarseStoredArray (2 * k + 1) × ℕ)
    (work : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ)
    (children : List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D))
    (hchild : ∀ child draw below, (child, draw, below) ∈ children →
      ∀ a start, (evaluate child below a start).2 ≤ 32 * work child below a + 1)
    (allowance : ℚ) (start : ℕ) :
    (coarseArrayEvalChildren k Q lam evaluate allowance children start).2 ≤
      32 * coarseActiveChildrenWork Q lam allowance work children +
        16 * children.length * (2 * k + 1) := by
…

theorem OAI.EditApproximation.coarseArrayEval_cost line 238

Source documentation

Every execution's shared evaluation has the rational-operation cost bounded by the very same pruning-stopped counter used in expectation.

theorem coarseArrayEval_cost {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (draws : CoarseThresholdDraws B D)
    (allowance : ℚ) (start : ℕ) :
    (coarseArrayEval k Q lam frame tree draws allowance start).2 ≤
      32 * coarseActiveArrayWork k Q lam tree draws allowance + 1 := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseArrayEval, OAI.EditApproximation.coarseActiveArrayWork

theorem OAI.EditApproximation.coarseArrayEval_expected_bound line 271

Source documentation

Expected rational-operation count for the actual shared-array evaluator. This estimate holds on every execution, including inaccurate ones.

theorem coarseArrayEval_expected_bound {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (allowance : ℚ) (start : ℕ)
    (hQ : 0 < Q) (hlam : 0 < lam) (ha : 0 < allowance) :
    (∫ draws, ((coarseArrayEval k Q lam frame tree draws allowance start).2 : ℝ)
      ∂coarseDrawMeasure B D) ≤
      32 * ((B * (2 * k + 1) : ℕ) * (tree.word.length : ℝ) / allowance *
        coarseWorkMultiplier (coarseInverseAllowanceFactor B Q lam) D) + 1 := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseArrayEval, OAI.EditApproximation.coarseDrawMeasure, OAI.EditApproximation.coarseWorkMultiplier, OAI.EditApproximation.coarseInverseAllowanceFactor