OAI/Geometry/UnitDistances/Quantization.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarUnitDistances.TripleCoupling.Outcome line 11
  2. def OAI.PlanarUnitDistances.TripleCoupling.law line 13
  3. def OAI.PlanarUnitDistances.TripleCoupling.point line 16
  4. def OAI.PlanarUnitDistances.TripleCoupling.prediction line 17
  5. def OAI.PlanarUnitDistances.TripleCoupling.neighbor line 18
  6. lemma OAI.PlanarUnitDistances.TripleCoupling.first line 21
  7. lemma OAI.PlanarUnitDistances.TripleCoupling.predicted_point line 25
  8. lemma OAI.PlanarUnitDistances.TripleCoupling.edge line 32
  9. lemma OAI.PlanarUnitDistances.TripleCoupling.center line 38
  10. lemma OAI.PlanarUnitDistances.TripleCoupling.predicted_pair line 43
  11. lemma OAI.PlanarUnitDistances.TripleCoupling.point_prediction line 51
  12. lemma OAI.PlanarUnitDistances.TripleCoupling.two_centers line 59
  13. lemma OAI.PlanarUnitDistances.TripleCoupling.predicted_diagonal line 64
  14. lemma OAI.PlanarUnitDistances.TripleCoupling.center_diagonal line 72
  15. def OAI.PlanarUnitDistances.FiniteQuantization.radius line 88
  16. abbrev OAI.PlanarUnitDistances.FiniteQuantization.Cell line 89
  17. abbrev OAI.PlanarUnitDistances.FiniteQuantization.Axis line 90
  18. abbrev OAI.PlanarUnitDistances.FiniteQuantization.Alphabet line 91
  19. def OAI.PlanarUnitDistances.FiniteQuantization.axis line 93
  20. def OAI.PlanarUnitDistances.FiniteQuantization.code line 97
  21. lemma OAI.PlanarUnitDistances.FiniteQuantization.bounded_cell line 100
  22. lemma OAI.PlanarUnitDistances.FiniteQuantization.axis_close line 118
  23. lemma OAI.PlanarUnitDistances.FiniteQuantization.complex_close line 138
  24. theorem OAI.PlanarUnitDistances.FiniteQuantization.same_code_close line 153
  25. lemma OAI.PlanarUnitDistances.FiniteQuantization.alphabet_card line 159
  26. lemma OAI.PlanarUnitDistances.BoundedScaleGeometry.inverse_difference_det line 170
  27. lemma OAI.PlanarUnitDistances.BoundedScaleGeometry.cramer_identity line 177
  28. lemma OAI.PlanarUnitDistances.BoundedScaleGeometry.quantized_edge_error line 186
  29. lemma OAI.PlanarUnitDistances.BoundedScaleGeometry.square_grid_edge_error line 207
  30. theorem OAI.PlanarUnitDistances.BoundedScaleGeometry.no_separated_approximate_point line 227
  31. lemma OAI.PlanarUnitDistances.QuantizedContradiction.difference_equation line 280
  32. theorem OAI.PlanarUnitDistances.QuantizedContradiction.impossible line 286
  33. abbrev OAI.PlanarUnitDistances.BoundedGeometricCover.BigIndex line 326
  34. abbrev OAI.PlanarUnitDistances.BoundedGeometricCover.SmallIndex line 327
  35. def OAI.PlanarUnitDistances.BoundedGeometricCover.big line 329
  36. def OAI.PlanarUnitDistances.BoundedGeometricCover.small line 336
  37. def OAI.PlanarUnitDistances.BoundedGeometricCover.accept line 340
  38. def OAI.PlanarUnitDistances.BoundedGeometricCover.bad line 344
  39. theorem OAI.PlanarUnitDistances.BoundedGeometricCover.cover line 353
  40. lemma OAI.PlanarUnitDistances.BoundedProbabilities.height_sub line 406
  41. lemma OAI.PlanarUnitDistances.BoundedProbabilities.big_mean line 412
  42. lemma OAI.PlanarUnitDistances.BoundedProbabilities.small_mean line 430
  43. lemma OAI.PlanarUnitDistances.BoundedProbabilities.large_bound line 450
  44. lemma OAI.PlanarUnitDistances.BoundedProbabilities.small_bound line 462
  45. lemma OAI.PlanarUnitDistances.BoundedProbabilities.point_bound line 473
  46. lemma OAI.PlanarUnitDistances.BoundedProbabilities.centers_bound line 489
  47. lemma OAI.PlanarUnitDistances.BoundedProbabilities.nonedge_zero line 513
  48. lemma OAI.PlanarUnitDistances.BoundedProbabilities.mixture_col line 541
  49. def OAI.PlanarUnitDistances.BoundedProbabilities.failure line 546
  50. lemma OAI.PlanarUnitDistances.BoundedProbabilities.failure_bound line 552