CoarseInitialWork.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Expected array work of the actual dyadic initial estimator

These are expectations of the concrete pruning-stopped counters. The linear penalty sweeps and representation bounds separately convert the array units into arithmetic and RAM work.

theorem OAI.EditApproximation.coarseInverseAllowanceFactor_nonneg line 23
theorem OAI.EditApproximation.coarseInverseAllowanceFactor_log_bound line 29
theorem OAI.EditApproximation.coarseWorkMultiplier_mono line 39

theorem OAI.EditApproximation.coarseRootArrayWork_expected_bound line 46

Source documentation

Root allowance equals the actual guessed distance. It cancels the array width 2k+1 in expectation, uniformly over every positive guess.

theorem coarseRootArrayWork_expected_bound {B D : ℕ} [NeZero B] {α : Type u}
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (k : ℕ) (Q lam : ℚ) (tree : CoarseSourceTree B α D)
    (hk : 0 < k) (hQ : 0 < Q) (hlam : 0 < lam)
    (factor : ℝ) (hfactor : 1 ≤ factor)
    (hinverse : coarseInverseAllowanceFactor B Q lam ≤ factor) :
    (∫ draws, (coarseActiveArrayWork k Q lam tree draws k : ℝ)
      ∂coarseDrawMeasure B D) ≤
      3 * B * tree.word.length * (D + 1 : ℕ) * factor ^ D := by
…

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

theorem OAI.EditApproximation.coarseInitialArrayWork_expected_bound line 81

Source documentation

The actual complete initial computation has the paper's expected array-work shape, on every execution and without conditioning on accuracy.

theorem coarseInitialArrayWork_expected_bound {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (Q lam : ℚ) (x y : List α) (hcapacity : coarseEntryWidth x y ≤ B ^ D)
    (hQ : 0 < Q) (hlam : 0 < lam)
    (factor : ℝ) (hfactor : 1 ≤ factor)
    (hinverse : coarseInverseAllowanceFactor B Q lam ≤ factor) :
    (∫ draws, (coarseInitialArrayWork B D Q lam x y draws : ℝ)
      ∂coarseInitialMeasure B D (coarseEntryWidth x y)) ≤
      3 * B * coarseEntryWidth x y * (Nat.clog 2 (coarseEntryWidth x y) + 1 : ℕ) *
        (D + 1 : ℕ) * factor ^ D := by
…

Mentions: OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.coarseInverseAllowanceFactor, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.coarseInitialMeasure