OAI/Combinatorics/EditApproximation/Coarse/CoarseThresholdStep.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseMultiply_nat_den line 15

   Source documentation

   Literal threshold numerator multiplication and denominator division. The fixed-denominator quotient retains a root's common array grid.

   private theorem coarseMultiply_nat_den (a : BinaryFraction) (n : ℕ) :
       (canonicalMulWithWork a (nat n)).1.representation.den = a.representation.den := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.canonicalMulWithWork, OAI.EditApproximation.BinaryFraction.nat

2. theorem OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork_value line 20
3. theorem OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork_den line 36
4. theorem OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork_value line 44

   Source documentation

   Local allowance division uses the same Boolean division and compression primitive as threshold construction.

    theorem coarseChildAllowanceWithWork_value (L : ℕ) (threshold : BinaryFraction)
       (hgrid : (threshold.value / L).den ∣ threshold.representation.den) :
       (coarseChildAllowanceWithWork L threshold).1.value = threshold.value / L := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork, OAI.EditApproximation.BinaryFraction.value

5. theorem OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork_den line 53