OAI/Combinatorics/KMedian/Machines/LocalCompiler.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.sum_left_index line 15
2. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.sum_right_index line 26
3. instance OAI.MetricKMedian.PCP.Compiler.LocalCompiler.assignmentSetCoding line 44
4. instance OAI.MetricKMedian.PCP.Compiler.LocalCompiler.assignmentSetHardcoded line 45
5. abbrev OAI.MetricKMedian.PCP.Compiler.LocalCompiler.Label line 46
6. def OAI.MetricKMedian.PCP.Compiler.LocalCompiler.relation line 47
7. lemma OAI.MetricKMedian.PCP.Compiler.LocalCompiler.poly_relation line 50
8. def OAI.MetricKMedian.PCP.Compiler.LocalCompiler.row line 52
9. def OAI.MetricKMedian.PCP.Compiler.LocalCompiler.table line 55
10. lemma OAI.MetricKMedian.PCP.Compiler.LocalCompiler.poly_table line 59
11. lemma OAI.MetricKMedian.PCP.Compiler.LocalCompiler.table_build line 85
12. def OAI.MetricKMedian.PCP.Compiler.LocalCompiler.represents line 102