OAI/Combinatorics/KMedian/Amplification/AmplifierProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.power line 16
2. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.bits line 17
3. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.next line 19
4. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.poly_bits line 20
5. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.poly_next line 21
6. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.bitsRep line 23
7. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.bits_wellFormed line 27
8. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.nextRep line 28
9. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.next_wellFormed line 31
10. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.complete line 34
11. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.gap line 42