OAI/Analysis/MatrixSigning/Complexity/RationalCost.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KS.W08.RatCounted line 9
  2. def OAI.KS.W08.RatCounted.pure line 17
  3. def OAI.KS.W08.RatCounted.bind line 18
  4. def OAI.KS.W08.RatCounted.add line 22
  5. def OAI.KS.W08.RatCounted.sub line 23
  6. def OAI.KS.W08.RatCounted.mul line 24
  7. def OAI.KS.W08.RatCounted.div line 25
  8. def OAI.KS.W08.RatCounted.neg line 26
  9. def OAI.KS.W08.RatCounted.inv line 27
  10. def OAI.KS.W08.RatCounted.positive line 28
  11. def OAI.KS.W08.RatCounted.traverse line 30
  12. theorem OAI.KS.W08.RatCounted.traverse_value_get line 34
  13. theorem OAI.KS.W08.RatCounted.traverse_ops line 39
  14. def OAI.KS.W08.RatCounted.sum line 44
  15. theorem OAI.KS.W08.RatCounted.sum_value line 48
  16. theorem OAI.KS.W08.RatCounted.sum_ops line 53
  17. def OAI.KS.W08.RatCounted.dot line 58
  18. theorem OAI.KS.W08.RatCounted.dot_value line 61
  19. theorem OAI.KS.W08.RatCounted.dot_ops line 67