OAI/Combinatorics/EditApproximation/Binary/UnreducedStorage.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Polynomial raw storage bounds used by the Boolean numerical loops.

  1. theorem OAI.EditApproximation.UnreducedRational.storageBits_nat line 12
  2. theorem OAI.EditApproximation.UnreducedRational.storageBits_one line 15
  3. theorem OAI.EditApproximation.UnreducedRational.storageBits_zero line 17
  4. theorem OAI.EditApproximation.UnreducedRational.storageBits_neg line 19
  5. theorem OAI.EditApproximation.UnreducedRational.storageBits_add line 22
  6. theorem OAI.EditApproximation.UnreducedRational.storageBits_mul line 33
  7. theorem OAI.EditApproximation.UnreducedRational.storageBits_sub line 40
  8. theorem OAI.EditApproximation.UnreducedRational.storageBits_inv line 44
  9. theorem OAI.EditApproximation.UnreducedRational.storageBits_div line 52
  10. theorem OAI.EditApproximation.UnreducedRational.logarithmRatio_storageBits line 56
  11. theorem OAI.EditApproximation.UnreducedRational.logarithm_storageBits_poly line 64
  12. theorem OAI.EditApproximation.UnreducedRational.logarithmPartial_abs_le line 76
  13. theorem OAI.EditApproximation.UnreducedRational.logarithmPartial_storageBits line 91
  14. theorem OAI.EditApproximation.UnreducedRational.pow_storageBits_abs_le_one line 96
  15. theorem OAI.EditApproximation.UnreducedRational.pow_storageBits line 105
  16. def OAI.EditApproximation.UnreducedRational.logarithmStorageBudget line 114
  17. theorem OAI.EditApproximation.UnreducedRational.logarithmStorageBudget_mono line 118
  18. def OAI.EditApproximation.UnreducedRational.gradientStorageBudget line 124
  19. theorem OAI.EditApproximation.UnreducedRational.gradientCell_storageBits line 128
  20. theorem OAI.EditApproximation.UnreducedRational.dotList_den_bits line 155
  21. theorem OAI.EditApproximation.UnreducedRational.dotList_abs_le line 173
  22. theorem OAI.EditApproximation.UnreducedRational.dotList_storageBits line 191
  23. theorem OAI.EditApproximation.UnreducedRational.logarithmPartial_storageBits_uniform line 203