OAI/Combinatorics/EditApproximation/Refinement/PhysicalCoarseInputWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.physicalFamilyCoarseInputWork line 27

   Source documentation

   Source scans and a constant setup charge for each first coarse request.

   noncomputable def physicalFamilyCoarseInputWork (bits : ℕ) (encode : Sum Key Table → ℕ)
       (root : Table) : ℝ :=
   …

2. theorem OAI.EditApproximation.physicalFamilyCoarseQuery_input_cost_le_width line 35
3. theorem OAI.EditApproximation.physicalFamilyCoarseInputWork_le line 54