OAI/Combinatorics/Progressions/Linear/SubquadraticRankPayment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.affine_recurrence_le line 10
  2. theorem OAI.Erdos3.log_rank_step line 31
  3. theorem OAI.Erdos3.log_rank_recurrence_le line 45
  4. theorem OAI.Erdos3.log_rank_at_selected_level line 57
  5. theorem OAI.Erdos3.subquadratic_rank_exponents line 71
  6. theorem OAI.Erdos3.density_invariant_with_general_loss line 88
  7. theorem OAI.Erdos3.log_one_add_rank_recurrence line 107
  8. theorem OAI.Erdos3.log_one_add_rank_at_selected_level line 122
  9. theorem OAI.Erdos3.eventually_rpow_log_le line 143
  10. theorem OAI.Erdos3.eventually_subquadratic_rank_loss_paid line 173