OAI/Analysis/BoxTransport/Computation.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Computable rational arithmetic and exponential/flat-function approximation.

  1. abbrev OAI.BoxTransport.Routing.Computation.QCode line 16
  2. def OAI.BoxTransport.Routing.Computation.Qval line 18
  3. def OAI.BoxTransport.Routing.Computation.qZero line 20
  4. def OAI.BoxTransport.Routing.Computation.qOne line 21
  5. def OAI.BoxTransport.Routing.Computation.qNat line 22
  6. def OAI.BoxTransport.Routing.Computation.qNeg line 23
  7. def OAI.BoxTransport.Routing.Computation.qAdd line 24
  8. def OAI.BoxTransport.Routing.Computation.qMul line 28
  9. def OAI.BoxTransport.Routing.Computation.qInv line 31
  10. def OAI.BoxTransport.Routing.Computation.qSub line 36
  11. def OAI.BoxTransport.Routing.Computation.qDiv line 37
  12. def OAI.BoxTransport.Routing.Computation.qPow line 38
  13. def OAI.BoxTransport.Routing.Computation.qLe line 40
  14. instance OAI.BoxTransport.Routing.Computation.(instance at line 43) line 43
  15. theorem OAI.BoxTransport.Routing.Computation.Qval_zero line 45
  16. theorem OAI.BoxTransport.Routing.Computation.Qval_one line 46
  17. theorem OAI.BoxTransport.Routing.Computation.Qval_nat line 47
  18. theorem OAI.BoxTransport.Routing.Computation.Qval_neg line 48
  19. theorem OAI.BoxTransport.Routing.Computation.denominator_product line 52
  20. theorem OAI.BoxTransport.Routing.Computation.Qval_add line 59
  21. theorem OAI.BoxTransport.Routing.Computation.Qval_mul line 64
  22. theorem OAI.BoxTransport.Routing.Computation.Qval_inv line 70
  23. theorem OAI.BoxTransport.Routing.Computation.Qval_sub line 87
  24. theorem OAI.BoxTransport.Routing.Computation.Qval_div line 89
  25. theorem OAI.BoxTransport.Routing.Computation.Qval_pow line 91
  26. theorem OAI.BoxTransport.Routing.Computation.qLe_iff line 98
  27. theorem OAI.BoxTransport.Routing.Computation.Qval_surjective line 109
  28. theorem OAI.BoxTransport.Routing.Computation.pr_plus line 122
  29. theorem OAI.BoxTransport.Routing.Computation.pr_times line 125
  30. theorem OAI.BoxTransport.Routing.Computation.primrec_qNat line 129
  31. theorem OAI.BoxTransport.Routing.Computation.primrec_qNeg line 130
  32. theorem OAI.BoxTransport.Routing.Computation.primrec_qAdd line 132
  33. theorem OAI.BoxTransport.Routing.Computation.primrec_qMul line 150
  34. theorem OAI.BoxTransport.Routing.Computation.primrec_qInv line 164
  35. theorem OAI.BoxTransport.Routing.Computation.primrec_qSub line 179
  36. theorem OAI.BoxTransport.Routing.Computation.primrec_qDiv line 181
  37. theorem OAI.BoxTransport.Routing.Computation.primrec_qPow line 183
  38. theorem OAI.BoxTransport.Routing.Computation.primrec_qLe line 187
  39. def OAI.BoxTransport.Routing.Computation.qAbs line 200
  40. theorem OAI.BoxTransport.Routing.Computation.Qval_abs line 202
  41. theorem OAI.BoxTransport.Routing.Computation.primrec_qAbs line 208
  42. theorem OAI.BoxTransport.Routing.Computation.primrec_factorial line 211
  43. def OAI.BoxTransport.Routing.Computation.qTaylor line 220
  44. theorem OAI.BoxTransport.Routing.Computation.Qval_taylor line 223
  45. theorem OAI.BoxTransport.Routing.Computation.primrec_qTaylor line 233
  46. def OAI.BoxTransport.Routing.Computation.expStop line 242
  47. instance OAI.BoxTransport.Routing.Computation.(instance at line 247) line 247
  48. theorem OAI.BoxTransport.Routing.Computation.primrec_expStop line 249
  49. theorem OAI.BoxTransport.Routing.Computation.expStop_iff line 261
  50. theorem OAI.BoxTransport.Routing.Computation.exists_expStop line 270
  51. def OAI.BoxTransport.Routing.Computation.qExp line 284
  52. theorem OAI.BoxTransport.Routing.Computation.computable_qExp line 286
  53. theorem OAI.BoxTransport.Routing.Computation.real_exp_taylor_bound line 289
  54. theorem OAI.BoxTransport.Routing.Computation.qExp_error line 299
  55. def OAI.BoxTransport.Routing.Computation.flatTerm line 312
  56. theorem OAI.BoxTransport.Routing.Computation.flatTerm_zero_index line 314
  57. theorem OAI.BoxTransport.Routing.Computation.flatTerm_zero line 318
  58. theorem OAI.BoxTransport.Routing.Computation.contDiff_flatTerm line 321
  59. theorem OAI.BoxTransport.Routing.Computation.hasDerivAt_flatTerm line 326
  60. theorem OAI.BoxTransport.Routing.Computation.flatTerm_nonneg line 340
  61. theorem OAI.BoxTransport.Routing.Computation.flatTerm_bound line 347
  62. def OAI.BoxTransport.Routing.Computation.flatLipschitzBound line 365
  63. theorem OAI.BoxTransport.Routing.Computation.flatTerm_lipschitz line 367
  64. theorem OAI.BoxTransport.Routing.Computation.computable_ite line 387
  65. def OAI.BoxTransport.Routing.Computation.qBound line 393
  66. theorem OAI.BoxTransport.Routing.Computation.Qval_bound line 395
  67. theorem OAI.BoxTransport.Routing.Computation.primrec_qBound line 402
  68. def OAI.BoxTransport.Routing.Computation.qFlat line 405
  69. theorem OAI.BoxTransport.Routing.Computation.computable_qFlat line 410
  70. theorem OAI.BoxTransport.Routing.Computation.qFlat_error line 421