OAI/Computability/VertexCover/Repetition/Scalar.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Repetition.logTwo line 40
2. theorem OAI.UniqueGames.Foundations.Repetition.logTwo_one line 42
3. theorem OAI.UniqueGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 44
4. theorem OAI.UniqueGames.Foundations.Repetition.contraction_step line 56
5. theorem OAI.UniqueGames.Foundations.Repetition.initial_step line 95
6. theorem OAI.UniqueGames.Foundations.Repetition.cutoff_step line 100
7. theorem OAI.UniqueGames.Foundations.Repetition.cutoff_le_length line 112
8. def OAI.UniqueGames.Foundations.Repetition.ScalarRecurrence line 120
9. theorem OAI.UniqueGames.Foundations.Repetition.decay_to_cutoff line 124
10. theorem OAI.UniqueGames.Foundations.Repetition.block_contraction line 161
11. theorem OAI.UniqueGames.Foundations.Repetition.scalar_bound_6000 line 173
12. def OAI.UniqueGames.Foundations.Repetition.incidenceRate line 196
13. theorem OAI.UniqueGames.Foundations.Repetition.incidenceRate_pos line 198
14. theorem OAI.UniqueGames.Foundations.Repetition.incidenceRate_lt_one line 200
15. theorem OAI.UniqueGames.Foundations.Repetition.incidenceRate_fourth line 202
16. theorem OAI.UniqueGames.Foundations.Repetition.incidence_rate_comparison line 206
17. theorem OAI.UniqueGames.Foundations.Repetition.scalar_incidence_bound line 217