OAI/Geometry/Convex/GeneralMahler/Intervals/Basic.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Fixed-denominator rational interval certificates (§07–08). Unknown intervals admit all real values.

  1. inductive OAI.GeneralMahler.Cert.IV line 9
  2. def OAI.GeneralMahler.Cert.IV.den line 15
  3. def OAI.GeneralMahler.Cert.IV.w line 16
  4. def OAI.GeneralMahler.Cert.IV.Has line 17
  5. instance OAI.GeneralMahler.Cert.IV.(instance at line 21) line 21
  6. def OAI.GeneralMahler.Cert.IV.c line 23
  7. instance OAI.GeneralMahler.Cert.IV.(instance at line 24) line 24
  8. def OAI.GeneralMahler.Cert.IV.add0 line 26
  9. instance OAI.GeneralMahler.Cert.IV.(instance at line 29) line 29
  10. def OAI.GeneralMahler.Cert.IV.n0 line 30
  11. instance OAI.GeneralMahler.Cert.IV.(instance at line 33) line 33
  12. instance OAI.GeneralMahler.Cert.IV.(instance at line 34) line 34
  13. def OAI.GeneralMahler.Cert.IV.ud line 37

    Source comment

    upward round division
    def ud (a b : Int) : Int := -((-a)/b)
  14. def OAI.GeneralMahler.Cert.IV.mul0 line 38
  15. instance OAI.GeneralMahler.Cert.IV.(instance at line 44) line 44
  16. def OAI.GeneralMahler.Cert.IV.posInv line 46
  17. def OAI.GeneralMahler.Cert.IV.inv0 line 47
  18. instance OAI.GeneralMahler.Cert.IV.(instance at line 50) line 50
  19. instance OAI.GeneralMahler.Cert.IV.(instance at line 51) line 51
  20. def OAI.GeneralMahler.Cert.IV.pow0 line 53
  21. instance OAI.GeneralMahler.Cert.IV.(instance at line 56) line 56
  22. def OAI.GeneralMahler.Cert.IV.pos0 line 58
  23. def OAI.GeneralMahler.Cert.IV.clampNN line 61
  24. def OAI.GeneralMahler.Cert.IV.Zmax line 65
  25. def OAI.GeneralMahler.Cert.IV.Zmin line 68
  26. def OAI.GeneralMahler.Cert.IV.Zabs line 69
  27. def OAI.GeneralMahler.Cert.IV.sq line 70
  28. def OAI.GeneralMahler.Cert.IV.span line 71
  29. def OAI.GeneralMahler.Cert.IV.meet line 74
  30. def OAI.GeneralMahler.Cert.IV.Less line 78
  31. def OAI.GeneralMahler.Cert.IV.LeB line 81
  32. def OAI.GeneralMahler.Cert.IV.SubB line 84
  33. lemma OAI.GeneralMahler.Cert.IV.dpos line 89
  34. lemma OAI.GeneralMahler.Cert.IV.rpos line 90
  35. lemma OAI.GeneralMahler.Cert.IV.w_mono line 91
  36. lemma OAI.GeneralMahler.Cert.IV.w_strict line 93
  37. lemma OAI.GeneralMahler.Cert.IV.w_max line 95
  38. lemma OAI.GeneralMahler.Cert.IV.w_min line 96
  39. lemma OAI.GeneralMahler.Cert.IV.w_add line 97
  40. lemma OAI.GeneralMahler.Cert.IV.w_neg line 98
  41. lemma OAI.GeneralMahler.Cert.IV.w0 line 99
  42. lemma OAI.GeneralMahler.Cert.IV.mc line 101
  43. lemma OAI.GeneralMahler.Cert.IV.nc line 105
  44. lemma OAI.GeneralMahler.Cert.IV.mz line 106
  45. lemma OAI.GeneralMahler.Cert.IV.mo line 107
  46. lemma OAI.GeneralMahler.Cert.IV.madd line 109
  47. lemma OAI.GeneralMahler.Cert.IV.mneg line 116
  48. lemma OAI.GeneralMahler.Cert.IV.msub line 121
  49. lemma OAI.GeneralMahler.Cert.IV.lower_div line 123
  50. lemma OAI.GeneralMahler.Cert.IV.upper_div line 127
  51. lemma OAI.GeneralMahler.Cert.IV.product_box line 133
  52. lemma OAI.GeneralMahler.Cert.IV.wdn line 148
  53. lemma OAI.GeneralMahler.Cert.IV.wup line 150
  54. lemma OAI.GeneralMahler.Cert.IV.wm line 152
  55. lemma OAI.GeneralMahler.Cert.IV.mmul line 154
  56. lemma OAI.GeneralMahler.Cert.IV.mposInv line 169
  57. lemma OAI.GeneralMahler.Cert.IV.minv line 182
  58. lemma OAI.GeneralMahler.Cert.IV.mdiv line 195
  59. lemma OAI.GeneralMahler.Cert.IV.mpow line 196
  60. lemma OAI.GeneralMahler.Cert.IV.mle line 201
  61. lemma OAI.GeneralMahler.Cert.IV.mlt line 204
  62. lemma OAI.GeneralMahler.Cert.IV.subB line 207
  63. lemma OAI.GeneralMahler.Cert.IV.mmax line 215
  64. lemma OAI.GeneralMahler.Cert.IV.mclamp line 220
  65. lemma OAI.GeneralMahler.Cert.IV.mabs line 225
  66. lemma OAI.GeneralMahler.Cert.IV.msq line 226
  67. lemma OAI.GeneralMahler.Cert.IV.mmeet line 229
  68. lemma OAI.GeneralMahler.Cert.IV.span_conv line 237