OAI/Computability/VertexCover/Reduction/PrivateProjectionGroupLower.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VertexCover.LabelCover.otherWeightProjection line 43
2. theorem OAI.VertexCover.LabelCover.privateSeed_weight_commute line 47
3. theorem OAI.VertexCover.LabelCover.privateSeed_otherWeight_commute line 53
4. def OAI.VertexCover.LabelCover.privateAverageProjection line 60
5. theorem OAI.VertexCover.LabelCover.privateAverage_weight_commute line 65
6. def OAI.VertexCover.LabelCover.privateProjection line 75
7. theorem OAI.VertexCover.LabelCover.privateProjection_weight_commute line 80
8. theorem OAI.VertexCover.LabelCover.privateProjection_group_le line 89
9. theorem OAI.VertexCover.LabelCover.privateProjection_group_eq line 96
10. theorem OAI.VertexCover.LabelCover.privateAverage_loss_le line 105
11. theorem OAI.VertexCover.LabelCover.privateProjection_group_lower line 122