OAI/Geometry/UnitDistances/PredictionBudget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarUnitDistances.LevelSnapshot.snapshot_swap line 10
  2. theorem OAI.PlanarUnitDistances.ActualColumnBudget.raw line 29
  3. lemma OAI.PlanarUnitDistances.ActualColumnBudget.col_weighted line 69
  4. theorem OAI.PlanarUnitDistances.ActualColumnBudget.upper line 88
  5. theorem OAI.PlanarUnitDistances.ActualTemplateBudget.upper line 122
  6. lemma OAI.PlanarUnitDistances.PredictionPairBudget.interval_bound line 185
  7. def OAI.PlanarUnitDistances.PredictionPairBudget.score line 219
  8. lemma OAI.PlanarUnitDistances.PredictionPairBudget.score_bounds line 224
  9. lemma OAI.PlanarUnitDistances.PredictionPairBudget.measurable_score line 230
  10. lemma OAI.PlanarUnitDistances.PredictionPairBudget.pair_place line 236
  11. theorem OAI.PlanarUnitDistances.PredictionPairBudget.full_pair line 260
  12. def OAI.PlanarUnitDistances.PredictionCut.pairScore line 284
  13. lemma OAI.PlanarUnitDistances.PredictionCut.pairScore_bounds line 286
  14. lemma OAI.PlanarUnitDistances.PredictionCut.pairScore_normal line 289
  15. lemma OAI.PlanarUnitDistances.PredictionCut.cut_bound line 301
  16. theorem OAI.PlanarUnitDistances.PredictionCut.integrated line 320
  17. theorem OAI.PlanarUnitDistances.ActualPredictionBudget.upper line 375
  18. theorem OAI.PlanarUnitDistances.ActualBookUpper.point line 430
  19. theorem OAI.PlanarUnitDistances.ActualBookUpper.center line 460
  20. theorem OAI.PlanarUnitDistances.ActualBookUpper.template line 489
  21. theorem OAI.PlanarUnitDistances.ActualBookUpper.prediction line 521