OAI/Combinatorics/KMedian/Amplification/PaddingSound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.testSum_embedding line 13
2. lemma OAI.MetricKMedian.PCP.PortCSP.extend_bad_outside line 38
3. lemma OAI.MetricKMedian.PCP.PortCSP.extend_failure_mass line 45