OAI/Geometry/UnitDistances/Scores.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.GlobalScores.common line 11
  2. def OAI.PlanarUnitDistances.GlobalScores.bad line 14
  3. theorem OAI.PlanarUnitDistances.GlobalScores.common_lower line 16
  4. lemma OAI.PlanarUnitDistances.GlobalScores.center_score_lower line 73
  5. theorem OAI.PlanarUnitDistances.GlobalScores.center_lower line 80
  6. theorem OAI.PlanarUnitDistances.GlobalMarginal.point_lower line 121
  7. theorem OAI.PlanarUnitDistances.GlobalMarginal.scale_lower line 177
  8. structure OAI.PlanarUnitDistances.ScoreBook.Book line 216
  9. def OAI.PlanarUnitDistances.ScoreBook.Book.C line 230
  10. def OAI.PlanarUnitDistances.ScoreBook.Book.R line 231
  11. def OAI.PlanarUnitDistances.ScoreBook.Book.S line 232
  12. def OAI.PlanarUnitDistances.ScoreBook.Book.M line 233
  13. def OAI.PlanarUnitDistances.ScoreBook.Book.WC line 234
  14. def OAI.PlanarUnitDistances.ScoreBook.Book.WB line 235
  15. def OAI.PlanarUnitDistances.ScoreBook.Book.HP line 236
  16. def OAI.PlanarUnitDistances.ScoreBook.Book.HQ line 237
  17. def OAI.PlanarUnitDistances.ScoreBook.Book.J line 238
  18. def OAI.PlanarUnitDistances.ScoreBook.Book.EP line 239
  19. def OAI.PlanarUnitDistances.ScoreBook.Book.CP line 240
  20. def OAI.PlanarUnitDistances.ScoreBook.Book.CQ line 241
  21. def OAI.PlanarUnitDistances.ScoreBook.Book.CT line 242
  22. def OAI.PlanarUnitDistances.ScoreBook.Book.DP line 245
  23. def OAI.PlanarUnitDistances.ScoreBook.Book.DQ line 247
  24. def OAI.PlanarUnitDistances.ScoreBook.Book.DT line 249
  25. def OAI.PlanarUnitDistances.ScoreBook.Book.T line 251
  26. lemma OAI.PlanarUnitDistances.ScoreBook.Book.nonneg line 255
  27. lemma OAI.PlanarUnitDistances.ScoreBook.Book.CT_nonneg line 263
  28. theorem OAI.PlanarUnitDistances.ScoreBook.Book.common_lower line 266
  29. lemma OAI.PlanarUnitDistances.ScoreBook.Book.center_lower line 278
  30. lemma OAI.PlanarUnitDistances.ScoreBook.Book.point_lower line 283
  31. lemma OAI.PlanarUnitDistances.ScoreBook.Book.scale_lower line 288
  32. theorem OAI.PlanarUnitDistances.ScoreCoercivity.from_scores line 302
  33. theorem OAI.PlanarUnitDistances.ScoreCoercivity.positive line 321
  34. def OAI.PlanarUnitDistances.BookCoercivity.commonLoss line 340
  35. def OAI.PlanarUnitDistances.BookCoercivity.centerLoss line 345
  36. def OAI.PlanarUnitDistances.BookCoercivity.pointLoss line 347
  37. def OAI.PlanarUnitDistances.BookCoercivity.scaleLoss line 350
  38. def OAI.PlanarUnitDistances.BookCoercivity.loss line 352
  39. lemma OAI.PlanarUnitDistances.BookCoercivity.loss_bounds line 357
  40. theorem OAI.PlanarUnitDistances.BookCoercivity.coercivity line 381
  41. abbrev OAI.PlanarUnitDistances.LevelSnapshot.Data line 415
  42. def OAI.PlanarUnitDistances.LevelSnapshot.snapshot line 417
  43. lemma OAI.PlanarUnitDistances.LevelSnapshot.measurable_snapshot line 422
  44. lemma OAI.PlanarUnitDistances.LevelSnapshot.measurable_value line 427
  45. lemma OAI.PlanarUnitDistances.LevelSnapshot.integrable_value line 432
  46. lemma OAI.PlanarUnitDistances.LevelSnapshot.integrable_piece line 442
  47. lemma OAI.PlanarUnitDistances.LevelSnapshot.measurable_selection line 451
  48. def OAI.PlanarUnitDistances.ActualSlots.frequency line 464
  49. def OAI.PlanarUnitDistances.ActualSlots.rareException line 465
  50. def OAI.PlanarUnitDistances.ActualSlots.active line 468
  51. def OAI.PlanarUnitDistances.ActualSlots.positive line 472
  52. def OAI.PlanarUnitDistances.ActualSlots.score line 477
  53. lemma OAI.PlanarUnitDistances.ActualSlots.positive_le_active line 483
  54. lemma OAI.PlanarUnitDistances.ActualSlots.diagonal line 503
  55. lemma OAI.PlanarUnitDistances.ActualSlots.measurable_score line 509
  56. lemma OAI.PlanarUnitDistances.ActualSlots.score_integrable line 516
  57. lemma OAI.PlanarUnitDistances.ActualSlots.negative_integral line 523
  58. lemma OAI.PlanarUnitDistances.ActualSlots.integrated_diagonal line 530
  59. lemma OAI.PlanarUnitDistances.GlobalPairBudget.total_allowance line 552
  60. lemma OAI.PlanarUnitDistances.GlobalPairBudget.thickness_nonneg line 558
  61. lemma OAI.PlanarUnitDistances.GlobalPairBudget.cancellation line 568
  62. theorem OAI.PlanarUnitDistances.GlobalPairBudget.weighted_pair line 582