OAI/Computability/VertexCover/PCP/PoweringOpinions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringOpinions.opinionAt line 20
2. theorem OAI.UniqueGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 27
3. def OAI.UniqueGames.Foundations.PCP.PoweringOpinions.honestLabels line 35
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 38
5. def OAI.UniqueGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 48
6. def OAI.UniqueGames.Foundations.PCP.PoweringOpinions.decoded line 53
7. def OAI.UniqueGames.Foundations.PCP.PoweringOpinions.matchFn line 58
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 64
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 74
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 84