OAI/Combinatorics/SharpRamsey/Marking/ClassConditioning.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.onContextEvent line 14
  2. lemma OAI.SharpLogRamsey.Selection.Law.onContextEvent_map_mass line 28
  3. lemma OAI.SharpLogRamsey.Selection.Law.onContextEvent_support line 46
  4. lemma OAI.SharpLogRamsey.Selection.Law.onContextEvent_cond line 56
  5. lemma OAI.SharpLogRamsey.Selection.Law.onContextEvent_domination line 73
  6. lemma OAI.SharpLogRamsey.Selection.Law.onContextEvent_expectation line 89
  7. theorem OAI.SharpLogRamsey.Selection.selectedDeficit_onContextEvent line 108
  8. theorem OAI.SharpLogRamsey.Selection.selectedDeficit_onContextEvent_le line 125