OAI/Combinatorics/KMedian/CookLevin/CookSize.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Tableau.clauseEquiv line 15
2. lemma OAI.MetricKMedian.PCP.Tableau.clause_card line 31
3. lemma OAI.MetricKMedian.PCP.Tableau.total_clause_bound line 36
4. lemma OAI.MetricKMedian.PCP.CookLevin.firstWord_length line 53
5. def OAI.MetricKMedian.PCP.CookLevin.inputPoly line 57
6. def OAI.MetricKMedian.PCP.CookLevin.timePoly line 58
7. def OAI.MetricKMedian.PCP.CookLevin.spacePoly line 59
8. lemma OAI.MetricKMedian.PCP.CookLevin.inputSize_bound line 60
9. lemma OAI.MetricKMedian.PCP.CookLevin.time_bound line 63
10. lemma OAI.MetricKMedian.PCP.CookLevin.space_bound line 67
11. def OAI.MetricKMedian.PCP.CookLevin.testPoly line 70
12. lemma OAI.MetricKMedian.PCP.CookLevin.test_bound line 72
13. def OAI.MetricKMedian.PCP.CookLevin.alphabetEdgeCoeff line 79
14. lemma OAI.MetricKMedian.PCP.CookLevin.box_edges_formula line 81
15. def OAI.MetricKMedian.PCP.CookLevin.edgePoly line 84
16. lemma OAI.MetricKMedian.PCP.CookLevin.box_edges_bound line 85