OAI/Analysis/PlanarPacking/Intervals.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

Integer interval arithmetic for a planar Fourier certificate

Real and complex interval operations with precision 10^30, including checked Taylor bounds for the complex exponential and rational Fourier kernels.

  1. def OAI.SharpPlanar.IntegerIntervals.precision line 22
  2. lemma OAI.SharpPlanar.IntegerIntervals.precision_pos line 23
  3. structure OAI.SharpPlanar.IntegerIntervals.RBox line 25
  4. structure OAI.SharpPlanar.IntegerIntervals.CBox line 29
  5. def OAI.SharpPlanar.IntegerIntervals.RBox.Contains line 34
  6. def OAI.SharpPlanar.IntegerIntervals.CBox.Contains line 36
  7. def OAI.SharpPlanar.IntegerIntervals.mulLo line 38
  8. def OAI.SharpPlanar.IntegerIntervals.mulHi line 40
  9. def OAI.SharpPlanar.IntegerIntervals.RBox.AddCheck line 43
  10. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 44) line 44
  11. def OAI.SharpPlanar.IntegerIntervals.RBox.MulCheck line 45
  12. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 46) line 46
  13. def OAI.SharpPlanar.IntegerIntervals.CBox.AddCheck line 48
  14. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 49) line 49
  15. def OAI.SharpPlanar.IntegerIntervals.CBox.MulCheck line 50
  16. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 55) line 55
  17. lemma OAI.SharpPlanar.IntegerIntervals.between_mul line 57
  18. lemma OAI.SharpPlanar.IntegerIntervals.real_mul_bounds line 65
  19. lemma OAI.SharpPlanar.IntegerIntervals.mul_bounds line 74
  20. lemma OAI.SharpPlanar.IntegerIntervals.RBox.add_contains line 79
  21. lemma OAI.SharpPlanar.IntegerIntervals.RBox.mul_contains line 85
  22. lemma OAI.SharpPlanar.IntegerIntervals.CBox.add_contains line 94
  23. lemma OAI.SharpPlanar.IntegerIntervals.CBox.mul_contains line 97
  24. def OAI.SharpPlanar.IntegerIntervals.RBox.RatCheck line 122
  25. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 124) line 124
  26. lemma OAI.SharpPlanar.IntegerIntervals.RBox.rat_contains line 125
  27. def OAI.SharpPlanar.IntegerIntervals.CBox.RatCheck line 134
  28. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 136) line 136
  29. lemma OAI.SharpPlanar.IntegerIntervals.CBox.rat_contains line 138
  30. def OAI.SharpPlanar.IntegerIntervals.RBox.neg line 144
  31. def OAI.SharpPlanar.IntegerIntervals.CBox.neg line 145
  32. lemma OAI.SharpPlanar.IntegerIntervals.RBox.neg_contains line 146
  33. lemma OAI.SharpPlanar.IntegerIntervals.CBox.neg_contains line 148
  34. def OAI.SharpPlanar.IntegerIntervals.RBox.ScaleCheck line 151
  35. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 153) line 153
  36. lemma OAI.SharpPlanar.IntegerIntervals.RBox.scale_contains line 155
  37. def OAI.SharpPlanar.IntegerIntervals.CBox.ScaleCheck line 169
  38. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 171) line 171
  39. lemma OAI.SharpPlanar.IntegerIntervals.CBox.scale_contains line 172
  40. def OAI.SharpPlanar.IntegerIntervals.RBox.InvCheck line 178
  41. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 180) line 180
  42. lemma OAI.SharpPlanar.IntegerIntervals.RBox.inv_contains line 181
  43. def OAI.SharpPlanar.IntegerIntervals.RBox.bound line 199
  44. lemma OAI.SharpPlanar.IntegerIntervals.RBox.abs_bound line 200
  45. def OAI.SharpPlanar.IntegerIntervals.CBox.NormCheck line 211
  46. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 212) line 212
  47. lemma OAI.SharpPlanar.IntegerIntervals.CBox.norm_le line 213
  48. def OAI.SharpPlanar.IntegerIntervals.CBox.WidenCheck line 222
  49. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 225) line 225
  50. lemma OAI.SharpPlanar.IntegerIntervals.CBox.widen_contains line 227
  51. def OAI.SharpPlanar.IntegerIntervals.expHorner line 246
  52. lemma OAI.SharpPlanar.IntegerIntervals.expHorner_eq line 250
  53. lemma OAI.SharpPlanar.IntegerIntervals.exp_small_error line 265
  54. lemma OAI.SharpPlanar.IntegerIntervals.horner_step line 278
  55. lemma OAI.SharpPlanar.IntegerIntervals.exp_from_horner line 285
  56. lemma OAI.SharpPlanar.IntegerIntervals.power_mul line 291
  57. lemma OAI.SharpPlanar.IntegerIntervals.CBox.inv_checked line 296
  58. def OAI.SharpPlanar.IntegerIntervals.piBounds line 308
  59. lemma OAI.SharpPlanar.IntegerIntervals.piBounds_contains line 309
  60. def OAI.SharpPlanar.IntegerIntervals.bBounds line 315
  61. lemma OAI.SharpPlanar.IntegerIntervals.bBounds_contains line 316
  62. lemma OAI.SharpPlanar.IntegerIntervals.CBox.ofReal_contains line 322
  63. lemma OAI.SharpPlanar.IntegerIntervals.floor_mul_le line 331
  64. lemma OAI.SharpPlanar.IntegerIntervals.le_ceil_mul line 333
  65. def OAI.SharpPlanar.IntegerIntervals.RBox.rat line 337
  66. def OAI.SharpPlanar.IntegerIntervals.CBox.rat line 338
  67. def OAI.SharpPlanar.IntegerIntervals.RBox.add line 339
  68. def OAI.SharpPlanar.IntegerIntervals.CBox.add line 340
  69. def OAI.SharpPlanar.IntegerIntervals.RBox.mul line 341
  70. def OAI.SharpPlanar.IntegerIntervals.CBox.mul line 343
  71. def OAI.SharpPlanar.IntegerIntervals.RBox.scale line 348
  72. def OAI.SharpPlanar.IntegerIntervals.CBox.scale line 350
  73. def OAI.SharpPlanar.IntegerIntervals.RBox.inv line 351
  74. def OAI.SharpPlanar.IntegerIntervals.CBox.inv line 352
  75. def OAI.SharpPlanar.IntegerIntervals.CBox.widen line 356
  76. def OAI.SharpPlanar.IntegerIntervals.CBox.horner line 358
  77. def OAI.SharpPlanar.IntegerIntervals.CBox.squareIter line 361
  78. def OAI.SharpPlanar.IntegerIntervals.CBox.exp line 364
  79. lemma OAI.SharpPlanar.IntegerIntervals.RBox.rat_check line 367
  80. lemma OAI.SharpPlanar.IntegerIntervals.CBox.rat_check line 369
  81. lemma OAI.SharpPlanar.IntegerIntervals.RBox.add_check line 372
  82. lemma OAI.SharpPlanar.IntegerIntervals.CBox.add_check line 373
  83. lemma OAI.SharpPlanar.IntegerIntervals.RBox.mul_check line 375
  84. lemma OAI.SharpPlanar.IntegerIntervals.CBox.mul_check line 377
  85. lemma OAI.SharpPlanar.IntegerIntervals.RBox.scale_check line 380
  86. lemma OAI.SharpPlanar.IntegerIntervals.CBox.scale_check line 382
  87. lemma OAI.SharpPlanar.IntegerIntervals.CBox.widen_check line 384
  88. lemma OAI.SharpPlanar.IntegerIntervals.RBox.contains_rat line 387
  89. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_rat line 389
  90. lemma OAI.SharpPlanar.IntegerIntervals.RBox.contains_add line 392
  91. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_add line 394
  92. lemma OAI.SharpPlanar.IntegerIntervals.RBox.contains_mul line 396
  93. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_mul line 398
  94. lemma OAI.SharpPlanar.IntegerIntervals.RBox.contains_scale line 400
  95. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_scale line 402
  96. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_horner line 404
  97. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_squareIter line 414
  98. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_exp line 421
  99. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_inv line 434
  100. def OAI.SharpPlanar.IntegerIntervals.CBox.powBin line 441
  101. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_powBin line 448
  102. lemma OAI.SharpPlanar.IntegerIntervals.RBox.lower_bound line 471
  103. lemma OAI.SharpPlanar.IntegerIntervals.RBox.upper_bound line 478
  104. def OAI.SharpPlanar.IntegerIntervals.pointLambda line 491

    Source comment

    These are exactly lambda,z from fourier:frequencies, restricted to real t.
    noncomputable def pointLambda (t : ℝ) : ℂ :=
