OAI/Combinatorics/EditApproximation/Coarse/CoarsePenaltyArithmetic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseGridLeftWithWork_value line 12
2. theorem OAI.EditApproximation.BinaryFraction.coarseGridLeftWithWork_bounds line 22
3. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumWithWork_value line 40
4. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumWithWork_cost line 52
5. theorem OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork_value line 74

   Source documentation

   The two sweeps and final comparison, with every list pass charged.

    theorem coarseGridPenaltyWithWork_value (two : BinaryFraction) (source : List BinaryFraction)
       (htwo : two.value = 2)
       (hs : ∀ a ∈ source, a.representation.den = two.representation.den) :
       (coarseGridPenaltyWithWork two source).1.map value = coarsePenaltyTransform (source.map value) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.coarsePenaltyTransform

6. theorem OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork_cost line 85