OAI/Combinatorics/EditApproximation/Binary/BinaryMedianKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Binary multiplication, natural ceiling, sorting and clamping for the literal seed median. The stored words are sorted without decoding them.

  1. theorem OAI.EditApproximation.wordLEWithWork_value line 17

    Source documentation

    Comparison of two stored nonnegative binary words.

    @[simp] theorem wordLEWithWork_value (a b : List Bool) :
    (wordLEWithWork a b).1 = true ↔ bitWordValue a ≤ bitWordValue b := by
…

    Mentions: OAI.EditApproximation.wordLEWithWork, OAI.EditApproximation.bitWordValue

  2. theorem OAI.EditApproximation.wordLEWithWork_cost line 22
  3. theorem OAI.EditApproximation.wordMinWithWork_value line 30
  4. theorem OAI.EditApproximation.wordMinWithWork_length line 38
  5. theorem OAI.EditApproximation.wordInsertWithWork_value line 46
  6. theorem OAI.EditApproximation.wordInsertWithWork_length line 60
  7. theorem OAI.EditApproximation.wordInsertWithWork_words line 65
  8. theorem OAI.EditApproximation.wordInsertWithWork_cost line 86
  9. theorem OAI.EditApproximation.wordSortWithWork_value line 103
  10. theorem OAI.EditApproximation.wordSortWithWork_length line 112
  11. theorem OAI.EditApproximation.wordSortWithWork_words line 117
  12. theorem OAI.EditApproximation.wordSortWithWork_cost line 126
  13. theorem OAI.EditApproximation.BinaryFraction.naturalCeilingWithWork_length line 143
  14. theorem OAI.EditApproximation.BinaryFraction.scaledCeilingWithWork_value line 156
  15. def OAI.EditApproximation.BinaryFraction.scaledCeilingBitBudget line 161
  16. theorem OAI.EditApproximation.BinaryFraction.scaledCeilingWithWork_bounds line 164
  17. theorem OAI.EditApproximation.BinaryFraction.medianSeedWithWork_value line 186

    Source documentation

    The exact clamped upper median on binary words, including every copy's multiplication and ceiling, all sorting comparisons and the middle read.

    @[simp] theorem medianSeedWithWork_value (N multiplier : ℕ) (values : List BinaryFraction) :
    bitWordValue (medianSeedWithWork N multiplier values).1 =
      min N (upperMedian (values.map fun a => ⌈(multiplier : ℚ) * a.value⌉₊)) := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.BinaryFraction.medianSeedWithWork, OAI.EditApproximation.upperMedian

  18. def OAI.EditApproximation.BinaryFraction.medianSeedBitBudget line 203
  19. theorem OAI.EditApproximation.BinaryFraction.medianSeedWithWork_bounds line 207