OAI/Combinatorics/KMedian/Amplification/CSPMix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.PortCSP.blend line 19
2. lemma OAI.MetricKMedian.PCP.PortCSP.blend_bad line 31
3. lemma OAI.MetricKMedian.PCP.PortCSP.blend_complete line 39
4. lemma OAI.MetricKMedian.PCP.PortCSP.blend_failure line 52
5. def OAI.MetricKMedian.PCP.PortCSP.always line 88
6. lemma OAI.MetricKMedian.PCP.PortCSP.always_complete line 93
7. lemma OAI.MetricKMedian.PCP.PortCSP.always_bad line 98
8. lemma OAI.MetricKMedian.PCP.PortCSP.always_failure line 102