OAI/Combinatorics/EditApproximation/Binary/FractionAllocation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.SignedBinary.addAllocation_le_work line 14

   Source documentation

   Fresh magnitude cells in exactly the branch taken by signed addition.

   theorem addAllocation_le_work (a b : SignedBinary) :
       a.addAllocation b ≤ (a.addWithWork b).2 := by
   …

   Mentions: OAI.EditApproximation.SignedBinary

2. theorem OAI.EditApproximation.SignedBinary.mulAllocation_le_work line 27
3. theorem OAI.EditApproximation.BinaryFraction.addAllocation_le_work line 40

   Source documentation

   Counts every newly allocated magnitude and denominator cell, including cross-products that are discarded after the numerator is computed.

   theorem addAllocation_le_work (a b : BinaryFraction) :
       a.addAllocation b ≤ (a.addWithWork b).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction

4. theorem OAI.EditApproximation.BinaryFraction.mulAllocation_le_work line 54
5. theorem OAI.EditApproximation.BinaryFraction.ltAllocation_le_work line 66

   Source documentation

   Signed comparisons themselves reuse input words; rational comparison allocates just its two cross-products.

   theorem ltAllocation_le_work (a b : BinaryFraction) :
       a.ltAllocation b ≤ (a.ltWithWork b).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction

6. theorem OAI.EditApproximation.BinaryFraction.canonicalizeAllocation_le_work line 76
7. theorem OAI.EditApproximation.BinaryFraction.canonicalAddAllocation_le_work line 86
8. theorem OAI.EditApproximation.BinaryFraction.canonicalMulAllocation_le_work line 93