OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGroupSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.cellScaleReadDraw_cast_plain line 15
2. theorem OAI.EditApproximation.cellScaleReadDraw_cast_bound line 22
3. def OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWork line 38
4. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWork_eq_cost line 50
5. theorem OAI.EditApproximation.BinaryFraction.add_source_cost line 71
6. theorem OAI.EditApproximation.BinaryFraction.computedCellSource_cast_cost line 81
7. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWork line 102
8. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWork_eq_cost_on line 117
9. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWork_eq_cost line 163
10. def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWork line 179

    Source documentation

    Every admitted scale uses the source-aware whole-cell loop.

    def preparedLocalCellGroupsSourceWithWork (N : ℕ)
        (draw : CellGroupReadDraws M F Q) (query : TargetInterval target.length) :
        List (BinaryBellmanAction (TargetInterval target.length)
          (Fin M × TargetInterval target.length) M) × ℕ :=
    …

    Mentions: OAI.EditApproximation.CellGroupReadDraws, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryBellmanAction

11. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWork_eq_cost_on line 194
12. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWork_eq_cost line 259