OAI/Combinatorics/Progressions/Dynamics/PointwiseSymbolBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.shift_le_power_succ line 9
2. theorem OAI.Erdos3.shifted_self_power_le_base_power line 20
3. theorem OAI.Erdos3.exists_symbol_extension_budget line 26
4. theorem OAI.Erdos3.symbol_spanning_count_bound line 52
5. theorem OAI.Erdos3.symbol_spanning_parameter_ge line 66
6. theorem OAI.Erdos3.symbol_spanning_parameter_power_bound line 73
7. theorem OAI.Erdos3.symbol_spanning_shifted_parameter_power_bound line 79