OAI/Combinatorics/SharpRamsey/Trees/PivotBanks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpLogRamsey.ActualPivot.Input line 18
  2. def OAI.SharpLogRamsey.ActualPivot.Input.firstCall line 36
  3. abbrev OAI.SharpLogRamsey.ActualPivot.FirstBank line 40
  4. abbrev OAI.SharpLogRamsey.ActualPivot.SecondBank line 42
  5. abbrev OAI.SharpLogRamsey.ActualPivot.Input.FirstRow line 45
  6. lemma OAI.SharpLogRamsey.ActualPivot.Input.first_valid line 50
  7. def OAI.SharpLogRamsey.ActualPivot.Input.secondCall line 55
  8. lemma OAI.SharpLogRamsey.ActualPivot.Input.second_overhead line 63
  9. def OAI.SharpLogRamsey.ActualPivot.Input.next line 67
  10. lemma OAI.SharpLogRamsey.ActualPivot.Input.next_none line 73
  11. lemma OAI.SharpLogRamsey.ActualPivot.Input.next_overhead line 79
  12. def OAI.SharpLogRamsey.ActualPivot.Input.failure line 88
  13. def OAI.SharpLogRamsey.ActualPivot.Input.secondLoss line 92
  14. theorem OAI.SharpLogRamsey.ActualPivot.Input.failure_bound line 98
  15. theorem OAI.SharpLogRamsey.ActualPivot.Input.second_loss_bound line 133