OAI/Combinatorics/EditApproximation/Binary/BinaryRawNumerics.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The optimizer's numerical loops executed on Boolean fraction storage. The value proofs identify the unreduced numerator and denominator, not just the represented rational. Thus the raw storage bounds apply to this code.

  1. theorem OAI.EditApproximation.BinaryFraction.vector_map_get line 15
  2. def OAI.EditApproximation.BinaryFraction.ofUnreduced line 19
  3. theorem OAI.EditApproximation.BinaryFraction.ofUnreduced_representation line 22
  4. theorem OAI.EditApproximation.BinaryFraction.ofUnreduced_width line 28
  5. theorem OAI.EditApproximation.BinaryFraction.nat_representation line 35
  6. theorem OAI.EditApproximation.BinaryFraction.one_representation line 43
  7. theorem OAI.EditApproximation.BinaryFraction.subWithWork_representation line 49
  8. theorem OAI.EditApproximation.BinaryFraction.divWithWork_representation line 56
  9. theorem OAI.EditApproximation.BinaryFraction.powWithWork_representation line 63
  10. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork_representation line 72
  11. theorem OAI.EditApproximation.BinaryFraction.logarithmWithWork_representation line 82
  12. theorem OAI.EditApproximation.BinaryFraction.dotListWithWork_representation line 91
  13. theorem OAI.EditApproximation.BinaryFraction.dotWithWork_representation line 103
  14. theorem OAI.EditApproximation.BinaryFraction.gradientCellWithWork_representation line 110
  15. theorem OAI.EditApproximation.BinaryFraction.nat_width_le_storageBits line 119
  16. theorem OAI.EditApproximation.BinaryFraction.zero_width_le_storageBits line 128
  17. theorem OAI.EditApproximation.BinaryFraction.powWithWork_width_le_storageBits line 130
  18. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork_width_le_storageBits line 138
  19. theorem OAI.EditApproximation.BinaryFraction.logarithmWithWork_width_le_storageBits line 147
  20. theorem OAI.EditApproximation.BinaryFraction.dotListWithWork_width_le_storageBits line 152
  21. theorem OAI.EditApproximation.BinaryFraction.gradientCellWithWork_width_le_storageBits line 162