OAI/Combinatorics/EditApproximation/Coarse/CoarseAccuracy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Pathwise accuracy of the concrete coarse recurrence

The events concern only fixed true child minima sampled with independent labels. The deterministic reconstruction requires no independence of approximate child costs.

  1. def OAI.EditApproximation.coarseTrueThresholdSum line 20

    Source documentation

    The true-cost threshold sum appearing in the simultaneous event.

    noncomputable def coarseTrueThresholdSum {B D : ℕ} {α : Type u}
    (k : ℕ) (Q : ℚ)
    (trueValue : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (allowance : ℚ) (transform : ℝ → ℝ) :
    List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D) →
      ℕ → Fin (2 * k + 1) → ℝ
  | [], _, _ => 0
  | (child, draw, _) :: rest, start, shift =>
    thresholdContribution (coarseChildThreshold B Q allowance draw) (allowance / Q)
      (transform ((univ.inf' univ_nonempty
        (fun next => trueValue child start next + 2 * Nat.dist shift.val next.val) : ℕ) : ℝ)) +
      coarseTrueThresholdSum k Q trueValue allowance transform rest (start + child.word.length) shift

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

  2. def OAI.EditApproximation.CoarseChildAccuracy line 35

    Source documentation

    Child accuracy at precisely the source positions visited by the actual traversal, with its actual per-child allowance.

    noncomputable def CoarseChildAccuracy {B D : ℕ} {α : Type u}
    (k : ℕ) (Q lam : ℚ)
    (trueValue : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (value : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ → Fin (2 * k + 1) → ℚ)
    (allowance : ℚ) (f : ℝ) :
    List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D) → ℕ → Prop
  | [], _ => True
  | (child, draw, below) :: rest, start =>
    (∀ shift,
      (trueValue child start shift : ℝ) / f -
          ((lam * coarseChildThreshold B Q allowance draw : ℚ) : ℝ) ≤
        value child below (lam * coarseChildThreshold B Q allowance draw) start shift ∧
…

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

  3. theorem OAI.EditApproximation.coarseThresholdChildrenCost_sandwich line 53

    Source documentation

    The actual rational estimator is trapped between two sums of fixed true costs, even when each child estimate depends on its threshold.

    theorem coarseThresholdChildrenCost_sandwich {B D : ℕ} {α : Type u}
    (k : ℕ) (Q lam : ℚ)
    (trueValue : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (value : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ → Fin (2 * k + 1) → ℚ)
    (children : List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D))
    (allowance : ℚ) (f : ℝ)
    (hQ : 0 ≤ Q) (ha : 0 ≤ allowance) (hf : 1 ≤ f)
    (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (start : ℕ) (shift : Fin (2 * k + 1))
    (hchild : CoarseChildAccuracy k Q lam trueValue value allowance f children start) :
    coarseTrueThresholdSum k Q trueValue allowance
        (fun cost => cost / (f * (1 + (lam : ℝ)))) children start shift ≤
…

    Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseChildAccuracy, OAI.EditApproximation.coarseTrueThresholdSum

  4. theorem OAI.EditApproximation.coarseThresholdChildrenCost_reconstruction line 94

    Source documentation

    Combining the true-cost concentration events gives the exact structural-factor update for the executable rational child traversal.

    theorem coarseThresholdChildrenCost_reconstruction {B D : ℕ} {α : Type u}
    (k : ℕ) (Q lam : ℚ)
    (trueValue : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (value : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ → Fin (2 * k + 1) → ℚ)
    (children : List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D))
    (allowance : ℚ) (f : ℝ)
    (hQ : 0 ≤ Q) (ha : 0 ≤ allowance) (hf : 1 ≤ f)
    (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (start : ℕ) (shift : Fin (2 * k + 1))
    (hchild : CoarseChildAccuracy k Q lam trueValue value allowance f children start)
    (hconcentrationLower :
      (1 - (lam : ℝ)) *
…

    Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseChildAccuracy

  5. def OAI.EditApproximation.coarseStructuralFactor line 136

    Source documentation

    The exact depth factor in Section 3.

    noncomputable def coarseStructuralFactor (lam : ℚ) (D : ℕ) : ℝ :=
…
  6. theorem OAI.EditApproximation.coarseStructuralFactor_one_le line 139
  7. theorem OAI.EditApproximation.coarseStructuralFactor_succ line 147
  8. def OAI.EditApproximation.CoarseDescendantEvents line 154

    Source documentation

    Events for all children, including children below a pruned node.

    def CoarseDescendantEvents {B D : ℕ} {α : Type u} (Q lam allowance : ℚ)
    (event : CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ → Prop) :
    List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D) → ℕ → Prop
  | [], _ => True
  | (child, draw, below) :: rest, start =>
    event child below (lam * coarseChildThreshold B Q allowance draw) start ∧
      CoarseDescendantEvents Q lam allowance event rest (start + child.word.length)

/-- The actual finite-tree event. At every node it uses only deterministic
true-cost minima and the node's current child threshold labels. -/

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

  9. def OAI.EditApproximation.CoarseAccuracyEvent line 164

    Source documentation

    The actual finite-tree event. At every node it uses only deterministic true-cost minima and the node's current child threshold labels.

    noncomputable def CoarseAccuracyEvent {B : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α)) :
    {D : ℕ} → CoarseSourceTree B α D → CoarseThresholdDraws B D → ℚ → ℕ → Prop
  | _, .leaf _, _, _, _ => True
  | D + 1, .branch children, (draws, below), allowance, start =>
    let data := List.ofFn (fun i => (children i, draws i, below i))
…

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

  10. theorem OAI.EditApproximation.CoarseDescendantEvents.to_accuracy line 186
  11. theorem OAI.EditApproximation.coarseThresholdEstimate_accurate line 211

    Source documentation

    On the concrete true-cost event, the literal rational pruned estimator has exactly the claimed depth-dependent error at every shift.

    theorem coarseThresholdEstimate_accurate {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (draws : CoarseThresholdDraws B D)
    (allowance : ℚ) (start : ℕ)
    (hQ : 0 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam < 1) (ha : 0 ≤ allowance)
    (hevent : CoarseAccuracyEvent k Q lam frame tree draws allowance start) :
    ∀ shift : Fin (2 * k + 1),
      (coarseShiftCost k frame tree start shift : ℝ) / coarseStructuralFactor lam D - allowance ≤
          coarseThresholdEstimate k Q lam frame tree draws allowance start shift ∧
      (coarseThresholdEstimate k Q lam frame tree draws allowance start shift : ℝ) ≤
        coarseStructuralFactor lam D * coarseShiftCost k frame tree start shift + allowance := by
…

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