OAI/Computability/UniqueGames/Inverse/RowErasureConcentration.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.UniqueGamesTheorem.Inverse.RowErasure.table_expect_prodline 15 - theorem
OAI.UniqueGamesTheorem.Inverse.RowErasure.exp_half_le_seven_quartersline 24 - theorem
OAI.UniqueGamesTheorem.Inverse.RowErasure.exp_half_indicatorline 30 - theorem
OAI.UniqueGamesTheorem.Inverse.RowErasure.table_coordinate_exp_leline 35