OAI/NumberTheory/GaussianMoat/SignedGeometry.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.cubeEquiv line 11
  2. def OAI.GaussianMoat.cubeSignEquiv line 19
  3. def OAI.GaussianMoat.signDist line 23
  4. theorem OAI.GaussianMoat.cubeEquiv_dist line 27
  5. theorem OAI.GaussianMoat.cubeSignEquiv_dist line 41
  6. theorem OAI.GaussianMoat.signMeasure_real_singleton line 50
  7. theorem OAI.GaussianMoat.signMeasure_real_set line 57
  8. theorem OAI.GaussianMoat.cubeSignEquiv_measure line 68
  9. def OAI.GaussianMoat.SplitSieve.extendSigns line 78
  10. theorem OAI.GaussianMoat.SplitSieve.extendSigns_mem line 82
  11. def OAI.GaussianMoat.SplitSieve.signedProduct line 86
  12. theorem OAI.GaussianMoat.SplitSieve.line_witness_log_lower line 89
  13. def OAI.GaussianMoat.SplitSieve.lineEvent line 128
  14. theorem OAI.GaussianMoat.SplitSieve.line_event_tail line 132
  15. def OAI.GaussianMoat.SplitSieve.commonProduct line 149
  16. theorem OAI.GaussianMoat.SplitSieve.commonProduct_dvd_left line 153
  17. theorem OAI.GaussianMoat.SplitSieve.commonProduct_comm line 158
  18. theorem OAI.GaussianMoat.SplitSieve.commonProduct_dvd_right line 168
  19. theorem OAI.GaussianMoat.SplitSieve.signDist_eq_card line 174
  20. theorem OAI.GaussianMoat.SplitSieve.period_le_common_norm line 184
  21. theorem OAI.GaussianMoat.SplitSieve.near_witnesses_collinear line 209
  22. theorem OAI.GaussianMoat.determinant_zero_trans line 221
  23. theorem OAI.GaussianMoat.determinant_self line 236
  24. theorem OAI.GaussianMoat.determinant_swap line 240
  25. def OAI.GaussianMoat.witnessLine line 244
  26. theorem OAI.GaussianMoat.witnessLine_eq line 246
  27. def OAI.GaussianMoat.SplitSieve.badSign line 254
  28. def OAI.GaussianMoat.SplitSieve.badWitness line 257
  29. theorem OAI.GaussianMoat.SplitSieve.badWitness_spec line 260
  30. def OAI.GaussianMoat.SplitSieve.badLines line 265
  31. instance OAI.GaussianMoat.SplitSieve.badLines_finite line 268
  32. theorem OAI.GaussianMoat.SplitSieve.badLine_primitive line 273
  33. def OAI.GaussianMoat.SplitSieve.lineClass line 286
  34. theorem OAI.GaussianMoat.SplitSieve.badSign_iff_class line 290
  35. theorem OAI.GaussianMoat.SplitSieve.lineClass_subset_event line 298
  36. theorem OAI.GaussianMoat.SplitSieve.lineClasses_separated line 308
  37. theorem OAI.GaussianMoat.cubeSize_exists_le_sum line 328
  38. theorem OAI.GaussianMoat.SplitSieve.signed_region_bound line 345
  39. theorem OAI.GaussianMoat.SplitSieve.signed_region_exp_bound line 396
  40. def OAI.GaussianMoat.orientedRectangle line 433
  41. theorem OAI.GaussianMoat.rectangle_norm_bound line 436
  42. theorem OAI.GaussianMoat.determinant_rotated line 450
  43. theorem OAI.GaussianMoat.rectangle_determinant_bound line 462
  44. theorem OAI.GaussianMoat.rectangle_cube_growth line 473
  45. theorem OAI.GaussianMoat.rectangle_linear_large line 517
  46. theorem OAI.GaussianMoat.rectangle_log_small line 523
  47. theorem OAI.GaussianMoat.rectangle_log_excess line 540
  48. theorem OAI.GaussianMoat.rectangle_hoeffding_exponent line 549
  49. theorem OAI.GaussianMoat.SplitSieve.log_period line 562
  50. def OAI.GaussianMoat.SplitSieve.logVariance line 571
  51. theorem OAI.GaussianMoat.SplitSieve.logVariance_pos line 574
  52. theorem OAI.GaussianMoat.SplitSieve.logVariance_le line 585
  53. theorem OAI.GaussianMoat.SplitSieve.signed_rectangle line 601