OAI/Combinatorics/SharpRamsey/Exposure/ExposureModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.equiprobable line 15
  2. lemma OAI.SharpLogRamsey.Selection.Law.equiprobable_sum line 20
  3. def OAI.SharpLogRamsey.Selection.pasteTuple line 25
  4. lemma OAI.SharpLogRamsey.Selection.pasteTuple_compl line 29
  5. lemma OAI.SharpLogRamsey.Selection.Law.restore_restrict line 32
  6. structure OAI.SharpLogRamsey.Selection.ExposureModel line 56
  7. def OAI.SharpLogRamsey.Selection.ExposureModel.expectation line 76
  8. def OAI.SharpLogRamsey.Selection.ExposureModel.initial line 79
  9. lemma OAI.SharpLogRamsey.Selection.ExposureModel.initial_expectation line 96
  10. def OAI.SharpLogRamsey.Selection.ExposureModel.join line 101
  11. lemma OAI.SharpLogRamsey.Selection.ExposureModel.join_expectation line 124
  12. lemma OAI.SharpLogRamsey.Selection.ExposureModel.join_preserves line 141