OAI/Computability/VertexCover/PCP/PoweringFinalConstants.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.Alphabetline 11 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.card_alphabetline 13 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_finalline 16 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.center_eqline 19 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.walkLength_eqline 25 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eqline 31 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.gain_eqline 35 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.gain_card_eqline 53 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eqline 59 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gapline 69