OAI/Combinatorics/EditApproximation/Refinement/PhysicalNodeRegret.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

First crossing for the literal physical refinement

Online and selected-group candidates are connected to the complete refinement by membership in its actual finite lists. Group success is the literal simultaneous estimator-error test, rather than a cone-bound assumption. The child environment remains fixed throughout this argument.

  1. theorem OAI.EditApproximation.representativeBandActions_zero_connection line 24
  2. theorem OAI.EditApproximation.sharedBandRationalAction_wide line 37
  3. theorem OAI.EditApproximation.rationalOnlineMinimum_le_member line 51
  4. theorem OAI.EditApproximation.rationalWideStep_online_exists line 61
  5. theorem OAI.EditApproximation.rationalWideStepCone_le_group line 78
  6. theorem OAI.EditApproximation.rationalWideStepCone_le_wide line 88
  7. def OAI.EditApproximation.unskippedGroupFailure line 100

    Source documentation

    The actual per-group failure test uses the rational estimated costs.

    def unskippedGroupFailure {α : Type*} (source target : List α) {M : ℕ}
    (parent : TargetInterval source.length) (b P thetaExponent : ℕ) (tau F : ℚ)
    (child initial value : Fin M → TargetInterval target.length → ℚ) (Q : ℕ)
    (members : List (UnskippedBand source target parent b P thetaExponent tau F child initial))
    (draw : ∀ scale : Fin (groupDyadicScales M b F).length,
      Fin (groupSampleCount M Q b (groupDyadicScaleAt M b F scale)) → Fin M)
    (gamma : ℚ) : Bool :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.groupDyadicScales, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.groupDyadicScaleAt

  8. theorem OAI.EditApproximation.unskippedGroupFailure_false line 111
  9. theorem OAI.EditApproximation.rationalWideStepCone_group_bound line 132

    Source documentation

    A selected group candidate in the actual list supplies the cone bound on the literal estimator-success event.

    theorem rationalWideStepCone_group_bound {α : Type*} (source target : List α) {M : ℕ}
    (parent : TargetInterval source.length) (representatives : List (ℕ × TargetInterval target.length))
    (b P F thetaExponent Q : ℕ) (tau a : ℚ)
    (parentInitial : TargetInterval target.length → ℚ)
    (child initial : Fin M → TargetInterval target.length → ℚ)
    (old current : Fin M × TargetInterval target.length → ℚ) (cell : ℕ × ℕ)
    (hnonempty : cellUnskippedBands source target parent b P F thetaExponent tau a
      parentInitial child initial cell ≠ [])
    (draw : ∀ scale : Fin (groupDyadicScales M b F).length,
      Fin (groupSampleCount M Q b (groupDyadicScaleAt M b F scale)) → Fin M)
    (specified : UnskippedBand source target parent b P thetaExponent tau F child initial)
    (hspecified : specified ∈ cellUnskippedBands source target parent b P F thetaExponent tau a
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.cellUnskippedBands, OAI.EditApproximation.groupDyadicScales, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.groupDyadicScaleAt, OAI.EditApproximation.UnskippedBand

  10. def OAI.EditApproximation.physicalNodeChildren line 177
  11. def OAI.EditApproximation.physicalNodeGroups line 180
  12. def OAI.EditApproximation.physicalNodeOnline line 183
  13. def OAI.EditApproximation.physicalNodeCone line 186
  14. def OAI.EditApproximation.physicalNodeOnlineValue line 194
  15. theorem OAI.EditApproximation.physicalNode_next_eq line 210

    Source documentation

    Literal candidate membership makes the online option present.

    theorem physicalNode_next_eq (hleaf : ¬ (parent).hi - (parent).lo ≤ 1)
    (t : ℕ) (q : TargetInterval target.length) (action : PhysicalRationalAction M target.length)
    (haction : action ∈ online t q) :
    (physicalRefinement source target U N P F A T delta choices node (t + 1) q : ℝ) =
      refinementUpdate (delta : ℝ) (cone t q : ℝ) (onlineValue t q : ℝ) := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalRationalAction, OAI.EditApproximation.physicalRefinement, OAI.EditApproximation.refinementUpdate

  16. theorem OAI.EditApproximation.physicalNode_online_le line 225

    Source documentation

    The actual online minimum is at most any listed shared band action.

    theorem physicalNode_online_le (t : ℕ) (q r : TargetInterval target.length)
    (action : Fin M → TargetInterval target.length)
    (haction : sharedBandRationalAction r action ∈ online t q) :
    (onlineValue t q : ℝ) ≤ (L : ℝ) * targetEndpointDistance q r +
      ∑ i, (history (t + 1) (i, action i) : ℝ) := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.sharedBandRationalAction, OAI.EditApproximation.targetEndpointDistance

  17. theorem OAI.EditApproximation.physicalNode_cone_le_old line 242

    Source documentation

    The old-index wide candidate remains one of the literal cone options.

    theorem physicalNode_cone_le_old (b : ℕ) (tau theta : ℚ) (r q : TargetInterval target.length)
    (child : Fin M → TargetInterval target.length → ℚ) (hrep : (b, r) ∈ representatives)
    (action : Fin M → TargetInterval target.length)
    (haction : action ∈ representativeBandActions source target parent r b P tau theta child) (t : ℕ) :
    (cone t q : ℝ) ≤ (L : ℝ) * targetEndpointDistance q r + ∑ i, (history t (i, action i) : ℝ) := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.representativeBandActions, OAI.EditApproximation.targetEndpointDistance

  18. theorem OAI.EditApproximation.physicalNode_comparison_lower line 257

    Source documentation

    True cost is bounded by the actual connection charge and clipped comparison children; no assumption about clipped warmup masses is needed.

    theorem physicalNode_comparison_lower (hM : 0 < M) (hF : 1 ≤ F)
    (b : ℕ) (tau theta : ℚ) (r q : TargetInterval target.length)
    (child : Fin M → TargetInterval target.length → ℚ)
    (comparison : Fin M → TargetInterval target.length)
    (hc : comparison ∈ representativeBandActions source target parent r b P tau theta child) (t : ℕ) :
    (stateEditCost (physicalSource source node) target q : ℝ) ≤
      (L : ℝ) * targetEndpointDistance q r + ∑ i,
        max (stateEditCost (physicalSource source (physicalChild node hbelow i)) target (comparison i) : ℝ)
          (history t (i, comparison i) : ℝ) := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.representativeBandActions, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.physicalChild

  19. def OAI.EditApproximation.physicalComparisonClipped line 285
  20. def OAI.EditApproximation.physicalNodeCellBands line 290
  21. def OAI.EditApproximation.physicalNodeSelectedGroup line 295
  22. def OAI.EditApproximation.physicalNodeGroupFailure line 302
  23. theorem OAI.EditApproximation.physicalNode_group_bound line 320

    Source documentation

    The selected whole-cell representative supplies the actual physical cone inequality on the actual estimator-success event.

    theorem physicalNode_group_bound (b thetaExponent Q : ℕ) (tau gamma : ℚ)
    (htau : 0 < tau) (hdelta : 0 ≤ delta) (cell : ℕ × ℕ)
    (hnonempty : physicalNodeCellBands source target U N P F A T node hbelow b thetaExponent tau cell ≠ [])
    (specified : UnskippedBand source target parent b P thetaExponent tau F
      (physicalBandChildMassTable source target U N P F A T node hbelow)
      (physicalBandChildInitial source target U N P F A node hbelow))
    (hspecified : specified ∈ physicalNodeCellBands source target U N P F A T node hbelow b thetaExponent tau cell)
    (t : ℕ) (draw : ∀ scale : Fin (groupDyadicScales M b F).length,
      Fin (groupSampleCount M Q b (groupDyadicScaleAt M b F scale)) → Fin M)
    (hselected : (physicalNodeSelectedGroup source target U N P F A T delta choices node hbelow
      b thetaExponent Q tau cell hnonempty t draw).rationalAction ∈ groups t)
    (hfailure : physicalNodeGroupFailure source target U N P F A T delta choices node hbelow
…

    Mentions: OAI.EditApproximation.physicalNodeCellBands, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.groupDyadicScales, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.groupDyadicScaleAt, OAI.EditApproximation.physicalNodeSelectedGroup, OAI.EditApproximation.physicalNodeGroupFailure

  24. theorem OAI.EditApproximation.physicalNode_clipped_upper line 362
  25. theorem OAI.EditApproximation.physicalNode_firstCrossing_regret line 378

    Source documentation

    Deterministic first-crossing transfer for the complete physical recurrence, using its actual sampled candidate lists and group-error test.

    theorem physicalNode_firstCrossing_regret
    (hleaf : ¬ (parent).hi - (parent).lo ≤ 1)
    (b thetaExponent Q : ℕ) (tau gamma κ : ℚ) (htau : 0 < tau)
    (hdelta : 0 < delta) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2) (cell : ℕ × ℕ)
    (hnonempty : physicalNodeCellBands source target U N P F A T node hbelow b thetaExponent tau cell ≠ [])
    (specified : UnskippedBand source target parent b P thetaExponent tau F
      (physicalBandChildMassTable source target U N P F A T node hbelow)
      (physicalBandChildInitial source target U N P F A node hbelow))
    (hspecified : specified ∈ physicalNodeCellBands source target U N P F A T node hbelow b thetaExponent tau cell)
    (hrep : (b, specified.center) ∈ representatives)
    (q : TargetInterval target.length)
    (hb : (b : ℝ) ≤ stateEditCost (physicalSource source node) target q)
…

    Mentions: OAI.EditApproximation.physicalNodeCellBands, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource