OAI/Combinatorics/SharpRamsey/Selection/FreshRepresentatives.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.Selection.ExposureModel.FreshHistory line 14
  2. def OAI.SharpLogRamsey.Selection.ExposureModel.freshLaw line 16
  3. lemma OAI.SharpLogRamsey.Selection.ExposureModel.freshLaw_sum line 21
  4. lemma OAI.SharpLogRamsey.Selection.ExposureModel.freshLaw_old line 31
  5. def OAI.SharpLogRamsey.Selection.ExposureModel.afterDraw line 43
  6. lemma OAI.SharpLogRamsey.Selection.ExposureModel.afterDraw_preserves line 59
  7. def OAI.SharpLogRamsey.Selection.ExposureModel.freshBad line 63
  8. def OAI.SharpLogRamsey.Selection.ExposureModel.freshSelected line 68
  9. lemma OAI.SharpLogRamsey.Selection.ExposureModel.fresh_bad_mean line 75
  10. lemma OAI.SharpLogRamsey.Selection.ExposureModel.fresh_selected_mean line 84