OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredPivot.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Binary search with counted predicate evaluations

The predicate is evaluated exactly once at each nonempty interval. The count includes endpoint arithmetic and the actual predicate callback cost.

  1. def OAI.LowSpaceSubsetSum.BinaryPivot.measuredStep line 15
  2. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredStep_value line 27
  3. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredStep_work line 32
  4. def OAI.LowSpaceSubsetSum.BinaryPivot.measuredRun line 42

    Source documentation

    The accumulator makes the search loop tail recursive.

    def measuredRun (p : Fin n → Bool × ℕ) : ℕ → Cut n → ℕ → Cut n × ℕ
  | 0, c, work => (c, work)
  | k + 1, c, work =>
    let q := measuredStep p c
…

    Mentions: OAI.LowSpaceSubsetSum.BinaryPivot.Cut, OAI.LowSpaceSubsetSum.BinaryPivot.measuredStep

  5. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredRun_value line 48
  6. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredRun_work line 55
  7. def OAI.LowSpaceSubsetSum.BinaryPivot.measuredSearch line 67
  8. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredSearch_value line 70
  9. theorem OAI.LowSpaceSubsetSum.BinaryPivot.measuredSearch_work line 73