OAI/Computability/VertexCover/PCP/SourceParameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Integration.SourceParameters.rate line 42
2. theorem OAI.UniqueGames.Integration.SourceParameters.rate_bounds line 44
3. theorem OAI.UniqueGames.Integration.SourceParameters.fourth_power_comparison line 50
4. theorem OAI.UniqueGames.Integration.SourceParameters.four_bit_rate_comparison line 66
5. theorem OAI.UniqueGames.Integration.SourceParameters.logTwo_sixteen line 81
6. theorem OAI.UniqueGames.Integration.SourceParameters.game_repetition_rate line 87
7. def OAI.UniqueGames.Integration.SourceParameters.sourceThreshold line 105
8. theorem OAI.UniqueGames.Integration.SourceParameters.sourceThreshold_pos line 107
9. theorem OAI.UniqueGames.Integration.SourceParameters.exists_repetition_length line 112
10. def OAI.UniqueGames.Integration.SourceParameters.repetitionLength line 118
11. theorem OAI.UniqueGames.Integration.SourceParameters.repetitionLength_spec line 122
12. theorem OAI.UniqueGames.Integration.SourceParameters.repetitionLength_real_bound line 128