OAI/Computability/VertexCover/PCP/PreprocessingGuarantees.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 19
2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 32
3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 45
4. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 53
5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 62
6. def OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 70
7. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 75
8. def OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.roundLabels line 83
9. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.soundness line 87
10. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.completeness line 95
11. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 108