OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGroupActions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete local group list is obtained by executed scale, cell, band, and sampled-selection loops. The source keeps the original finite sample counts and shares its draws between all members of each cell.

  1. theorem OAI.EditApproximation.BinaryFraction.refinementScaleGuardWithWork_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.cellDraw_roundtrip line 22
  3. def OAI.EditApproximation.BinaryFraction.localGroupScaleWithWork line 29
  4. theorem OAI.EditApproximation.BinaryFraction.localGroupScaleWithWork_value line 47
  5. def OAI.EditApproximation.BinaryFraction.localCellGroupsWithWork line 72
  6. theorem OAI.EditApproximation.BinaryFraction.flatMap_filter_condition line 90

    Also declared: OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedLocalGroups.lean:79 (same declaration text).

  7. theorem OAI.EditApproximation.BinaryFraction.localCellGroupsWithWork_value line 100