OAI/Combinatorics/Progressions/Dynamics/SpectralLogBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.CyclicCrootSisask.spectralIterations line 9
2. def OAI.Erdos3.CyclicCrootSisask.spectralIterationFactor line 12
3. theorem OAI.Erdos3.CyclicCrootSisask.spectralIterations_pos line 15
4. theorem OAI.Erdos3.CyclicCrootSisask.spectralIterationFactor_pos line 19
5. theorem OAI.Erdos3.CyclicCrootSisask.spectralIterations_le line 29
6. theorem OAI.Erdos3.CyclicCrootSisask.half_pow_spectralIterations_mul_exp_le line 52
7. theorem OAI.Erdos3.log_sixteen_div_le line 80
8. theorem OAI.Erdos3.CyclicCrootSisask.spectralIterations_le_logBudget line 97
9. theorem OAI.Erdos3.affineAllowance_inverse_le_exp line 118