CoarseArrayRepresentation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Binary storage operations used by the shared coarse-array recursion. A missing array is the same zero marker as in the rational specification.

def OAI.EditApproximation.BinaryFraction.coarseBinaryContents line 16
def OAI.EditApproximation.BinaryFraction.coarseRationalContents line 19
theorem OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyWithWork_value line 24
theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork_value line 34
Source documentation
Both input lists are visited once; the same denominator is retained.
```
 theorem coarseGridZipAddWithWork_value (left right : List BinaryFraction)
    (hden : ∀ a ∈ left, ∀ b ∈ right, a.representation.den = b.representation.den) :
    (coarseGridZipAddWithWork left right).1.map value =
      List.zipWith (· + ·) (left.map value) (right.map value) := by
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork, OAI.EditApproximation.BinaryFraction.value
theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork_cost line 48
theorem OAI.EditApproximation.BinaryFraction.coarseBinaryMapWithWork_value line 71