OAI/Combinatorics/KMedian/Amplification/PoweringConstruction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.cast_start line 16
2. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.cast_end line 18
3. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.center_left_far line 20
4. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.center_right_far line 24
5. def OAI.MetricKMedian.PCP.PortCSP.CutAccept line 36
6. lemma OAI.MetricKMedian.PCP.PortCSP.cutAccept_iff line 42
7. lemma OAI.MetricKMedian.PCP.PortCSP.accepted_cut_zero line 52
8. def OAI.MetricKMedian.PCP.PortCSP.PathAccept line 65
9. def OAI.MetricKMedian.PCP.PortCSP.stoppedPath line 68
10. abbrev OAI.MetricKMedian.PCP.PortCSP.PowerEdge line 72
11. def OAI.MetricKMedian.PCP.PortCSP.powered line 74
12. lemma OAI.MetricKMedian.PCP.PortCSP.powered_allowed line 82
13. lemma OAI.MetricKMedian.PCP.PortCSP.honest_cut line 88
14. theorem OAI.MetricKMedian.PCP.PortCSP.powered_complete line 96
15. lemma OAI.MetricKMedian.PCP.PortCSP.accepted_witness_zero line 107
16. theorem OAI.MetricKMedian.PCP.PortCSP.support_le_powered line 128
17. theorem OAI.MetricKMedian.PCP.PortCSP.powered_sound line 134
18. theorem OAI.MetricKMedian.PCP.PortCSP.powered_edges line 147