OAI/Combinatorics/Progressions/Dynamics/CandidateFrontSourceLossBudget.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.le_power_budget line 10
  2. theorem OAI.Erdos3.shifted_power_budget_le line 17
  3. theorem OAI.Erdos3.polynomial_budget_comp line 29
  4. def OAI.Erdos3.budgetDepthExponent line 37
  5. theorem OAI.Erdos3.bounded_depth_budget line 41
  6. theorem OAI.Erdos3.exponential_budget_comp line 49
  7. theorem OAI.Erdos3.product_exponential_budget line 54
  8. def OAI.Erdos3.VectorPolynomial.candidateFrontFamilyParameter line 77
  9. theorem OAI.Erdos3.VectorPolynomial.candidateFrontFamilyBounds line 79
  10. def OAI.Erdos3.iteratedPowerBudget line 146
  11. theorem OAI.Erdos3.iteratedPowerBudget_zero line 150
  12. theorem OAI.Erdos3.iteratedPowerBudget_succ line 152
  13. theorem OAI.Erdos3.iteratedPowerBudget_nonneg line 155
  14. theorem OAI.Erdos3.iteratedPowerBudget_monotone line 161
  15. theorem OAI.Erdos3.iteratedPowerBudget_ge line 167
  16. theorem OAI.Erdos3.iteratedPowerBudget_le_power line 171
  17. theorem OAI.Erdos3.powerCover_index_allowance_le_exp line 184
  18. theorem OAI.Erdos3.powerCover_grid_allowance_le_exp line 197
  19. theorem OAI.Erdos3.quadratic_shift_exp_budget line 208
  20. theorem OAI.Erdos3.VectorPolynomial.candidateFrontSourceLossBounds line 227