OAI/Combinatorics/KMedian/Amplification/LabelTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.BinaryCSP.mapLabels line 16
2. lemma OAI.MetricKMedian.PCP.BinaryCSP.mapLabels_allowed line 22
3. lemma OAI.MetricKMedian.PCP.BinaryCSP.mapLabels_complete line 27
4. lemma OAI.MetricKMedian.PCP.BinaryCSP.mapLabels_rejection line 34
5. abbrev OAI.MetricKMedian.PCP.Advice.BitIndex line 42
6. def OAI.MetricKMedian.PCP.Advice.bitsEquiv line 43