OAI/Combinatorics/RamseyFive/Trees/PivotPotential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.PivotTree.potential line 7
2. lemma OAI.SharpRamseyFive.PivotTree.cap_potential line 9
3. theorem OAI.SharpRamseyFive.PivotTree.split_potential line 25
4. lemma OAI.SharpRamseyFive.PivotTree.log_deficits line 47
5. lemma OAI.SharpRamseyFive.PivotTree.initial_potential line 64