OAI/Computability/BinPacking/Information/TraceLaw.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.CorrelatedSampling.firstAccepted line 19
  2. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.first_union_common line 24
  3. def OAI.BinPackingGames.Foundations.CorrelatedSampling.thresholdSample line 47
  4. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 51
  5. def OAI.BinPackingGames.Foundations.CorrelatedSampling.totalVariation line 68
  6. def OAI.BinPackingGames.Foundations.CorrelatedSampling.overlapMass line 70
  7. def OAI.BinPackingGames.Foundations.CorrelatedSampling.unionMass line 72
  8. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 74
  9. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 78
  10. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.min_abs_identity line 82
  11. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.max_abs_identity line 89
  12. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.overlapMass_eq line 96
  13. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.unionMass_eq line 104
  14. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.totalVariation_le_one line 112
  15. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.overlap_union_ratio line 119
  16. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 125
  17. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 134
  18. def OAI.BinPackingGames.Foundations.CorrelatedSampling.eventMass line 145
  19. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.eventMass_nonneg line 148
  20. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.eventMass_complement line 154
  21. def OAI.BinPackingGames.Foundations.CorrelatedSampling.geometricMass line 166
  22. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.geometricMass_nonneg line 170
  23. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.geometricMass_identity line 176
  24. def OAI.BinPackingGames.Foundations.CorrelatedSampling.firstHitWeight line 187
  25. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.firstHitWeight_nonneg line 195
  26. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.firstHitWeight_none line 209
  27. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.firstHitWeight_some line 215
  28. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.firstHitWeight_normalized line 225
  29. def OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstMass line 238
  30. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstMass_eq line 241
  31. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstMass_exact line 252
  32. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.commonMass_le_acceptMass line 268
  33. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstMass_lower_bound line 275
  34. structure OAI.BinPackingGames.Foundations.CorrelatedSampling.ThresholdInterval line 290
  35. def OAI.BinPackingGames.Foundations.CorrelatedSampling.splitPoint line 295
  36. def OAI.BinPackingGames.Foundations.CorrelatedSampling.splitLeft line 297
  37. def OAI.BinPackingGames.Foundations.CorrelatedSampling.splitRight line 300
  38. def OAI.BinPackingGames.Foundations.CorrelatedSampling.cutAt line 303
  39. def OAI.BinPackingGames.Foundations.CorrelatedSampling.intervalCDF line 305
  40. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.split_cdf line 307
  41. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.accepted_interval_mass line 312
  42. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitLeft_cut line 320
  43. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitRight_cut line 325
  44. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 333
  45. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 339
  46. def OAI.BinPackingGames.Foundations.CorrelatedSampling.splitAll line 345
  47. def OAI.BinPackingGames.Foundations.CorrelatedSampling.unitThresholdInterval line 349
  48. def OAI.BinPackingGames.Foundations.CorrelatedSampling.thresholdPartition line 351
  49. def OAI.BinPackingGames.Foundations.CorrelatedSampling.sumOnIntervals line 355
  50. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sumOn_splitAll line 359
  51. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.partition_sum line 369
  52. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.partition_total_mass line 378
  53. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.partition_cdf line 384
  54. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 389
  55. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 401
  56. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.partition_cuts line 415
  57. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 425
  58. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 435
  59. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sum_interval_get line 445
  60. def OAI.BinPackingGames.Foundations.CorrelatedSampling.traceAverage line 454
  61. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.traceAverage_const line 458
  62. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.traceAverage_mono line 464
  63. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.traceAverage_sum line 476
  64. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.firstAccepted_law line 488
  65. def OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstIndicator line 534
  66. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 539
  67. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 555