OAI/Combinatorics/EditApproximation/Geometry/GroupInputDependence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Shared group estimates depend only on the explicitly bounded sampled input cover. Thus scanning or repeatedly scoring all cell members can reuse gathered values rather than issue new recursive requests.

  1. theorem OAI.EditApproximation.groupScaleEstimate_congr_queried line 13
  2. theorem OAI.EditApproximation.dyadicUnskippedGroupEstimate_congr_cover line 37
  3. theorem OAI.EditApproximation.rational_argmax_congr_on line 64
  4. theorem OAI.EditApproximation.selectGroupMember_congr_on line 78
  5. theorem OAI.EditApproximation.chooseCellGroupAction_congr_cover line 86