OAI/Computability/VertexCover/PCP/CayleySampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.CayleySampling.FalseFiber line 18
2. def OAI.UniqueGames.Foundations.PCP.CayleySampling.falseRepresentative line 20
3. def OAI.UniqueGames.Foundations.PCP.CayleySampling.booleanSplitEquiv line 25
4. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 41
5. def OAI.UniqueGames.Foundations.PCP.CayleySampling.sampleSplitEquiv line 45
6. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 51
7. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.card_boolean_split line 55
8. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.expect_boolean_samples line 60
9. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 80
10. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.expect_parity_samples line 89
11. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.expect_walsh_samples line 98
12. theorem OAI.UniqueGames.Foundations.PCP.CayleySampling.expect_walsh_mean line 105