OAI/Combinatorics/Progressions/Dynamics/PatchIterationBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_reset_scale_of_log_bound line 10
  2. theorem OAI.Erdos3.log_log_length_loss line 46
  3. theorem OAI.Erdos3.log_patch_reset_cost_le line 68
  4. theorem OAI.Erdos3.slice_reset_log_room line 81
  5. theorem OAI.Erdos3.patch_reset_cutoff_bound line 105
  6. theorem OAI.Erdos3.patch_reset_cutoff_of_loglog line 125
  7. theorem OAI.Erdos3.eventually_two_resource_costs_fit line 155
  8. theorem OAI.Erdos3.eventually_constant_add_rank_loss_paid line 164
  9. theorem OAI.Erdos3.subquadratic_patch_iteration_budgets line 177