OAI/Computability/VertexCover/Repetition/Factorization.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.UniqueGames.Foundations.Repetition.revealedProductWeightline 46 - def
OAI.UniqueGames.Foundations.Repetition.revealedLeftWeightline 52 - def
OAI.UniqueGames.Foundations.Repetition.revealedRightWeightline 57 - theorem
OAI.UniqueGames.Foundations.Repetition.revealedProductWeight_factorizesline 62 - theorem
OAI.UniqueGames.Foundations.Repetition.revealedProductWeight_local_restrictionsline 75 - theorem
OAI.UniqueGames.Foundations.Repetition.productWeight_massline 88 - def
OAI.UniqueGames.Foundations.Repetition.normalizedWeightline 94 - theorem
OAI.UniqueGames.Foundations.Repetition.normalizedWeight_isProbabilityline 97 - theorem
OAI.UniqueGames.Foundations.Repetition.normalized_productWeightline 105 - theorem
OAI.UniqueGames.Foundations.Repetition.normalized_rectangle_restrictionline 113