OAI/Combinatorics/Progressions/Estimates/FixedPositiveCoefficientSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fixedPositiveCoefficientSource line 11
  2. theorem OAI.Erdos3.fixedPositiveCoefficientSource_length line 16
  3. theorem OAI.Erdos3.fixedPositiveCoefficientSource_weightBound line 19
  4. theorem OAI.Erdos3.fixedPositiveCoefficientSource_weightLipschitz line 22
  5. theorem OAI.Erdos3.fixedPositiveCoefficientSource_residueSet line 25
  6. theorem OAI.Erdos3.fixedPositiveCoefficientSource_mean line 40
  7. theorem OAI.Erdos3.fixedPositiveCoefficientSource_complexMean line 49
  8. theorem OAI.Erdos3.fixedPositiveCoefficientSource_law line 58
  9. theorem OAI.Erdos3.fixedPositiveCoefficientSource_support line 72
  10. theorem OAI.Erdos3.fixedPositiveCoefficientSource_positive line 86
  11. theorem OAI.Erdos3.fixedPositiveCoefficientSource_primitive line 97
  12. theorem OAI.Erdos3.fixedPositiveCoefficientSource_primitive_of_le line 102