OAI/Combinatorics/Progressions/Dynamics/CylinderShellCountBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.uniform_section_norm_product_le_exp line 11
2. theorem OAI.Erdos3.retained_shell_prefactor_le_exp line 33
3. theorem OAI.Erdos3.list_map_sum_le_exp line 69
4. theorem OAI.Erdos3.CylinderRemovalChain.shell_prefactor_le_exp line 88