OAI/Combinatorics/IndependentSets/Expansion/PoweringTableSemantics.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 10
2. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 13
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 16
4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 20
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 24
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 30
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 36
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 48
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 57
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 72
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 83
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 90
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 97
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 114
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 122
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 137
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 156