OAI/Combinatorics/SharpRamsey/Selection/EndpointCurrent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Selection.Law.event_union_le line 13
  2. lemma OAI.SharpLogRamsey.Selection.Law.event_mono line 23
  3. def OAI.SharpLogRamsey.Selection.conditionalHeavy line 26
  4. def OAI.SharpLogRamsey.Selection.goodSecond line 29
  5. theorem OAI.SharpLogRamsey.Selection.badSecond_mass line 32
  6. def OAI.SharpLogRamsey.Selection.goodSecondHigh line 62
  7. theorem OAI.SharpLogRamsey.Selection.badSecondHigh_mass line 65
  8. theorem OAI.SharpLogRamsey.Selection.endpoint_entropy_from_fibers line 88