OAI/Computability/VertexCover/Fourier/SourceContexts.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 36
2. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 42
3. instance OAI.UniqueGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 48
4. instance OAI.UniqueGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 51
5. instance OAI.UniqueGames.Foundations.Hastad.SourceContexts.slotFintype line 53
6. instance OAI.UniqueGames.Foundations.Hastad.SourceContexts.slotInhabited line 57
7. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 59
8. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_slot line 63
9. abbrev OAI.UniqueGames.Foundations.Hastad.SourceContexts.I line 65
10. abbrev OAI.UniqueGames.Foundations.Hastad.SourceContexts.J line 66
11. abbrev OAI.UniqueGames.Foundations.Hastad.SourceContexts.ClauseContext line 67
12. abbrev OAI.UniqueGames.Foundations.Hastad.SourceContexts.VariableContext line 68
13. abbrev OAI.UniqueGames.Foundations.Hastad.SourceContexts.SlotContext line 69
14. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_I line 71
15. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_J line 72
16. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 73
17. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_VariableContext line 75
18. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.card_SlotContext line 77
19. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.localConsistent line 80
20. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 84
21. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.validJ line 91
22. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 96
23. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 104
24. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.validJ_consistent line 109
25. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 116
26. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.canonicalSlot line 123
27. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 127
28. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.pi line 139
29. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.sampledVariables line 143
30. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 147
31. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 152
32. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 160
33. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.honestJ line 168
34. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.honestI line 172
35. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.honestJ_valid line 176
36. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.pi_honest line 188
37. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 196
38. def OAI.UniqueGames.Foundations.Hastad.SourceContexts.baseAccepts line 202
39. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 208
40. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 216
41. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 223
42. theorem OAI.UniqueGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 233