OAI/Computability/VertexCover/Reduction/RestrictionStarBudget.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_apply_function line 44
2. theorem OAI.VertexCover.Restriction.CompactCube.realWeights_update line 59
3. abbrev OAI.VertexCover.LabelCover.RestrictionWeights line 76
4. abbrev OAI.VertexCover.LabelCover.RestrictionSpace line 79
5. def OAI.VertexCover.LabelCover.restrictionBase line 82
6. def OAI.VertexCover.LabelCover.restrictionForm line 86
7. def OAI.VertexCover.LabelCover.restrictionFunction line 89
8. theorem OAI.VertexCover.LabelCover.restrictionFunction_apply line 94
9. theorem OAI.VertexCover.LabelCover.restrictionForm_energy line 100
10. def OAI.VertexCover.LabelCover.weightProjection line 106
11. theorem OAI.VertexCover.LabelCover.weightProjection_apply line 110
12. theorem OAI.VertexCover.LabelCover.weightProjection_commute line 116
13. theorem OAI.VertexCover.LabelCover.restriction_full_mean_zero line 123
14. def OAI.VertexCover.LabelCover.weightGroup line 138
15. theorem OAI.VertexCover.LabelCover.weightGroup_centered line 142
16. theorem OAI.VertexCover.LabelCover.weightGroup_energy_sum line 147
17. def OAI.VertexCover.LabelCover.seedProjection line 157
18. def OAI.VertexCover.LabelCover.starProjection line 162
19. def OAI.VertexCover.LabelCover.oppositeProjection line 165
20. theorem OAI.VertexCover.LabelCover.oppositeProjection_charge line 169
21. theorem OAI.VertexCover.LabelCover.condition_weightProjection_commute line 179
22. theorem OAI.VertexCover.LabelCover.weightProjection_separator line 185
23. theorem OAI.VertexCover.LabelCover.seedProjection_separator line 197
24. theorem OAI.VertexCover.LabelCover.starProjection_separator line 206
25. theorem OAI.VertexCover.LabelCover.restriction_weight_budget line 215
26. theorem OAI.VertexCover.LabelCover.restriction_seed_budget line 236
27. theorem OAI.VertexCover.LabelCover.restriction_star_budget line 257