OAI/Combinatorics/Chromatic/Witness/GraphDecoratedHistories.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.sum_subtype_ite line 14
2. abbrev OAI.ElementaryPositivity.TriangularDynamics.DecoratedLeaf line 27
3. def OAI.ElementaryPositivity.TriangularDynamics.leafEnergy line 30
4. abbrev OAI.ElementaryPositivity.TriangularDynamics.DecoratedWord line 31
5. def OAI.ElementaryPositivity.TriangularDynamics.decoratedMask line 32
6. def OAI.ElementaryPositivity.TriangularDynamics.decoratedEnergy line 33
7. abbrev OAI.ElementaryPositivity.TriangularDynamics.RequiredDecorated line 34
8. def OAI.ElementaryPositivity.TriangularDynamics.requiredDecoratedEquiv line 36
9. lemma OAI.ElementaryPositivity.TriangularDynamics.decorated_coefficient line 43
10. lemma OAI.ElementaryPositivity.TriangularDynamics.required_energy_sum line 61