OAI/Combinatorics/EditApproximation/Coarse/CoarseArrayArithmetic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The coarse penalty sweep executed on shared-denominator Boolean cells. Each transition performs a numerator addition and a rational comparison.

  1. theorem OAI.EditApproximation.BinaryFraction.coarseMin_den line 14
  2. theorem OAI.EditApproximation.BinaryFraction.coarseMin_den_length line 23
  3. theorem OAI.EditApproximation.BinaryFraction.coarseGridAdd_den_length line 30
  4. theorem OAI.EditApproximation.BinaryFraction.coarseGridScanWithWork_value line 39

    Source documentation

    The complete left sweep, including writes and traversal.

     theorem coarseGridScanWithWork_value (two previous : BinaryFraction)
    (source : List BinaryFraction) (htwo : two.value = 2)
    (hp : previous.representation.den = two.representation.den)
    (hs : ∀ a ∈ source, a.representation.den = two.representation.den) :
    (coarseGridScanWithWork two previous source).1.map value =
      (source.map value).scanl (fun old a => min a (old + 2)) previous.value := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseGridScanWithWork, OAI.EditApproximation.BinaryFraction.value

  5. def OAI.EditApproximation.BinaryFraction.CoarseGridCell line 59

    Source documentation

    Invariant of a stored coarse cell on the common denominator.

    def CoarseGridCell (two a : BinaryFraction) (V D B : ℕ) : Prop :=
…

    Mentions: OAI.EditApproximation.BinaryFraction

  6. theorem OAI.EditApproximation.BinaryFraction.coarseGridScanWithWork_bounds line 63