CoarseChildControlSpace.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.BinaryFraction.coarseIndexChildrenInvocations line 11

Source documentation

Invocation count follows the same child sequence, thresholds, recursive calls, penalty sweeps and accumulated array as the indexed evaluator.

def coarseIndexChildrenInvocations {B : ℕ} (q L : ℕ) (two : BinaryFraction)
    (width : Fin B → ℕ)
    (evaluate : Fin B → BinaryFraction → ℕ → CoarseBinaryArray × ℕ)
    (allocation : Fin B → BinaryFraction → ℕ → ℕ)
    (draw : Fin B → Fin B) (allowance : BinaryFraction) : List (Fin B) → ℕ → ℕ
  | [], _ => 1
  | i :: rest, start =>
    let threshold := coarseChildThresholdWithWork B q allowance (draw i)
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.width, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork

theorem OAI.EditApproximation.BinaryFraction.coarseIndexChildren_unused_k line 33
Source documentation
The loop's first argument does not contribute to its runtime control space.
Also declared: OAI/Combinatorics/EditApproximation/Coarse/CoarseChildAllocation.lean:33 (same declaration text).
```
private theorem coarseIndexChildren_unused_k {B : ℕ} (k q L : ℕ) (two : BinaryFraction)
    (width : Fin B → ℕ) (evaluate : Fin B → BinaryFraction → ℕ → CoarseBinaryArray × ℕ)
    (draw : Fin B → Fin B) (allowance : BinaryFraction) (indices : List (Fin B)) (start : ℕ) :
    coarseIndexChildren k q L two width evaluate draw allowance indices start =
      coarseIndexChildren 0 q L two width evaluate draw allowance indices start := by
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.width, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseIndexChildren
theorem OAI.EditApproximation.BinaryFraction.coarseIndexChildrenInvocations_le_work line 42