OAI/Combinatorics/KMedian/CookLevin/CookAmplify.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.CookProgram.initial line 20
2. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_initial line 21
3. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.initial_valid line 23
4. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.initial_correct line 25
5. def OAI.MetricKMedian.PCP.Compiler.CookProgram.amplified line 29
6. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_amplified line 30
7. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.amplified_valid line 31
8. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.amplified_complete line 32
9. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.amplified_sound line 35