OAI/Combinatorics/KMedian/CookLevin/SemanticProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.Width line 16
2. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.LeftAlphabet line 17
3. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.RightAlphabet line 18
4. def OAI.MetricKMedian.PCP.ProjectionSeed.input line 19
5. lemma OAI.MetricKMedian.PCP.ProjectionSeed.input_perfect line 22
6. lemma OAI.MetricKMedian.PCP.ProjectionSeed.input_sound line 26
7. lemma OAI.MetricKMedian.PCP.ProjectionSeed.repetition_exists line 36
8. theorem OAI.MetricKMedian.PCP.mathematical_projection_producer line 43