OAI/Combinatorics/KMedian/Amplification/AmplifierGuard.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.State line 12
2. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.guarded line 13
3. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.poly_guarded line 15
4. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule line 22
5. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule_zero line 24
6. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule_succ line 26
7. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.guarded_iterate line 42
8. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule_valid line 46
9. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule_count line 48
10. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.schedule_counter line 59
11. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.generate line 66
12. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.generate_eq line 68
13. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.generate_valid line 74