OAI/Combinatorics/EditApproximation/Refinement/PhysicalCoarseBitWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.physicalFamilyCoarseBitWork line 28

   Source documentation

   Bit arithmetic is executed once for each fresh coarse source request.

   noncomputable def physicalFamilyCoarseBitWork (bits : ℕ) (encode : Sum Key Table → ℕ)
       (root : Table) (coarse : PhysicalCoarseDraw source target B depth) : ℝ :=
   …

   Mentions: OAI.EditApproximation.PhysicalCoarseDraw

2. theorem OAI.EditApproximation.physicalFamilyCoarseBitWork_bound line 37