OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalReaderSpace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.physicalTableCodeAllocation_le_work line 15

   Source documentation

   Scalar RAM cells created by the node-code recurrence, two powers and entry/table arithmetic. The path and input request are borrowed.

   theorem physicalTableCodeAllocation_le_work {M J n : ℕ} (copies T S : ℕ)
       (request : PhysicalTableRequest M J n) :
       physicalTableCodeAllocation request ≤ (physicalTableCodeWithWork copies T S request).2 := by
   …

   Mentions: OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.physicalTableCodeAllocation, OAI.EditApproximation.physicalTableCodeWithWork

2. def OAI.EditApproximation.queryPhysicalTableReadHeap line 28
3. def OAI.EditApproximation.queryMeanReadHeap line 36
4. def OAI.EditApproximation.queryPhysicalEarlierReadHeap line 48
5. def OAI.EditApproximation.queryPhysicalRandomDataRequestHeap line 58