OAI/Computability/VertexCover/Reduction/HighVectorsSeparated.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.VertexCover.LabelCover.pairEvents_card_eq_sum line 42
2. theorem OAI.VertexCover.LabelCover.decoding_upper_bound line 55
3. theorem OAI.VertexCover.LabelCover.norm_sub_rev line 78
4. theorem OAI.VertexCover.LabelCover.norm_sub_triangle line 85
5. def OAI.VertexCover.LabelCover.distanceTo line 90
6. theorem OAI.VertexCover.LabelCover.distanceTo_nonneg line 94
7. theorem OAI.VertexCover.LabelCover.distanceTo_le line 99
8. theorem OAI.VertexCover.LabelCover.distanceTo_self line 104
9. theorem OAI.VertexCover.LabelCover.distanceTo_triangle line 112
10. def OAI.VertexCover.LabelCover.separator line 122
11. theorem OAI.VertexCover.LabelCover.separator_odd line 126
12. theorem OAI.VertexCover.LabelCover.separator_zero line 132
13. theorem OAI.VertexCover.LabelCover.separator_lipschitz line 136
14. theorem OAI.VertexCover.LabelCover.separator_pos_on line 151
15. def OAI.VertexCover.LabelCover.highVectors line 165
16. theorem OAI.VertexCover.LabelCover.highVectors_separated line 170