OAI/Combinatorics/KMedian/Expanders/SmallBias.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.testRate_exists_le_sum line 13
2. lemma OAI.MetricKMedian.PCP.Walsh.small_bias_word_bound line 34
3. theorem OAI.MetricKMedian.PCP.Walsh.exists_small_bias line 60
4. theorem OAI.MetricKMedian.PCP.Walsh.exists_base_generators line 87
5. def OAI.MetricKMedian.PCP.Walsh.baseGenerators line 93
6. def OAI.MetricKMedian.PCP.Walsh.baseGraph line 95
7. theorem OAI.MetricKMedian.PCP.Walsh.baseGraph_contracts line 97