OAI/Combinatorics/Progressions/Polynomial/AffineSidePolynomialBudget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineLocalDegreeInputBudget line 9
  2. def OAI.Erdos3.affineOuterDegreeInputBudget line 12
  3. def OAI.Erdos3.affineLocalDegreeBudget line 14
  4. def OAI.Erdos3.affineAdaptiveDegreeBudget line 17
  5. theorem OAI.Erdos3.affineDegreeBudgets_nonneg line 20
  6. theorem OAI.Erdos3.affineComparisonDegree_le_polynomialBudget line 32
  7. theorem OAI.Erdos3.affineGlobalComparisonDegree_le_polynomialBudget line 73
  8. theorem OAI.Erdos3.adaptiveAffineCutoff_le_polynomialBudget line 106
  9. def OAI.Erdos3.affineOrderPolynomialBudget line 133
  10. def OAI.Erdos3.affineAccuracyPolynomialBudget line 137
  11. def OAI.Erdos3.affineSidePolynomialBudget line 141
  12. theorem OAI.Erdos3.affineSidePolynomialBudgets_nonneg line 144
  13. theorem OAI.Erdos3.affineComparisonRequiredOrder_le_budget line 154
  14. theorem OAI.Erdos3.affineComparisonAccuracyLog_le_budget line 175
  15. theorem OAI.Erdos3.adaptiveAffineSideLog_le_polynomialBudget line 188