OAI/Combinatorics/EditApproximation/Geometry/RankedMemoStorage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Every value retained by the actual binary dictionary obeys the semantic value bound. This includes every allocated path, not only keys queried after the computation.

  1. def OAI.EditApproximation.BinaryMemo.AllValues line 14
  2. theorem OAI.EditApproximation.BinaryMemo.allValues_empty line 17
  3. theorem OAI.EditApproximation.BinaryMemo.AllValues.insert line 22
  4. def OAI.EditApproximation.BinaryMemo.rationalStorage line 36

    Source documentation

    One word each for the tag and two child pointers, plus the value bits. Counting bits individually is an upper bound on logarithmic-word storage.

    def rationalStorage : BinaryMemo ℚ → ℕ
  | .empty => 0
  | .node value left right =>
    3 + (value.map rationalEncodingBits).getD 0 + left.rationalStorage + right.rationalStorage

    Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.BinaryMemo.value, OAI.EditApproximation.BinaryMemo.left, OAI.EditApproximation.BinaryMemo.right, OAI.EditApproximation.rationalEncodingBits

  5. theorem OAI.EditApproximation.BinaryMemo.rationalStorage_le line 41
  6. theorem OAI.EditApproximation.FiniteQuery.run_invariant line 66
  7. theorem OAI.EditApproximation.rankedMemoEvaluate_allValues line 77
  8. theorem OAI.EditApproximation.SourceRanked.memo_allValues line 129