OAI/Combinatorics/IndependentSets/Expansion/GraphRounding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.mismatchSet line 16
2. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 20
3. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 23
4. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.roundLabels line 27
5. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 31
6. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 49
7. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 56
8. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 78
9. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 86
10. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 103
11. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 110
12. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 116
13. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 122
14. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.replacement_soundness line 134
15. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 150
16. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.combine_counts line 165