OAI/Combinatorics/KMedian/CookLevin/TableauCorrect.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.Tableau.decoded_run line 16
2. def OAI.MetricKMedian.PCP.Tableau.emptyControl line 33
3. def OAI.MetricKMedian.PCP.Tableau.emptyResponse line 34
4. def OAI.MetricKMedian.PCP.Tableau.honest line 35
5. lemma OAI.MetricKMedian.PCP.Tableau.honest_clamp line 41
6. lemma OAI.MetricKMedian.PCP.Tableau.honest_satisfies line 50