OAI/Combinatorics/SharpRamsey/Trees/ChronologicalExecution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.FreshExecution.card_mul_kernel_sum line 15
  2. lemma OAI.SharpLogRamsey.FreshExecution.sdiff_card_eq_sum line 30
  3. lemma OAI.SharpLogRamsey.FreshExecution.firstLoss_points line 38
  4. lemma OAI.SharpLogRamsey.FreshExecution.secondLoss_points line 48
  5. abbrev OAI.SharpLogRamsey.ActualPivot.ChronoDomains line 70
  6. def OAI.SharpLogRamsey.ActualPivot.chronoRead line 72
  7. def OAI.SharpLogRamsey.ActualPivot.chronoMask line 76
  8. lemma OAI.SharpLogRamsey.ActualPivot.chronoRead_first line 81
  9. lemma OAI.SharpLogRamsey.ActualPivot.chronoRead_second line 87
  10. def OAI.SharpLogRamsey.ActualPivot.Book.chronoChoose line 95
  11. theorem OAI.SharpLogRamsey.ActualPivot.Book.first_loss_bound line 99
  12. theorem OAI.SharpLogRamsey.ActualPivot.Book.second_loss_bound line 126