OAI/Combinatorics/SharpRamsey/Trees/OriginalTreeLoss.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.ActualPivot.banks_nonempty line 21
  2. def OAI.SharpLogRamsey.ActualPivot.density line 27
  3. lemma OAI.SharpLogRamsey.ActualPivot.density_nonneg line 33
  4. lemma OAI.SharpLogRamsey.ActualPivot.density_eq_count line 41
  5. lemma OAI.SharpLogRamsey.ActualPivot.Book.ready_failure_chrono line 52
  6. theorem OAI.SharpLogRamsey.ActualPivot.original_density_rejection line 79
  7. theorem OAI.SharpLogRamsey.ActualPivot.Book.first_trim line 108
  8. theorem OAI.SharpLogRamsey.ActualPivot.Book.second_trim line 137
  9. theorem OAI.SharpLogRamsey.ActualPivot.Book.deletion_loss line 166