OAI/Combinatorics/IndependentSets/Expansion/PoweringOpinions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.opinionAt line 17
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 24
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.honestLabels line 32
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 35
5. def OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 45
6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.decoded line 50
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.matchFn line 55
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 61
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 71
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 81
11. def OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.ReachLE line 106
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reach_refl line 109
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reach_mono line 112
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reach_prepend line 117
15. def OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reversePorts line 124
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reversePorts_length line 128
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 134
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 145
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.reach_reverse line 155
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.tail_reach line 167
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 181
22. def OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.tailFromStart line 195
23. def OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.headFromEnd line 199
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.tailFromStart_val line 203
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReach.headFromEnd_val line 207