OAI/Combinatorics/EditApproximation/Geometry/GatheredLocalStep.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The current-index part of a local step can be evaluated in two stages: gather the shared sampled inputs, select the whole-cell actions, then gather their actual costs and the online action costs.

  1. theorem OAI.EditApproximation.localCellGroupActions_congr_cover line 16
  2. theorem OAI.EditApproximation.rationalActionValues_congr_cover line 47
  3. def OAI.EditApproximation.gatheredInputValue line 62
  4. theorem OAI.EditApproximation.gatheredInputValue_eq line 66
  5. theorem OAI.EditApproximation.mem_orderedInputs line 77
  6. theorem OAI.EditApproximation.orderedInputs_length line 83
  7. def OAI.EditApproximation.gatheredFiniteValue line 89
  8. theorem OAI.EditApproximation.gatheredFiniteValue_eq line 93
  9. def OAI.EditApproximation.gatheredCellGroupActions line 114
  10. theorem OAI.EditApproximation.gatheredCellGroupActions_eq line 119
  11. def OAI.EditApproximation.gatheredLocalWideStep line 126
  12. theorem OAI.EditApproximation.gatheredLocalWideStep_eq line 138
  13. def OAI.EditApproximation.gatheredLocalCurrentCalls line 165

    Source documentation

    Actual oracle requests in the two gathers. Each list is sorted and contains no duplicates; overlap between the two stages is harmless.

    def gatheredLocalCurrentCalls : ℕ :=
…
  14. theorem OAI.EditApproximation.gatheredLocalCurrentCalls_le line 174