OAI/Computability/MinUncut/Games/Parameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Integration.SourceParameters.rate line 10
2. theorem OAI.MinUncutGames.Integration.SourceParameters.rate_bounds line 12
3. theorem OAI.MinUncutGames.Integration.SourceParameters.fourth_power_comparison line 18
4. theorem OAI.MinUncutGames.Integration.SourceParameters.four_bit_rate_comparison line 34
5. theorem OAI.MinUncutGames.Integration.SourceParameters.logTwo_sixteen line 49
6. theorem OAI.MinUncutGames.Integration.SourceParameters.game_repetition_rate line 55
7. def OAI.MinUncutGames.Integration.SourceParameters.sourceThreshold line 73
8. theorem OAI.MinUncutGames.Integration.SourceParameters.sourceThreshold_pos line 75
9. theorem OAI.MinUncutGames.Integration.SourceParameters.exists_repetition_length line 80
10. def OAI.MinUncutGames.Integration.SourceParameters.repetitionLength line 86
11. theorem OAI.MinUncutGames.Integration.SourceParameters.repetitionLength_spec line 90
12. theorem OAI.MinUncutGames.Integration.SourceParameters.repetitionLength_real_bound line 96