OAI/Computability/VertexCover/PCP/PreprocessingRegularSoundness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 12
2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 16
3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 22
4. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 29
5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 40
6. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 49
7. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 71
8. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 78
9. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 89
10. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 98
11. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 104
12. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 126
13. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 135