OAI/Geometry/UnitDistances/Predictions.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.FiniteLaw.uniform line 11
  2. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_avg line 16
  3. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_equiv line 20
  4. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_pair line 24
  5. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_eval line 31
  6. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_eval_two line 41
  7. lemma OAI.PlanarUnitDistances.FiniteLaw.uniform_collision line 55
  8. def OAI.PlanarUnitDistances.FiniteLaw.Law.pmf line 67
  9. lemma OAI.PlanarUnitDistances.FiniteLaw.Law.pmf_apply line 70
  10. lemma OAI.PlanarUnitDistances.FiniteLaw.integral_pmf line 72
  11. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.arch_average_posLog_le line 88
  12. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.large_embedding_tail line 95
  13. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.small_embedding_tail line 111
  14. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.random_large_embedding_tail line 124
  15. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.random_small_embedding_tail line 134
  16. abbrev OAI.PlanarUnitDistances.EmbeddingTails.Embeddings line 154
  17. instance OAI.PlanarUnitDistances.EmbeddingTails.(instance at line 156) line 156
  18. lemma OAI.PlanarUnitDistances.EmbeddingTails.large line 159
  19. lemma OAI.PlanarUnitDistances.EmbeddingTails.small line 174
  20. lemma OAI.PlanarUnitDistances.EmbeddingTails.large_family line 187
  21. lemma OAI.PlanarUnitDistances.EmbeddingTails.small_family line 195
  22. lemma OAI.PlanarUnitDistances.FiniteLaw.exists_good line 212
  23. lemma OAI.PlanarUnitDistances.FiniteLaw.exists_all_good line 225
  24. lemma OAI.PlanarUnitDistances.TemplateCollision.collision_eq line 238
  25. lemma OAI.PlanarUnitDistances.TemplateCollision.atom_le_one line 242
  26. lemma OAI.PlanarUnitDistances.TemplateCollision.slice_collision line 245
  27. theorem OAI.PlanarUnitDistances.TemplateCollision.weighted line 264
  28. lemma OAI.PlanarUnitDistances.TemplateCollision.row_weighted line 283
  29. lemma OAI.PlanarUnitDistances.FiniteLaw.event_and_lower line 309
  30. lemma OAI.PlanarUnitDistances.FiniteLaw.event_disjoint_union line 314
  31. def OAI.PlanarUnitDistances.FiniteMarginalScore.collision line 331
  32. def OAI.PlanarUnitDistances.FiniteMarginalScore.tau line 334
  33. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.collision_nonneg line 336
  34. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.collision_atom line 338
  35. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.collision_two line 342
  36. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.collision_one_linear line 348
  37. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.collision_two_linear line 352
  38. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_lower line 359
  39. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_row line 362
  40. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_col line 368
  41. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_cross line 374
  42. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_atom line 384
  43. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.tau_two line 392
  44. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.two_cross_mass line 407
  45. lemma OAI.PlanarUnitDistances.FiniteMarginalScore.three_cross_mass line 413
  46. theorem OAI.PlanarUnitDistances.FiniteMarginalScore.second_slice line 421
  47. def OAI.PlanarUnitDistances.PredictionCoupling.coupling line 536
  48. lemma OAI.PlanarUnitDistances.PredictionCoupling.first line 539
  49. lemma OAI.PlanarUnitDistances.PredictionCoupling.second line 544
  50. lemma OAI.PlanarUnitDistances.PredictionCoupling.cond_diagonal line 550
  51. theorem OAI.PlanarUnitDistances.PredictionCoupling.diagonal line 566
  52. lemma OAI.PlanarUnitDistances.PredictionCoupling.coordinate_collision line 574
  53. lemma OAI.PlanarUnitDistances.PredictionCoupling.collision_push line 585
  54. lemma OAI.PlanarUnitDistances.PredictionCoupling.tau_pair line 590
  55. theorem OAI.PlanarUnitDistances.PredictionCoupling.tau_eq line 598
  56. abbrev OAI.PlanarUnitDistances.HashFeatures.Index line 614
  57. abbrev OAI.PlanarUnitDistances.HashFeatures.V line 615
  58. def OAI.PlanarUnitDistances.HashFeatures.vector line 617
  59. lemma OAI.PlanarUnitDistances.HashFeatures.single_inner line 622
  60. lemma OAI.PlanarUnitDistances.HashFeatures.inner_vector line 629
  61. lemma OAI.PlanarUnitDistances.HashFeatures.norm_vector_sq line 640
  62. lemma OAI.PlanarUnitDistances.HashFeatures.norm_feature line 645
  63. lemma OAI.PlanarUnitDistances.HashFeatures.norm_test line 649
  64. lemma OAI.PlanarUnitDistances.HashFeatures.strict_cross_inner line 654
  65. lemma OAI.PlanarUnitDistances.HashFeatures.prediction_constant line 670
  66. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_comm line 683
  67. lemma OAI.PlanarUnitDistances.FiniteLaw.abs_avg_le line 692
  68. abbrev OAI.PlanarUnitDistances.Hashing.Hash line 706
  69. def OAI.PlanarUnitDistances.Hashing.law line 707
  70. def OAI.PlanarUnitDistances.Hashing.state line 708
  71. def OAI.PlanarUnitDistances.Hashing.indicator line 710
  72. lemma OAI.PlanarUnitDistances.Hashing.error_pointwise line 713
  73. lemma OAI.PlanarUnitDistances.Hashing.coord_error line 723
  74. lemma OAI.PlanarUnitDistances.Hashing.error_bound line 732
  75. lemma OAI.PlanarUnitDistances.Hashing.averaged_error line 748
  76. def OAI.PlanarUnitDistances.FiniteLaw.mixture line 762
  77. lemma OAI.PlanarUnitDistances.FiniteLaw.mixture_avg line 771
  78. lemma OAI.PlanarUnitDistances.FiniteLaw.abs_avg_sub_le line 776
  79. lemma OAI.PlanarUnitDistances.CrossPrediction.push_mass line 792
  80. lemma OAI.PlanarUnitDistances.CrossPrediction.posterior_cond line 801
  81. def OAI.PlanarUnitDistances.CrossPrediction.actual line 807
  82. def OAI.PlanarUnitDistances.CrossPrediction.predicted line 810
  83. lemma OAI.PlanarUnitDistances.CrossPrediction.actual_hash_error line 814
  84. lemma OAI.PlanarUnitDistances.CrossPrediction.predicted_hash_error line 828
  85. lemma OAI.PlanarUnitDistances.CrossPrediction.discrepancy_eq line 844
  86. lemma OAI.PlanarUnitDistances.CrossPrediction.hash_transfer line 865
  87. lemma OAI.PlanarUnitDistances.CrossPrediction.history_singleton line 884
  88. theorem OAI.PlanarUnitDistances.CrossPrediction.exists_cross_history line 892
  89. lemma OAI.PlanarUnitDistances.FiniteLaw.sum_real_atoms line 958
  90. def OAI.PlanarUnitDistances.FiniteLaw.fromMeasure line 962
  91. lemma OAI.PlanarUnitDistances.FiniteLaw.fromMeasure_avg line 967
  92. lemma OAI.PlanarUnitDistances.FiniteLaw.map_real_univ line 976
  93. def OAI.PlanarUnitDistances.FiniteLaw.compress line 980
  94. lemma OAI.PlanarUnitDistances.FiniteLaw.compress_avg line 984
  95. theorem OAI.PlanarUnitDistances.CrossPrediction.exists_measured_history line 1000
  96. def OAI.PlanarUnitDistances.FiniteLaw.triple line 1028
  97. def OAI.PlanarUnitDistances.FiniteLaw.entry line 1029
  98. lemma OAI.PlanarUnitDistances.FiniteLaw.triple_coordinate line 1031
  99. lemma OAI.PlanarUnitDistances.FiniteLaw.triple_pair line 1035
  100. lemma OAI.PlanarUnitDistances.FiniteLaw.triple_collision line 1041
  101. lemma OAI.PlanarUnitDistances.FiniteLaw.collision_le_atom line 1050