OAI/Computability/VertexCover/Reduction/HonestLargeSumIndependent.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VertexCover.LabelCover.gridRational line 40
2. abbrev OAI.VertexCover.LabelCover.Vertex line 43
3. def OAI.VertexCover.LabelCover.sumVector line 46
4. def OAI.VertexCover.LabelCover.graph line 50
5. theorem OAI.VertexCover.LabelCover.low_norm_adjacent line 55
6. theorem OAI.VertexCover.LabelCover.low_norm_subsingleton line 61
7. theorem OAI.VertexCover.LabelCover.honestSelection_form_increment line 69
8. def OAI.VertexCover.LabelCover.honestSum line 88
9. theorem OAI.VertexCover.LabelCover.honestSelection_form_sumVector line 93
10. theorem OAI.VertexCover.LabelCover.honest_large_sum_independent line 101