OAI/Combinatorics/Progressions/Dynamics/PreparedFreezingEarlyLogBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.preparedFreezingRadiusBudget_of_terms line 11
2. theorem OAI.Erdos3.preparedFreezingRadiusBudget_of_inflated_chart line 46
3. theorem OAI.Erdos3.preparedFreezingRadiusBudget_of_radius line 68
4. theorem OAI.Erdos3.preparedFreezingInflation_exp_bound line 98
5. theorem OAI.Erdos3.exp_succ_bounds_add_one line 113
6. theorem OAI.Erdos3.preparedFreezingEarlyLogBudget line 120