OAI/Combinatorics/KMedian/Machines/RawCSP.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MetricKMedian.PCP.Compiler.relationCoding line 12
2. instance OAI.MetricKMedian.PCP.Compiler.relationHardcoded line 13
3. abbrev OAI.MetricKMedian.PCP.Compiler.CSPRow line 15
4. abbrev OAI.MetricKMedian.PCP.Compiler.CSPTable line 16
5. lemma OAI.MetricKMedian.PCP.Compiler.csp_ext line 17
6. def OAI.MetricKMedian.PCP.Compiler.CSPTable.WellFormed line 22
7. def OAI.MetricKMedian.PCP.Compiler.CSPTable.csp line 24
8. structure OAI.MetricKMedian.PCP.Compiler.CSPTable.Represents line 30
9. lemma OAI.MetricKMedian.PCP.Compiler.CSPTable.Represents.wellFormed line 35
10. lemma OAI.MetricKMedian.PCP.Compiler.CSPTable.Represents.csp_eq line 50
11. def OAI.MetricKMedian.PCP.Compiler.CSPTable.self_represents line 66
12. def OAI.MetricKMedian.PCP.Compiler.CSPTable.row line 68
13. lemma OAI.MetricKMedian.PCP.Compiler.CSPTable.poly_row line 70