OAI/Combinatorics/SharpRamsey/Exposure/ExposureMixture.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.ExposureModel.mix line 15
  2. lemma OAI.SharpLogRamsey.Selection.ExposureModel.mix_expectation line 31
  3. lemma OAI.SharpLogRamsey.Selection.ExposureModel.mix_mean line 36
  4. abbrev OAI.SharpLogRamsey.Selection.ExposureModel.Joint line 40
  5. def OAI.SharpLogRamsey.Selection.ExposureModel.joint line 42
  6. lemma OAI.SharpLogRamsey.Selection.ExposureModel.joint_expectation line 46
  7. lemma OAI.SharpLogRamsey.Selection.ExposureModel.restored_map line 51
  8. lemma OAI.SharpLogRamsey.Selection.ExposureModel.restore_support line 60
  9. def OAI.SharpLogRamsey.Selection.ExposureModel.contextual line 68
  10. theorem OAI.SharpLogRamsey.Selection.ExposureModel.contextual_preserves line 73
  11. theorem OAI.SharpLogRamsey.Selection.ExposureModel.contextual_map line 84