OAI/Combinatorics/Progressions/Fourier/RationalBohrWidth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.BohrWidthBudget.selector_scale_lower_bound line 9
2. theorem OAI.Erdos3.BohrWidthBudget.polynomial_denominator_le_exp line 21
3. theorem OAI.Erdos3.BohrWidthBudget.exp_neg_budget_le_reciprocal line 50
4. theorem OAI.Erdos3.BohrWidthBudget.rational_width_lower_bound line 66
5. theorem OAI.Erdos3.BohrWidthBudget.rational_width_ge_exponential line 96