OAI/Computability/MinUncut/Encoding/GameDecoder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Hastad.distribution_sq_expectation_le line 14
2. def OAI.MinUncutGames.Foundations.Hastad.projectionGame line 44
3. def OAI.MinUncutGames.Foundations.Hastad.questionBias line 49
4. def OAI.MinUncutGames.Foundations.Hastad.questionAcceptance line 53
5. theorem OAI.MinUncutGames.Foundations.Hastad.questionAcceptance_eq line 58
6. inductive OAI.MinUncutGames.Foundations.Hastad.ConditionedOracle line 69
7. def OAI.MinUncutGames.Foundations.Hastad.ConditionedOracle.answer line 73
8. def OAI.MinUncutGames.Foundations.Hastad.ConditionedOracle.fallback line 77
9. theorem OAI.MinUncutGames.Foundations.Hastad.testBias_constant_right line 83
10. theorem OAI.MinUncutGames.Foundations.Hastad.empty_conditioned_bias line 90
11. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedOracle_response_bound line 100
12. theorem OAI.MinUncutGames.Foundations.Hastad.folded_game_decoder_bound line 120
13. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 158
14. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 194