OAI/Combinatorics/Progressions/Dynamics/ModularDecayBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.modularTagGap_exponent line 12
2. theorem OAI.Erdos3.exists_modular_uncharged_decay_parameters line 39
3. theorem OAI.Erdos3.modular_local_decay_budget line 56
4. theorem OAI.Erdos3.modular_prod_rpow line 75
5. theorem OAI.Erdos3.modular_product_decay_budget line 87