BinaryCellSourcePort.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceWithWork line 21
Source documentation
The same raw dyadic scale list and Fin-count indices as the original cell estimator, now with the cost of decoding every sampled coordinate.
```
def preparedCellGroupSourceWithWork (cell : ℕ × ℕ) :
    Option (BinaryBellmanAction (TargetInterval target.length)
      (Fin M × TargetInterval target.length) M) × ℕ :=
…
```
Mentions: OAI.EditApproximation.BinaryBellmanAction, OAI.EditApproximation.TargetInterval
theorem OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceWithWork_eq_cost line 35
theorem OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceWithWork_value line 62