OAI/Combinatorics/EditApproximation/Refinement/PhysicalValueBits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit bit bounds for the actual returned physical table values.

  1. theorem OAI.EditApproximation.rationalEncodingBits_of_den_dvd line 10
  2. theorem OAI.EditApproximation.physicalRefinement_encoding_bits line 19
  3. theorem OAI.EditApproximation.refinement_denominator_base_bits line 44