OAI/Geometry/UnitDistances/Slots.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.LevelGeometry.allowance line 11
  2. lemma OAI.PlanarUnitDistances.LevelGeometry.allowance_nonneg line 14
  3. lemma OAI.PlanarUnitDistances.LevelGeometry.first_bound line 17
  4. lemma OAI.PlanarUnitDistances.LevelGeometry.second_bound line 34
  5. lemma OAI.PlanarUnitDistances.LevelGeometry.first_log_bound line 51
  6. lemma OAI.PlanarUnitDistances.LevelGeometry.second_log_bound line 57
  7. lemma OAI.PlanarUnitDistances.LevelGeometry.thickness_nonneg line 64
  8. lemma OAI.PlanarUnitDistances.LevelGeometry.opposite_log line 74
  9. theorem OAI.PlanarUnitDistances.LevelGeometry.positive_flanks line 84
  10. def OAI.PlanarUnitDistances.BudgetIntervals.overlap line 131
  11. lemma OAI.PlanarUnitDistances.BudgetIntervals.overlap_nonneg line 133
  12. lemma OAI.PlanarUnitDistances.BudgetIntervals.overlap_le_length line 135
  13. lemma OAI.PlanarUnitDistances.BudgetIntervals.overlap_pos_iff line 141
  14. lemma OAI.PlanarUnitDistances.BudgetIntervals.disjoint_overlap_sum line 145
  15. theorem OAI.PlanarUnitDistances.BudgetIntervals.central_envelope line 164
  16. def OAI.PlanarUnitDistances.BudgetIntervals.tail line 195
  17. def OAI.PlanarUnitDistances.BudgetIntervals.interiorMass line 198
  18. lemma OAI.PlanarUnitDistances.BudgetIntervals.interiorMass_nonneg line 201
  19. theorem OAI.PlanarUnitDistances.BudgetIntervals.interior_mass_le line 205
  20. lemma OAI.PlanarUnitDistances.BudgetIntervals.overlap_eq_volume line 256
  21. lemma OAI.PlanarUnitDistances.BudgetIntervals.sorted_interior line 261
  22. lemma OAI.PlanarUnitDistances.BudgetIntervals.pair_interior_mass line 272
  23. theorem OAI.PlanarUnitDistances.BudgetIntervals.expected_central_envelope line 285
  24. def OAI.PlanarUnitDistances.PlaceScore.common line 324
  25. def OAI.PlanarUnitDistances.PlaceScore.reward line 326
  26. lemma OAI.PlanarUnitDistances.PlaceScore.coefficient_bounds line 330
  27. lemma OAI.PlanarUnitDistances.PlaceScore.reward_bounds line 333
  28. lemma OAI.PlanarUnitDistances.PlaceScore.reward_true_zero line 337
  29. lemma OAI.PlanarUnitDistances.PlaceScore.reward_false_zero line 341
  30. def OAI.PlanarUnitDistances.PlaceScore.ind line 346
  31. lemma OAI.PlanarUnitDistances.PlaceScore.ind_nonneg line 347
  32. lemma OAI.PlanarUnitDistances.PlaceScore.ind_le_one line 349
  33. lemma OAI.PlanarUnitDistances.PlaceScore.ind_Icc_integrable line 351
  34. lemma OAI.PlanarUnitDistances.PlaceScore.ind_Icc_integral line 353
  35. lemma OAI.PlanarUnitDistances.PlaceScore.ind_inter_integrable line 357
  36. lemma OAI.PlanarUnitDistances.PlaceScore.ind_inter_integral line 360
  37. def OAI.PlanarUnitDistances.PlaceScore.cap line 365
  38. lemma OAI.PlanarUnitDistances.PlaceScore.low_cap line 369
  39. lemma OAI.PlanarUnitDistances.PlaceScore.high_cap line 388
  40. lemma OAI.PlanarUnitDistances.PlaceScore.middle_reward line 401
  41. lemma OAI.PlanarUnitDistances.PlaceScore.middle_cap line 407
  42. theorem OAI.PlanarUnitDistances.PlaceScore.positive_budget line 452
  43. def OAI.PlanarUnitDistances.LevelScores.minority line 502
  44. def OAI.PlanarUnitDistances.LevelScores.positive line 504
  45. def OAI.PlanarUnitDistances.LevelScores.score line 509
  46. lemma OAI.PlanarUnitDistances.LevelScores.positive_bounds line 512
  47. lemma OAI.PlanarUnitDistances.LevelScores.score_bounds line 524
  48. lemma OAI.PlanarUnitDistances.LevelScores.minority_reward line 532
  49. lemma OAI.PlanarUnitDistances.LevelScores.positive_le_rewards line 545
  50. lemma OAI.PlanarUnitDistances.LevelScores.rare_score line 581
  51. lemma OAI.PlanarUnitDistances.LevelScores.damaged_score line 585
  52. theorem OAI.PlanarUnitDistances.LevelSlotGeometry.positive_le_cap line 599
  53. def OAI.PlanarUnitDistances.RareRows.frequency line 644
  54. def OAI.PlanarUnitDistances.RareRows.scoreP line 645
  55. def OAI.PlanarUnitDistances.RareRows.scoreQ line 650
  56. lemma OAI.PlanarUnitDistances.RareRows.common_slot line 656
  57. lemma OAI.PlanarUnitDistances.RareRows.common_P line 662
  58. lemma OAI.PlanarUnitDistances.RareRows.common_Q line 671
  59. lemma OAI.PlanarUnitDistances.RareRows.consistency_symm line 681
  60. theorem OAI.PlanarUnitDistances.RareRows.rare_P line 684
  61. theorem OAI.PlanarUnitDistances.RareRows.rare_Q line 712
  62. lemma OAI.PlanarUnitDistances.RareRows.scoreP_lower line 749
  63. lemma OAI.PlanarUnitDistances.RareRows.scoreQ_lower line 756
  64. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_avg_original line 771
  65. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_event_original line 775
  66. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_left_event line 778
  67. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_right_event line 782
  68. def OAI.PlanarUnitDistances.RareRows.scoreT line 795
  69. theorem OAI.PlanarUnitDistances.RareRows.rare_T line 799
  70. lemma OAI.PlanarUnitDistances.RareRows.common_T line 811
  71. lemma OAI.PlanarUnitDistances.RareRows.scoreT_lower line 819