OnlineEarlierDependence.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual online optimizer reads only the recorded band coordinates and earlier child histories. Equality on the finite query cover suffices for equality of its returned action, including deterministic tie breaking.

theorem OAI.EditApproximation.rationalLinearizationMaximizer_congr_on line 14
theorem OAI.EditApproximation.finiteRationalOptimizer_congr_linear_on line 26
theorem OAI.EditApproximation.finiteOptimizerAction_congr_linear_on line 41
theorem OAI.EditApproximation.finiteOptimizerActionDraw_congr_linear_on line 65

theorem OAI.EditApproximation.rationalOnlineLinear_child_congr line 76

Source documentation

The gain at t and decrements at indices below t inspect exactly the input table indices at most t.

theorem rationalOnlineLinear_child_congr {β σ : Type*} (mass : β → ℚ)
    (left right : ℕ → β × σ → ℚ) (eta kappa : ℚ) (t : ℕ) (i : β × σ)
    (heq : ∀ s ≤ t, left s i = right s i) :
    rationalOnlineLinear eta kappa (childGain mass left) (childDecrement mass left) t i =
      rationalOnlineLinear eta kappa (childGain mass right) (childDecrement mass right) t i := by
…

Mentions: OAI.EditApproximation.rationalOnlineLinear, OAI.EditApproximation.childGain, OAI.EditApproximation.childDecrement

theorem OAI.EditApproximation.keyedOnlineCandidate_congr_history line 93
theorem OAI.EditApproximation.keyedOnlineCandidate_congr_earlier_cover line 127

theorem OAI.EditApproximation.localOnlineCandidates_congr_earlier_cover line 146

Source documentation

All online candidates for a local query, with their original order and ties, are fixed by the finite earlier-input cover.

theorem localOnlineCandidates_congr_earlier_cover {α : Type*} (source target : List α) {M : ℕ}
    (parent : TargetInterval source.length) (N P F exponent H history : ℕ) (tau a eta kappa : ℚ)
    (parentInitial : TargetInterval target.length → ℚ)
    (child initial : Fin M → TargetInterval target.length → ℚ)
    (left right : PhysicalChildTables M target.length) (t : ℕ)
    (integer : ℕ → TargetInterval target.length → ℕ) (q : TargetInterval target.length)
    (ht : t < history)
    (heq : ∀ i s r, (i, s, r) ∈ queryEarlierInputCover parent N P F exponent history a parentInitial q →
      left i s r = right i s r) :
    localOnlineCandidates source target parent N P F exponent H tau a eta kappa
      parentInitial child initial left t integer q =
      localOnlineCandidates source target parent N P F exponent H tau a eta kappa
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.queryEarlierInputCover, OAI.EditApproximation.localOnlineCandidates

theorem OAI.EditApproximation.physicalLocalOnline_congr_earlier_cover line 179

Source documentation

At a positive physical refinement time t, the online provider depends only on child times strictly less than t in the query cover.

theorem physicalLocalOnline_congr_earlier_cover
    (integer : PhysicalInternalNode M J → Fin R → ℕ → TargetInterval target.length → ℕ)
    (node : PhysicalInternalNode M J) (left right : PhysicalChildTables M target.length)
    (t : ℕ) (ht : 0 < t) (q : TargetInterval target.length)
    (heq : ∀ i s r, (i, s, r) ∈ queryEarlierInputCover
      (physicalSourceInterval source.length node.1) N P F exponent t (refinementFactor A F)
      (fun r => stageInitial source target U N P F A (node.1, r)) q →
        left i s r = right i s r) :
    physicalLocalOnline source target U N P F exponent H T A tau eta kappa integer node.1 left t q =
      physicalLocalOnline source target U N P F exponent H T A tau eta kappa integer node.1 right t q := by
…

Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.queryEarlierInputCover, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.refinementFactor, OAI.EditApproximation.stageInitial, OAI.EditApproximation.physicalLocalOnline