…
  105. def OAI.SharpPlanar.IntegerIntervals.pointZ line 493
  106. structure OAI.SharpPlanar.IntegerIntervals.PointBox line 496
  107. def OAI.SharpPlanar.IntegerIntervals.rcast line 504
  108. def OAI.SharpPlanar.IntegerIntervals.piI line 505
  109. def OAI.SharpPlanar.IntegerIntervals.denBox line 506
  110. def OAI.SharpPlanar.IntegerIntervals.lamDenBox line 507
  111. def OAI.SharpPlanar.IntegerIntervals.lamBox line 508
  112. def OAI.SharpPlanar.IntegerIntervals.zBox line 509
  113. def OAI.SharpPlanar.IntegerIntervals.directArgBox line 510
  114. def OAI.SharpPlanar.IntegerIntervals.quarterArgBox line 511
  115. def OAI.SharpPlanar.IntegerIntervals.CBox.GoodInv line 513
  116. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 516) line 516
  117. def OAI.SharpPlanar.IntegerIntervals.PointBox.Check line 518
  118. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 522) line 522
  119. def OAI.SharpPlanar.IntegerIntervals.PointBox.calc line 524
  120. def OAI.SharpPlanar.IntegerIntervals.PointBox.Contains line 527
  121. lemma OAI.SharpPlanar.IntegerIntervals.rcast_contains line 532
  122. lemma OAI.SharpPlanar.IntegerIntervals.piI_contains line 534
  123. lemma OAI.SharpPlanar.IntegerIntervals.denBox_contains line 538
  124. lemma OAI.SharpPlanar.IntegerIntervals.lamDenBox_contains line 543
  125. lemma OAI.SharpPlanar.IntegerIntervals.lamBox_contains line 546
  126. lemma OAI.SharpPlanar.IntegerIntervals.zBox_contains line 552
  127. lemma OAI.SharpPlanar.IntegerIntervals.directArgBox_contains line 562
  128. lemma OAI.SharpPlanar.IntegerIntervals.quarterArgBox_contains line 565
  129. lemma OAI.SharpPlanar.IntegerIntervals.PointBox.calc_contains line 572