OAI/Combinatorics/BalancedRyser/Profiles/ProfileMarkedOrders.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileMarkedOrders.expect_pair_by_target line 21
  2. theorem OAI.Balanced.ProfileMarkedOrders.real_uniform_event line 34
  3. theorem OAI.Balanced.ProfileMarkedOrders.memLp_finite line 42
  4. def OAI.Balanced.ProfileMarkedOrders.firstMark line 52
  5. def OAI.Balanced.ProfileMarkedOrders.firstMarkCount line 60
  6. theorem OAI.Balanced.ProfileMarkedOrders.firstMarkCount_le line 65
  7. theorem OAI.Balanced.ProfileMarkedOrders.firstMarkCount_antitone line 71
  8. theorem OAI.Balanced.ProfileMarkedOrders.mean_firstMarkCount_eq_sum line 81
  9. def OAI.Balanced.ProfileMarkedOrders.targetMarkEvent line 94
  10. theorem OAI.Balanced.ProfileMarkedOrders.mean_firstMark_eq_conditioned line 101
  11. theorem OAI.Balanced.ProfileMarkedOrders.mean_firstMarkCount_eq_conditioned_sum line 123
  12. def OAI.Balanced.ProfileMarkedOrders.targetStatistic line 133
  13. def OAI.Balanced.ProfileMarkedOrders.planeStatistic line 138
  14. def OAI.Balanced.ProfileMarkedOrders.conditionalMean line 142
  15. theorem OAI.Balanced.ProfileMarkedOrders.integral_conditioned_eq line 147
  16. theorem OAI.Balanced.ProfileMarkedOrders.detection_le_targetMark_add_error line 152
  17. theorem OAI.Balanced.ProfileMarkedOrders.detection_sum_le_mean_firstMarkCount_add_error line 193
  18. theorem OAI.Balanced.ProfileMarkedOrders.normalized_variance_error_le line 221
  19. def OAI.Balanced.ProfileMarkedOrders.markCount line 248
  20. theorem OAI.Balanced.ProfileMarkedOrders.markCount_le line 255
  21. theorem OAI.Balanced.ProfileMarkedOrders.markCount_antitone line 263
  22. theorem OAI.Balanced.ProfileMarkedOrders.mean_markCount_antitone line 272
  23. theorem OAI.Balanced.ProfileMarkedOrders.mean_markCount_eq_add line 283
  24. def OAI.Balanced.ProfileMarkedOrders.orderLaw line 292
  25. theorem OAI.Balanced.ProfileMarkedOrders.integral_orderLaw_eq line 295
  26. theorem OAI.Balanced.ProfileMarkedOrders.positive_mark_tail_of_mean_margin line 299