OAI/Geometry/UnitDistances/Scale.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.FiniteAcceptance.feature line 12
  2. def OAI.PlanarUnitDistances.FiniteAcceptance.test line 13
  3. lemma OAI.PlanarUnitDistances.FiniteAcceptance.feature_inner line 16
  4. lemma OAI.PlanarUnitDistances.FiniteAcceptance.norm_feature line 22
  5. lemma OAI.PlanarUnitDistances.FiniteAcceptance.norm_test line 30
  6. def OAI.PlanarUnitDistances.FiniteAcceptance.actual line 44
  7. def OAI.PlanarUnitDistances.FiniteAcceptance.predicted line 48
  8. lemma OAI.PlanarUnitDistances.FiniteAcceptance.discrepancy_eq line 52
  9. lemma OAI.PlanarUnitDistances.FiniteAcceptance.actual_one line 66
  10. theorem OAI.PlanarUnitDistances.FiniteAcceptance.exists_history line 84
  11. theorem OAI.PlanarUnitDistances.BoundedScaleFinite.obstruction line 123
  12. def OAI.PlanarUnitDistances.BoundedScaleFinite.information line 163
  13. theorem OAI.PlanarUnitDistances.BoundedScaleFinite.exists_small_failure line 168
  14. theorem OAI.PlanarUnitDistances.BoundedConstants.exists_cutoffs line 201
  15. theorem OAI.PlanarUnitDistances.BoundedScaleUniform.obstruction line 243
  16. def OAI.PlanarUnitDistances.LogHistory.length line 283
  17. lemma OAI.PlanarUnitDistances.LogHistory.length_pos line 285
  18. lemma OAI.PlanarUnitDistances.LogHistory.bounds line 287
  19. lemma OAI.PlanarUnitDistances.LogHistory.ratio_limit line 315
  20. lemma OAI.PlanarUnitDistances.LogHistory.density_limit line 340
  21. lemma OAI.PlanarUnitDistances.BoundedScaleExclusion.information_nonneg line 365
  22. theorem OAI.PlanarUnitDistances.BoundedScaleExclusion.no_sequence line 377
  23. theorem OAI.PlanarUnitDistances.ScaleDivergence.not_bounded line 427
  24. theorem OAI.PlanarUnitDistances.ScaleDivergence.tends_to_infinity line 461
  25. def OAI.PlanarUnitDistances.IncidenceScale.graph line 504
  26. def OAI.PlanarUnitDistances.IncidenceScale.model line 505
  27. lemma OAI.PlanarUnitDistances.IncidenceScale.positive line 507
  28. lemma OAI.PlanarUnitDistances.IncidenceScale.positiveQ line 510
  29. lemma OAI.PlanarUnitDistances.IncidenceScale.support line 513
  30. lemma OAI.PlanarUnitDistances.IncidenceScale.point_bound line 518
  31. lemma OAI.PlanarUnitDistances.IncidenceScale.row_bound line 521
  32. lemma OAI.PlanarUnitDistances.IncidenceScale.information_eq line 530
  33. lemma OAI.PlanarUnitDistances.IncidenceScale.label_control line 535
  34. def OAI.PlanarUnitDistances.IncidenceScale.scale line 554
  35. theorem OAI.PlanarUnitDistances.IncidenceScale.scale_limit line 557
  36. lemma OAI.PlanarUnitDistances.CommonTemplate.bad_good_indicator line 592
  37. def OAI.PlanarUnitDistances.CommonTemplate.templateLaw line 599
  38. def OAI.PlanarUnitDistances.CommonTemplate.predictionError line 602
  39. def OAI.PlanarUnitDistances.CommonTemplate.samplingError line 605
  40. lemma OAI.PlanarUnitDistances.CommonTemplate.candidate_miss_mean line 608
  41. lemma OAI.PlanarUnitDistances.CommonTemplate.failure_mean line 632
  42. theorem OAI.PlanarUnitDistances.CommonTemplate.common_score line 644