OAI/Combinatorics/KMedian/Projection/SeedTables.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.neutralTable line 12
2. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.portOrder line 14
3. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.goodTable line 15
4. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_goodTable line 17
5. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.badRoot line 20
6. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.badNodes line 21
7. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.badTable line 22
8. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.seedTable line 24
9. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_seedTable line 26
10. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.goodRoot line 28
11. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.goodNodes line 29
12. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.goodTable_build line 30