OAI/Combinatorics/SharpRamsey/Marking/HighRankEndpoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Selection.Law.support_card_pos line 13
  2. lemma OAI.SharpLogRamsey.Selection.entropy_snd_fiber_lower line 20
  3. lemma OAI.SharpLogRamsey.Selection.entropy_fst_fiber_lower line 42
  4. def OAI.SharpLogRamsey.Selection.highGoodFirst line 64
  5. def OAI.SharpLogRamsey.Selection.highGoodSecond line 67
  6. lemma OAI.SharpLogRamsey.Selection.Law.event_not_and line 70
  7. theorem OAI.SharpLogRamsey.Selection.high_second_upper_mass line 78
  8. theorem OAI.SharpLogRamsey.Selection.high_first_upper_mass line 87
  9. theorem OAI.SharpLogRamsey.Selection.high_second_bad line 96
  10. theorem OAI.SharpLogRamsey.Selection.high_first_bad line 111