OAI/Combinatorics/KMedian/Amplification/AmplifierIteration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.fallback line 12
2. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.fallback_valid line 13
3. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.normalize line 20
4. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.normalize_valid line 21
5. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.normalize_eq line 26
6. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.poly_normalize line 28
7. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.iterate line 31
8. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.iterate_valid line 34
9. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.iterate_count line 40
10. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.iterate_complete line 52
11. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.iterate_gap line 61