OAI/Combinatorics/IndependentSets/Repetition/Scalar.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.logTwo line 7
2. theorem OAI.IndependentSetsGames.Foundations.Repetition.logTwo_one line 9
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 11
4. theorem OAI.IndependentSetsGames.Foundations.Repetition.contraction_step line 23
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.initial_step line 62
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.cutoff_step line 67
7. theorem OAI.IndependentSetsGames.Foundations.Repetition.cutoff_le_length line 79
8. def OAI.IndependentSetsGames.Foundations.Repetition.ScalarRecurrence line 87
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.decay_to_cutoff line 91
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.block_contraction line 128
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.scalar_bound_6000 line 140
12. def OAI.IndependentSetsGames.Foundations.Repetition.incidenceRate line 163
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.incidenceRate_pos line 165
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.incidenceRate_lt_one line 167
15. theorem OAI.IndependentSetsGames.Foundations.Repetition.incidenceRate_fourth line 169
16. theorem OAI.IndependentSetsGames.Foundations.Repetition.incidence_rate_comparison line 173
17. theorem OAI.IndependentSetsGames.Foundations.Repetition.scalar_incidence_bound line 184