OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationStoredArrays.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Measured stored-array preparation with concrete prefix predicates

  1. def OAI.LowSpaceSubsetSum.IndexedMask.measuredDomain line 13
  2. theorem OAI.LowSpaceSubsetSum.IndexedMask.measuredDomain_semantic line 17
  3. theorem OAI.LowSpaceSubsetSum.IndexedMask.measuredDomain_work line 21
  4. def OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredArray line 30
  5. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredArray_value line 36
  6. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredArray_size line 44
  7. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredArray_work line 53
  8. def OAI.LowSpaceSubsetSum.RepresentationStoredArrays.prepare line 84

    Source documentation

    Shared arrays are returned once. The caller retains them through row initialization and all later reads. The mask equalities are proof arguments.

    def prepare (D : RepresentationParentData n) (F ones zeros : IndexedMask n) (j : Fin 2) :
    (Array (LeafRecord n) × Array (LeafRecord n)) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord

  9. theorem OAI.LowSpaceSubsetSum.RepresentationStoredArrays.left_value line 93
  10. theorem OAI.LowSpaceSubsetSum.RepresentationStoredArrays.right_value line 101
  11. theorem OAI.LowSpaceSubsetSum.RepresentationStoredArrays.prepare_value line 109
  12. theorem OAI.LowSpaceSubsetSum.RepresentationStoredArrays.prepare_sizes line 117
  13. theorem OAI.LowSpaceSubsetSum.RepresentationStoredArrays.prepare_work line 127