CoarseEstimator.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete pruned coarse estimator

The random labels are a finite complete tree of integers in 1,...,B. Every execution below uses rational arithmetic and literal finite minima; pruned arrays are represented by the zero function. Accuracy events are kept separate from this executable definition.

theorem OAI.EditApproximation.coarseThresholdContribution_cast line 29
Source documentation
Rational version of the literal threshold contribution.
```
theorem coarseThresholdContribution_cast (threshold scale value : ℚ) :
    (coarseThresholdContribution threshold scale value : ℝ) =
      thresholdContribution threshold scale value := by
…
```
Mentions: OAI.EditApproximation.coarseThresholdContribution, OAI.EditApproximation.thresholdContribution
theorem OAI.EditApproximation.coarseThresholdContribution_nonneg line 40
theorem OAI.EditApproximation.coarseChildThreshold_nonneg line 57
Source documentation
Section 3's pruned rational recurrence. All labels are supplied beforehand; execution exposes a label only when its parent is expanded.
```
theorem coarseChildThreshold_nonneg {B : ℕ} {Q allowance : ℚ} (draw : Fin B)
    (hQ : 0 ≤ Q) (ha : 0 ≤ allowance) : 0 ≤ coarseChildThreshold B Q allowance draw := by
…
```
Mentions: OAI.EditApproximation.coarseChildThreshold
theorem OAI.EditApproximation.coarseChildThreshold_pos line 62
theorem OAI.EditApproximation.coarseThresholdChildrenCost_nonneg line 68
theorem OAI.EditApproximation.coarseThresholdEstimate_nonneg line 83

theorem OAI.EditApproximation.coarse_penalty_minimum_error line 104

Source documentation

Adding a nonnegative connection penalty and taking the actual finite minimum preserves the multiplicative/additive child guarantee.

theorem coarse_penalty_minimum_error {ι : Type*} [Fintype ι] [Nonempty ι]
    (trueCost penalty : ι → ℕ) (estimate : ι → ℚ) (f error : ℝ)
    (hf : 1 ≤ f)
    (hlower : ∀ i, (trueCost i : ℝ) / f - error ≤ estimate i)
    (hupper : ∀ i, (estimate i : ℝ) ≤ f * trueCost i + error) :
    ((univ.inf' univ_nonempty (fun i => trueCost i + penalty i) : ℕ) : ℝ) / f - error ≤
        ((univ.inf' univ_nonempty (fun i => estimate i + (penalty i : ℚ)) : ℚ) : ℝ) ∧
      ((univ.inf' univ_nonempty (fun i => estimate i + (penalty i : ℚ)) : ℚ) : ℝ) ≤
        f * ((univ.inf' univ_nonempty (fun i => trueCost i + penalty i) : ℕ) : ℝ) + error := by
…

theorem OAI.EditApproximation.coarse_penalty_minimum_zero line 141

Source documentation

A zero literal penalty minimum forces the zero-cost child to use the parent's same shift.

theorem coarse_penalty_minimum_zero (k : ℕ) (value : Fin (2 * k + 1) → ℕ)
    (shift : Fin (2 * k + 1))
    (hzero : univ.inf' univ_nonempty
      (fun next => value next + 2 * Nat.dist shift.val next.val) = 0) : value shift = 0 := by
…

theorem OAI.EditApproximation.coarse_estimated_minimum_zero line 154

Source documentation

If the same-shift child estimate is zero, its actual minimum is zero.

theorem coarse_estimated_minimum_zero (k : ℕ) (value : Fin (2 * k + 1) → ℚ)
    (shift : Fin (2 * k + 1)) (hnonnegative : ∀ next, 0 ≤ value next)
    (hzero : value shift = 0) :
    univ.inf' univ_nonempty (fun next => value next + (2 * Nat.dist shift.val next.val : ℕ)) = 0 := by
…

theorem OAI.EditApproximation.coarseThresholdChildrenCost_zero line 166

theorem OAI.EditApproximation.coarseThresholdEstimate_zero line 204

Source documentation

Exact zero states remain zero on every label realization, without conditioning on any accuracy event.

theorem coarseThresholdEstimate_zero {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (draws : CoarseThresholdDraws B D)
    (allowance : ℚ) (start : ℕ) (shift : Fin (2 * k + 1))
    (hQ : 0 < Q) (hlam : 0 < lam) (ha : 0 < allowance)
    (hzero : coarseShiftCost k frame tree start shift = 0) :
    coarseThresholdEstimate k Q lam frame tree draws allowance start shift = 0 := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseShiftCost, OAI.EditApproximation.coarseThresholdEstimate