OAI/Combinatorics/KMedian/PCP/LocalReduction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.LocalRelation.Relation line 16
2. abbrev OAI.MetricKMedian.PCP.LocalRelation.Allowed line 20
3. abbrev OAI.MetricKMedian.PCP.LocalRelation.Vars line 21
4. abbrev OAI.MetricKMedian.PCP.LocalRelation.Eqs line 22
5. instance OAI.MetricKMedian.PCP.LocalRelation.(instance at line 24) line 24
6. instance OAI.MetricKMedian.PCP.LocalRelation.(instance at line 27) line 27
7. def OAI.MetricKMedian.PCP.LocalRelation.label line 31
8. def OAI.MetricKMedian.PCP.LocalRelation.quadratic line 33
9. def OAI.MetricKMedian.PCP.LocalRelation.leftEmbed line 35
10. def OAI.MetricKMedian.PCP.LocalRelation.rightEmbed line 36
11. def OAI.MetricKMedian.PCP.LocalRelation.rejectionWeight line 38
12. theorem OAI.MetricKMedian.PCP.LocalRelation.rejectionWeight_nonneg line 43
13. theorem OAI.MetricKMedian.PCP.LocalRelation.decode line 51
14. theorem OAI.MetricKMedian.PCP.LocalRelation.sound line 87
15. theorem OAI.MetricKMedian.PCP.LocalRelation.complete line 94