LocalGroupCones.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cell-keyed shared draws permit direct local group enumeration. The complete and local finite programs use the same draw at every cell label.

theorem OAI.EditApproximation.targetCell_of_cellTargetStates line 13
theorem OAI.EditApproximation.chooseCellGroupAction_center line 23
def OAI.EditApproximation.representativeCells line 42
theorem OAI.EditApproximation.representativeCells_mem line 47
def OAI.EditApproximation.completeCellGroupActions line 67
theorem OAI.EditApproximation.cellGroupAction_location line 75
theorem OAI.EditApproximation.localCellGroupActions_subset line 91
theorem OAI.EditApproximation.completeCellGroupActions_wide line 106

theorem OAI.EditApproximation.localCellGroupMinimum_eq line 118

Source documentation

All improving complete cell cones occur in the bounded local cell program. Identical cell keys use identical shared samples.

theorem localCellGroupMinimum_eq (q : TargetInterval target.length) (fallback : ℚ)
    (ha : 1 ≤ a) (hF : 1 ≤ F) (hfallback : fallback ≤ parentInitial q)
    (hcurrent : ∀ i r, 0 ≤ current i r)
    (hspatial : ∀ r, |parentInitial q - parentInitial r| ≤ 32 * F * targetEndpointDistance q r) :
    rationalMinimum fallback
        ((localCellGroupActions source target parent N P F exponent Q tau a parentInitial
          child initial current draw q).map
          (rationalActionValue (fun q r => targetEndpointDistance q r) (128 * F)
            (fun is => current is.1 is.2) q)) =
      rationalMinimum fallback
        ((completeCellGroupActions source target parent N P F exponent Q tau a parentInitial
          child initial current draw).map
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.rationalMinimum, OAI.EditApproximation.localCellGroupActions, OAI.EditApproximation.rationalActionValue, OAI.EditApproximation.completeCellGroupActions