OAI/Combinatorics/IndependentSets/Reduction/Parameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Integration.SourceParameters.rate line 9
2. theorem OAI.IndependentSetsGames.Integration.SourceParameters.rate_bounds line 11
3. theorem OAI.IndependentSetsGames.Integration.SourceParameters.fourth_power_comparison line 17
4. theorem OAI.IndependentSetsGames.Integration.SourceParameters.four_bit_rate_comparison line 33
5. theorem OAI.IndependentSetsGames.Integration.SourceParameters.logTwo_sixteen line 48
6. theorem OAI.IndependentSetsGames.Integration.SourceParameters.game_repetition_rate line 54
7. def OAI.IndependentSetsGames.Integration.SourceParameters.sourceThreshold line 72
8. theorem OAI.IndependentSetsGames.Integration.SourceParameters.sourceThreshold_pos line 74
9. theorem OAI.IndependentSetsGames.Integration.SourceParameters.exists_repetition_length line 79
10. def OAI.IndependentSetsGames.Integration.SourceParameters.repetitionLength line 85
11. theorem OAI.IndependentSetsGames.Integration.SourceParameters.repetitionLength_spec line 89
12. theorem OAI.IndependentSetsGames.Integration.SourceParameters.repetitionLength_real_bound line 95