OAI/Combinatorics/EditApproximation/Refinement/PhysicalScalarReadCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Each physical group or online source reader requests at most one scalar. The guards and dependent index transports do not create reads.

  1. theorem OAI.EditApproximation.groupQuery_transport_cost line 19
  2. theorem OAI.EditApproximation.physicalScalarGroupRead_cost_le line 30
  3. theorem OAI.EditApproximation.physicalScalarOnlineRead_cost_le line 50
  4. theorem OAI.EditApproximation.physicalFamilyGroupRead_cost_le line 73
  5. theorem OAI.EditApproximation.physicalFamilyOnlineRead_cost_le line 83