CoarseWork.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Expected active work in the concrete pruned coarse tree

The counter records the array units of the actual execution; pruning stops all descendant visits. Constant child overhead is charged to its expanded parent. The linear-sweep proof converts these units to rational operations; bit/RAM charging is separate.

def OAI.EditApproximation.coarseExpectedArrayWork line 30

Source documentation

Finite conditional expectation recurrence for the same active work. The root labels are independent uniforms, and each child uses its own independent recursive label tree.

noncomputable def coarseExpectedArrayWork {B : ℕ} {α : Type u} (k : ℕ) (Q lam : ℚ) :
    {D : ℕ} → CoarseSourceTree B α D → ℚ → ℝ
  | _, tree, allowance =>
    if (tree.word.length : ℚ) ≤ allowance then 0 else
    match tree with
    | .leaf _ => (B * (2 * k + 1) : ℕ)
    | .branch children =>
      (B * (2 * k + 1) : ℕ) +
        ∑ i : Fin B, uniformMean (fun draw : Fin B =>
          coarseExpectedArrayWork k Q lam (children i)
            (lam * coarseChildThreshold B Q allowance draw))

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.uniformMean, OAI.EditApproximation.coarseChildThreshold

def OAI.EditApproximation.coarseInverseAllowanceFactor line 42
def OAI.EditApproximation.coarseWorkMultiplier line 45
theorem OAI.EditApproximation.coarseWorkMultiplier_nonneg line 48
theorem OAI.EditApproximation.coarseWorkMultiplier_succ line 52
theorem OAI.EditApproximation.coarseWorkMultiplier_le line 59
theorem OAI.EditApproximation.uniformMean_mono line 67
Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Probability/SampledRegret.lean:19 (different declaration text). Qualify references as OAI.EditApproximation.uniformMean_mono@path.
theorem OAI.EditApproximation.uniformMean_const_mul line 71
theorem OAI.EditApproximation.coarse_inverse_allowance_mean line 78
Source documentation
Exact expected inverse allowance under the literal integer threshold law. This identity is independent of all estimated arrays and accuracy.
```
theorem coarse_inverse_allowance_mean (B : ℕ) [NeZero B] (Q lam allowance : ℚ)
    (hQ : 0 < Q) (hlam : 0 < lam) (ha : 0 < allowance) :
    uniformMean (fun draw : Fin B =>
      1 / ((lam * coarseChildThreshold B Q allowance draw : ℚ) : ℝ)) =
        coarseInverseAllowanceFactor B Q lam / allowance := by
…
```
Mentions: OAI.EditApproximation.uniformMean, OAI.EditApproximation.coarseChildThreshold, OAI.EditApproximation.coarseInverseAllowanceFactor
theorem OAI.EditApproximation.coarseBranch_word_length line 100

theorem OAI.EditApproximation.coarseExpectedArrayWork_bound line 108

Source documentation

The expected active work has the paper's inverse-allowance bound. The inequality holds regardless of every coarse accuracy event.

theorem coarseExpectedArrayWork_bound {B D : ℕ} [NeZero B] {α : Type u}
    (k : ℕ) (Q lam : ℚ) (tree : CoarseSourceTree B α D) (allowance : ℚ)
    (hQ : 0 < Q) (hlam : 0 < lam) (ha : 0 < allowance) :
    coarseExpectedArrayWork k Q lam tree allowance ≤
      (B * (2 * k + 1) : ℕ) * (tree.word.length : ℝ) / allowance *
        coarseWorkMultiplier (coarseInverseAllowanceFactor B Q lam) D := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseExpectedArrayWork, OAI.EditApproximation.coarseWorkMultiplier, OAI.EditApproximation.coarseInverseAllowanceFactor

theorem OAI.EditApproximation.coarseActiveChildrenWork_eq_sum line 181
theorem OAI.EditApproximation.coarseActiveChildrenWork_ofFn line 194
theorem OAI.EditApproximation.coarseActiveArrayWork_integral line 207
Source documentation
The finite expectation recurrence is exactly the expectation of the actual pruning-stopped execution counter under the concrete recursive law.
```
theorem coarseActiveArrayWork_integral {B D : ℕ} [NeZero B] {α : Type u}
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (k : ℕ) (Q lam : ℚ) (tree : CoarseSourceTree B α D) (allowance : ℚ) :
    (∫ draws, (coarseActiveArrayWork k Q lam tree draws allowance : ℝ)
      ∂coarseDrawMeasure B D) = coarseExpectedArrayWork k Q lam tree allowance := by
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseActiveArrayWork, OAI.EditApproximation.coarseDrawMeasure, OAI.EditApproximation.coarseExpectedArrayWork

theorem OAI.EditApproximation.coarseActiveArrayWork_expected_bound line 277

Source documentation

Expected active work, stated directly for the actual execution law, without any conditioning on accuracy.

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

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