OAI/Combinatorics/KMedian/Amplification/RegularSpec.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.padGraph line 15
2. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.padCSP line 16
3. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.regularGraph line 17
4. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.regularCSP line 18
5. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.paddedRotate_correct line 20
6. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.paddedAllowed_correct line 39
7. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.strongRotate_correct line 50
8. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.rotate_correct line 58
9. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.allowed_correct line 66