OAI/Combinatorics/EditApproximation/Coarse/CoarseDenominatorArithmetic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseDenominatorWithWork_value line 14

   Source documentation

   Construct the common denominator by Boolean products and binary exponentiation, charging all intermediate bit operations.

    theorem coarseDenominatorWithWork_value (allowanceDen q L branching : List Bool) (D : ℕ) :
       bitWordValue (coarseDenominatorWithWork allowanceDen q L branching D).1 =
         coarseCommonDenominator (bitWordValue allowanceDen) (bitWordValue q)
           (bitWordValue L) (bitWordValue branching) D := by
   …

   Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.coarseDenominatorWithWork, OAI.EditApproximation.coarseCommonDenominator

2. theorem OAI.EditApproximation.coarseDenominatorWithWork_length line 21
3. theorem OAI.EditApproximation.coarseDenominatorWithWork_cost line 29