OAI/Combinatorics/KMedian/Projection/SeedSound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.good line 13
2. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.chosen_legal line 14
3. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.good_consistent line 18
4. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.regular_complete line 21
5. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.allLegal_of_perfect line 25
6. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.good_perfect line 33
7. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.rejection line 37
8. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.good_bound line 50