ComparisonBandCoverage.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Comparison action coverage by the computed predictor

Masses, gaps, prefix costs and curvature are those of the actual labeled comparison action. The finite wide-action minimum supplies Z. No scalar prefix prediction contract is assumed.

def OAI.EditApproximation.comparisonActionMass line 18
def OAI.EditApproximation.comparisonActionCurvature line 22
theorem OAI.EditApproximation.comparisonPrefixShift_origin line 32

theorem OAI.EditApproximation.comparisonPrefixPrediction_error line 45

Source documentation

The actual comparison prefix prediction error is at most sqrt(W*K) + 2*(W-Z). All mass, gap and finite-minimum inequalities are derived from the genuine child table lower invariant.

theorem comparisonPrefixPrediction_error {α : Type*} (source target : List α)
    {M b P : ℕ} (hM : 0 < M) (parent : TargetInterval source.length)
    (r : TargetInterval target.length) (comparison : Fin M → TargetInterval target.length)
    (hcomparison : comparison ∈ wideActionList M parent r b P)
    (hnonempty : wideActionList M parent r b P ≠ [])
    (child : Fin M → TargetInterval target.length → ℝ)
    (a : ℝ) (ha : 1 ≤ a)
    (hchild : ∀ i s, max ((stateEditCost
      (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s : ℝ) / a)
        |stateLengthGap (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s| ≤
          child i s)
    (hzero : endpointActionConnection r comparison = 0)
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.wideActionList, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.substring, OAI.EditApproximation.sourceChild, OAI.EditApproximation.stateLengthGap, OAI.EditApproximation.endpointActionConnection

theorem OAI.EditApproximation.comparison_computedBandActions_mem line 144

Source documentation

The derived analytic estimate places the actual comparison action in the literal rational finite filter once its explicit numerical budget holds.

theorem comparison_computedBandActions_mem {α : Type*} (source target : List α)
    {M b P : ℕ} (hM : 0 < M) (parent : TargetInterval source.length)
    (r : TargetInterval target.length) (comparison : Fin M → TargetInterval target.length)
    (hcomparison : comparison ∈ wideActionList M parent r b P)
    (hnonempty : wideActionList M parent r b P ≠ [])
    (tau theta : ℚ) (child : Fin M → TargetInterval target.length → ℚ)
    (a : ℝ) (ha : 1 ≤ a)
    (hchild : ∀ i s, max ((stateEditCost
      (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s : ℝ) / a)
        |stateLengthGap (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s| ≤
          (child i s : ℝ))
    (hzero : endpointActionConnection r comparison = 0)
…

theorem OAI.EditApproximation.comparison_representativeBandActions_mem line 190

Source documentation

The representative wrapper computes precisely the velocity used in the preceding finite-filter membership result.

theorem comparison_representativeBandActions_mem {α : Type*} (source target : List α)
    {M b P : ℕ} (hM : 0 < M) (parent : TargetInterval source.length)
    (r : TargetInterval target.length) (comparison : Fin M → TargetInterval target.length)
    (hcomparison : comparison ∈ wideActionList M parent r b P)
    (hnonempty : wideActionList M parent r b P ≠ [])
    (tau theta : ℚ) (child : Fin M → TargetInterval target.length → ℚ)
    (a : ℝ) (ha : 1 ≤ a)
    (hchild : ∀ i s, max ((stateEditCost
      (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s : ℝ) / a)
        |stateLengthGap (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target s| ≤
          (child i s : ℝ))
    (hzero : endpointActionConnection r comparison = 0)
…