OAI/Combinatorics/SharpRamsey/Trees/TreePotential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.TreePotential.total line 10
2. def OAI.SharpLogRamsey.TreePotential.root line 14
3. def OAI.SharpLogRamsey.TreePotential.Admissible line 18
4. lemma OAI.SharpLogRamsey.TreePotential.root_nonneg line 23
5. lemma OAI.SharpLogRamsey.TreePotential.total_nonneg line 29
6. theorem OAI.SharpLogRamsey.TreePotential.total_le_height line 35
7. lemma OAI.SharpLogRamsey.TreePotential.total_mono line 55
8. lemma OAI.SharpLogRamsey.TreePotential.total_affine line 61
9. theorem OAI.SharpLogRamsey.TreePotential.cost_bound line 67