OAI/Combinatorics/KMedian/Amplification/PaddedAlphabet.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.RelationInterior line 13
2. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.UniversalInterior line 16
3. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.PaddedPosition line 18
4. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.PaddedNode line 20
5. instance OAI.MetricKMedian.PCP.AlphabetReduction.paddedNodeFintype line 22
6. def OAI.MetricKMedian.PCP.AlphabetReduction.interiorEmbed line 28
7. def OAI.MetricKMedian.PCP.AlphabetReduction.positionEmbed line 31
8. def OAI.MetricKMedian.PCP.AlphabetReduction.nodeEmbed line 33
9. def OAI.MetricKMedian.PCP.AlphabetReduction.paddedBinary line 35
10. lemma OAI.MetricKMedian.PCP.AlphabetReduction.padded_complete line 38
11. lemma OAI.MetricKMedian.PCP.AlphabetReduction.padded_sound line 43
12. lemma OAI.MetricKMedian.PCP.AlphabetReduction.universalInterior_card line 46
13. lemma OAI.MetricKMedian.PCP.AlphabetReduction.padded_node_card line 49