OAI/Combinatorics/EditApproximation/Queries/QueryScalarReadSpace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.naturalPairWithWork_lower line 11
  2. theorem OAI.EditApproximation.physicalScalarCodeAllocation_le_work line 18

    Source documentation

    Address-recurrence and pairing cells; source data and node paths are borrowed.

    theorem physicalScalarCodeAllocation_le_work {M J N n exponent F Q R B : ℕ}
    (key : PhysicalScalarKey M J N n exponent F Q R B) :
    physicalScalarCodeAllocation key ≤ (physicalScalarCodeWithWork key).2 := by
…

    Mentions: OAI.EditApproximation.PhysicalScalarKey, OAI.EditApproximation.physicalScalarCodeAllocation, OAI.EditApproximation.physicalScalarCodeWithWork

  3. def OAI.EditApproximation.queryPhysicalScalarReadHeap line 58
  4. def OAI.EditApproximation.groupHeapTransport line 63
  5. def OAI.EditApproximation.queryPhysicalScalarGroupQueriesHeap line 70
  6. def OAI.EditApproximation.queryPhysicalScalarGroupReadHeap line 95
  7. def OAI.EditApproximation.queryPhysicalScalarOnlineReadHeap line 103
  8. theorem OAI.EditApproximation.queryFamilyTagAllocation_le_work line 131
  9. def OAI.EditApproximation.queryFamilyGroupReadHeap line 147
  10. def OAI.EditApproximation.queryFamilyOnlineReadHeap line 153