OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredInitialization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Measured construction of the row tournament

Each leaf calls its measured initializer once; each internal node evaluates its two candidate keys. Binary paths are converted to array indices by an explicit recursive computation. No row array is constructed by this routine.

  1. def OAI.LowSpaceSubsetSum.Tournament.measuredBuild line 18
  2. theorem OAI.LowSpaceSubsetSum.Tournament.measuredBuild_value line 29
  3. theorem OAI.LowSpaceSubsetSum.Tournament.measuredBuild_work line 36
  4. def OAI.LowSpaceSubsetSum.PaddedRows.measuredIndex line 59

    Source documentation

    Little-endian binary evaluation. The cost includes access to a bit in a path built by at most d nested Fin.cons nodes.

    def measuredIndex : (d : ℕ) → (RowMerge.Path d) → ℕ × ℕ
  | 0, _ => (0, 1)
  | d + 1, p =>
    let t := measuredIndex d (fun i => p i.succ)
…

    Mentions: OAI.LowSpaceSubsetSum.RowMerge.Path

  5. theorem OAI.LowSpaceSubsetSum.PaddedRows.index_sum line 65
  6. theorem OAI.LowSpaceSubsetSum.PaddedRows.measuredIndex_value line 72
  7. theorem OAI.LowSpaceSubsetSum.PaddedRows.measuredIndex_work line 86
  8. def OAI.LowSpaceSubsetSum.FilteredStream.measuredFront line 103

    Source documentation

    Initialize and read one padded row, directly from the shared arrays.

    def measuredFront (left : Array α) (right : Array β)
    (row : α → PairCursor.State α right.size × ℕ) (d : ℕ) (p : RowMerge.Path d) :
    Option (RowMerge.Front d (α × β) (Cursor (α := α) right)) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.FilteredStream.row, OAI.LowSpaceSubsetSum.PairCursor.State, OAI.LowSpaceSubsetSum.RowMerge.Path, OAI.LowSpaceSubsetSum.RowMerge.Front, OAI.LowSpaceSubsetSum.FilteredStream.Cursor

  9. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredFront_value line 113
  10. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredFront_work line 124
  11. def OAI.LowSpaceSubsetSum.FilteredStream.measuredInitialTree line 139
  12. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredInitialTree_value line 145
  13. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredInitialTree_work line 155