OAI/Combinatorics/ThinTrees/ShortcutDuality.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.StrongThinTree.MultiGraph.point line 13
2. def OAI.StrongThinTree.MultiGraph.incidence line 15
3. lemma OAI.StrongThinTree.MultiGraph.eval_incidence line 17
4. abbrev OAI.StrongThinTree.MultiGraph.ProperCut line 21
5. def OAI.StrongThinTree.MultiGraph.cutIndicator line 23
6. lemma OAI.StrongThinTree.MultiGraph.cutIndicator_binary line 25
7. lemma OAI.StrongThinTree.MultiGraph.cutIndicator_energy line 29
8. lemma OAI.StrongThinTree.MultiGraph.binary_matrix_energy line 38
9. lemma OAI.StrongThinTree.MultiGraph.contraction_embedding line 52
10. lemma OAI.StrongThinTree.MultiGraph.contraction_edge_diag line 75
11. def OAI.StrongThinTree.MultiGraph.Hierarchy.shortcutCoefficient line 89
12. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.shortcutCoefficient_nonneg line 92
13. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.binary_numerator_bound line 98
14. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.exists_shortcut_explicit line 124