OAI/Combinatorics/EditApproximation/Geometry/PrefixComparison.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Actual comparison prefixes in the finite wide action family

The cut is the start of the remaining comparator suffix, or the parent's end when that suffix is empty. Splitting at this cut preserves the literal connection budget. Splicing any enumerated prefix to the comparator suffix remains an enumerated wide action.

  1. def OAI.EditApproximation.connectionPrefixBoundary line 20
  2. theorem OAI.EditApproximation.realConnectionBudget_nonneg line 23
  3. theorem OAI.EditApproximation.realConnectionBudget_split line 30

    Source documentation

    Exact splitting at the first endpoint of the remaining suffix.

    theorem realConnectionBudget_split {n : ℕ} (states : List (TargetInterval n))
    (start : ℝ) (finish j : ℕ) :
    realConnectionBudget start states finish =
      realConnectionBudget start (states.take j) (connectionPrefixBoundary states finish j) +
      realConnectionBudget (connectionPrefixBoundary states finish j) (states.drop j) finish := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.realConnectionBudget, OAI.EditApproximation.connectionPrefixBoundary

  4. theorem OAI.EditApproximation.realConnectionBudget_append_le line 48

    Source documentation

    A detour through an arbitrary real cut only increases the budget.

    theorem realConnectionBudget_append_le {n : ℕ} (before after : List (TargetInterval n))
    (start finish cut : ℝ) :
    realConnectionBudget start (before ++ after) finish ≤
      realConnectionBudget start before cut + realConnectionBudget cut after finish := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.realConnectionBudget

  5. theorem OAI.EditApproximation.zero_connection_prefix_suffix line 65
  6. def OAI.EditApproximation.comparisonPrefixSplice line 85
  7. theorem OAI.EditApproximation.comparisonPrefixSplice_list line 88
  8. theorem OAI.EditApproximation.comparisonPrefixSplice_mem line 113
  9. def OAI.EditApproximation.comparisonPrefixShift line 125
  10. theorem OAI.EditApproximation.connectionPrefixBoundary_ofFn line 130
  11. theorem OAI.EditApproximation.comparisonPrefixShift_at_child line 137

    Source documentation

    Internal comparison cuts are exactly the next child's left shift.

    theorem comparisonPrefixShift_at_child {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (comparison : Fin M → TargetInterval ny) (j : Fin M) :
    comparisonPrefixShift parent r comparison j.val =
      ((comparison j).lo : ℝ) - (sourceChild parent j).lo := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.comparisonPrefixShift, OAI.EditApproximation.sourceChild

  12. def OAI.EditApproximation.comparisonPrefixValue line 143
  13. theorem OAI.EditApproximation.comparisonPrefixCost_eq line 147
  14. theorem OAI.EditApproximation.comparisonPrefixSplice_cost line 163

    Source documentation

    An arbitrary actual wide prefix can be completed by the comparator suffix at exactly the comparison cut.

    theorem comparisonPrefixSplice_cost {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (before comparison : Fin M → TargetInterval ny)
    (child : Fin M → TargetInterval ny → ℝ) (j : ℕ) (hj : j ≤ M)
    (hzero : endpointActionConnection r comparison = 0) :
    endpointActionValue r (comparisonPrefixSplice before comparison j) child ≤
      widePrefixCost parent r before child j (comparisonPrefixShift parent r comparison j) +
        (∑ i, child i (comparison i)) - comparisonPrefixValue comparison child j := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.endpointActionConnection, OAI.EditApproximation.endpointActionValue, OAI.EditApproximation.comparisonPrefixSplice, OAI.EditApproximation.widePrefixCost, OAI.EditApproximation.comparisonPrefixShift, OAI.EditApproximation.comparisonPrefixValue

  15. theorem OAI.EditApproximation.comparisonPrefixMinimum_bounds line 197

    Source documentation

    The comparison prefix is covered by the literal finite predictor. The full-action lower bound is later instantiated by the actual warmup Bellman value; no prefix estimate is assumed.

    theorem comparisonPrefixMinimum_bounds {nx ny M b P : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (comparison : Fin M → TargetInterval ny)
    (hcomparison : comparison ∈ wideActionList M parent r b P)
    (hnonempty : wideActionList M parent r b P ≠ [])
    (child : Fin M → TargetInterval ny → ℝ) (j : ℕ) (hj : j ≤ M)
    (hzero : endpointActionConnection r comparison = 0) (fullLower : ℝ)
    (hfull : ∀ action ∈ wideActionList M parent r b P,
      fullLower ≤ endpointActionValue r action child) :
    comparisonPrefixValue comparison child j - ((∑ i, child i (comparison i)) - fullLower) ≤
        widePrefixMinimum parent r (wideActionList M parent r b P) hnonempty child j
          (comparisonPrefixShift parent r comparison j) ∧
      widePrefixMinimum parent r (wideActionList M parent r b P) hnonempty child j
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.wideActionList, OAI.EditApproximation.endpointActionConnection, OAI.EditApproximation.endpointActionValue, OAI.EditApproximation.comparisonPrefixValue, OAI.EditApproximation.widePrefixMinimum, OAI.EditApproximation.comparisonPrefixShift

  16. def OAI.EditApproximation.wideActionMinimum line 222

    Source documentation

    Real form of the literal local wide-action minimum; the first member is duplicated as fallback, exactly as in the rational predictor.

    noncomputable def wideActionMinimum {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (b P : ℕ) (hnonempty : wideActionList M parent r b P ≠ [])
    (child : Fin M → TargetInterval ny → ℝ) : ℝ :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.wideActionList

  17. theorem OAI.EditApproximation.wideActionMinimum_le_member line 228
  18. theorem OAI.EditApproximation.comparisonPrefixMinimum_actual_bounds line 236

    Source documentation

    Exact finite predictor coverage with its actual wide-action minimum Z.

    theorem comparisonPrefixMinimum_actual_bounds {nx ny M b P : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (comparison : Fin M → TargetInterval ny)
    (hcomparison : comparison ∈ wideActionList M parent r b P)
    (hnonempty : wideActionList M parent r b P ≠ [])
    (child : Fin M → TargetInterval ny → ℝ) (j : ℕ) (hj : j ≤ M)
    (hzero : endpointActionConnection r comparison = 0) :
    comparisonPrefixValue comparison child j -
        ((∑ i, child i (comparison i)) - wideActionMinimum parent r b P hnonempty child) ≤
      widePrefixMinimum parent r (wideActionList M parent r b P) hnonempty child j
        (comparisonPrefixShift parent r comparison j) ∧
      widePrefixMinimum parent r (wideActionList M parent r b P) hnonempty child j
        (comparisonPrefixShift parent r comparison j) ≤ comparisonPrefixValue comparison child j :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.wideActionList, OAI.EditApproximation.endpointActionConnection, OAI.EditApproximation.comparisonPrefixValue, OAI.EditApproximation.wideActionMinimum, OAI.EditApproximation.widePrefixMinimum, OAI.EditApproximation.comparisonPrefixShift

  19. theorem OAI.EditApproximation.connectionBudget_zero_span line 253

    Source documentation

    A zero connection path has exactly the endpoint length span.

    theorem connectionBudget_zero_span {n : ℕ} (states : List (TargetInterval n))
    (start finish : ℕ) (hzero : connectionBudget start states finish = 0) :
    start ≤ finish ∧ (states.map fun state => state.hi - state.lo).sum = finish - start := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.connectionBudget

  20. theorem OAI.EditApproximation.comparisonPrefixShift_gap_sum line 275

    Source documentation

    The comparison cut displacement is the sum of the actual target-minus- source child length gaps in its prefix.

    theorem comparisonPrefixShift_gap_sum {α : Type*} (source target : List α)
    {M : ℕ} (hM : 0 < M) (parent : TargetInterval source.length)
    (r : TargetInterval target.length) (comparison : Fin M → TargetInterval target.length)
    (j : ℕ) (hj : j ≤ M) (hzero : endpointActionConnection r comparison = 0) :
    comparisonPrefixShift parent r comparison j - comparisonPrefixShift parent r comparison 0 =
      ∑ i, if i.val < j then
        stateLengthGap (substring source (sourceChild parent i).lo (sourceChild parent i).hi)
          target (comparison i) else 0 := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.endpointActionConnection, OAI.EditApproximation.comparisonPrefixShift, OAI.EditApproximation.stateLengthGap, OAI.EditApproximation.substring, OAI.EditApproximation.sourceChild