OAI/Geometry/UnitDistances/Preparation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarUnitDistances.ActualScoreBook.ActualBook line 13
  2. def OAI.PlanarUnitDistances.ActualScoreBook.mass line 16
  3. def OAI.PlanarUnitDistances.ActualScoreBook.make line 18
  4. lemma OAI.PlanarUnitDistances.ActualScoreBook.average line 34
  5. lemma OAI.PlanarUnitDistances.ActualScoreBook.active_point line 45
  6. lemma OAI.PlanarUnitDistances.ActualScoreBook.point_activity line 64
  7. lemma OAI.PlanarUnitDistances.ActualScoreBook.active_center line 77
  8. lemma OAI.PlanarUnitDistances.ActualScoreBook.center_activity line 96
  9. lemma OAI.PlanarUnitDistances.FiniteLaw.fiber_average line 117
  10. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_average line 123
  11. lemma OAI.PlanarUnitDistances.GraphPrediction.mixture_col line 136
  12. lemma OAI.PlanarUnitDistances.GraphPrediction.prediction_eq line 142
  13. lemma OAI.PlanarUnitDistances.GraphPrediction.actual_error line 154
  14. theorem OAI.PlanarUnitDistances.GraphPrediction.exists_common_history line 171
  15. def OAI.PlanarUnitDistances.LawStable.majority line 209
  16. def OAI.PlanarUnitDistances.LawStable.minorityFrequency line 210
  17. lemma OAI.PlanarUnitDistances.LawStable.minority_le_half line 212
  18. lemma OAI.PlanarUnitDistances.LawStable.minority_event line 217
  19. lemma OAI.PlanarUnitDistances.LawStable.majority_error line 230
  20. lemma OAI.PlanarUnitDistances.LawStable.majority_le_variation line 242
  21. theorem OAI.PlanarUnitDistances.LawStable.stable line 254
  22. theorem OAI.PlanarUnitDistances.SelectedBook.constants line 315
  23. theorem OAI.PlanarUnitDistances.PreparedSelection.constants line 363
  24. theorem OAI.PlanarUnitDistances.LevelStates.exists_bounded_states_support line 413
  25. lemma OAI.PlanarUnitDistances.ActualPreparation.scale_le_mass line 435
  26. lemma OAI.PlanarUnitDistances.ActualPreparation.frequency line 444
  27. lemma OAI.PlanarUnitDistances.ActualPreparation.inconsistency line 459
  28. theorem OAI.PlanarUnitDistances.ActualPreparation.states line 472
  29. theorem OAI.PlanarUnitDistances.ActualPrepared.constants line 508