OAI/Combinatorics/SharpRamsey/Exposure/ExposureAverages.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.Selection.StateStatistic line 13
  2. def OAI.SharpLogRamsey.Selection.ExposureModel.mean line 20
  3. lemma OAI.SharpLogRamsey.Selection.ExposureModel.initial_mean line 24
  4. lemma OAI.SharpLogRamsey.Selection.ExposureModel.join_mean line 29
  5. def OAI.SharpLogRamsey.Selection.exposureAverage line 48
  6. theorem OAI.SharpLogRamsey.Selection.ExposureModel.atRound_mean line 57
  7. def OAI.SharpLogRamsey.Selection.reciprocalBadStatistic line 74
  8. def OAI.SharpLogRamsey.Selection.reciprocalSelectedStatistic line 78
  9. lemma OAI.SharpLogRamsey.Selection.exposureAverage_bad line 83
  10. lemma OAI.SharpLogRamsey.Selection.exposureAverage_selected line 99
  11. theorem OAI.SharpLogRamsey.Selection.ExposureModel.atRound_bad_selected line 115