OAI/Combinatorics/EditApproximation/Binary/BinaryIndexedLeaf.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.indexedLeafWithWork_le line 13

    Source documentation

    The indexed terminal result is written directly as a binary rational.

    theorem indexedLeafWithWork_le (table : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
    (symbol : Option ℕ) (lo hi : ℕ) :
    (indexedLeafWithWork table symbolBits positionBits symbol lo hi).1 ≤ hi + 1 := by
…

    Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.indexedLeafWithWork

  2. theorem OAI.EditApproximation.binaryIndexedLeafWithWork_value line 23
  3. theorem OAI.EditApproximation.binaryIndexedLeafWithWork_bounds line 29
  4. theorem OAI.EditApproximation.integerBinaryIndexedLeafWithWork_cost line 41