OAI/Computability/VertexCover/Repetition/Overlap.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.UniqueGames.Foundations.Repetition.min_half_formulaline 45 - theorem
OAI.UniqueGames.Foundations.Repetition.sum_min_one_sub_tvline 53 - theorem
OAI.UniqueGames.Foundations.Repetition.discount_le_selfline 62 - theorem
OAI.UniqueGames.Foundations.Repetition.discount_loss_le_mulline 67 - def
OAI.UniqueGames.Foundations.Repetition.discountedCommonMassline 77 - theorem
OAI.UniqueGames.Foundations.Repetition.discounted_common_mass_boundsline 81 - def
OAI.UniqueGames.Foundations.Repetition.diagonalWeightsline 141 - theorem
OAI.UniqueGames.Foundations.Repetition.diagonalWeights_isProbabilityline 146 - theorem
OAI.UniqueGames.Foundations.Repetition.diagonal_overlap_identityline 157 - theorem
OAI.UniqueGames.Foundations.Repetition.diagonal_sampler_totalVariation_leline 182