OAI/Combinatorics/Progressions/Estimates/FiniteSeriesCoefficientBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteSeriesWeight line 11
  2. def OAI.Erdos3.finiteSeriesDenominator line 14
  3. def OAI.Erdos3.finiteSeriesNumerator line 16
  4. def OAI.Erdos3.finiteSeriesNumeratorBound line 19
  5. theorem OAI.Erdos3.finiteSeriesDenominator_pos line 22
  6. theorem OAI.Erdos3.finiteSeriesNumeratorBound_pos line 25
  7. theorem OAI.Erdos3.finiteSeriesNumerator_cast line 29
  8. theorem OAI.Erdos3.finiteSeriesNumerator_le line 33
  9. theorem OAI.Erdos3.finiteExp_freeCoefficientBound line 39
  10. theorem OAI.Erdos3.finiteLog_freeCoefficientBound line 53
  11. def OAI.Erdos3.bchProductDenominator line 83
  12. def OAI.Erdos3.bchProductNumeratorBound line 86
  13. theorem OAI.Erdos3.bchProductDenominator_pos line 91
  14. theorem OAI.Erdos3.bchProductPolynomial_coefficient_bound line 95