OAI/Combinatorics/Progressions/Estimates/RetainedCoefficientSlice.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.RetainedCoefficientSlice line 11
  2. abbrev OAI.Erdos3.RetainedCoefficientSlice.Domain line 27
  3. def OAI.Erdos3.RetainedCoefficientSlice.sliceWeight line 29
  4. theorem OAI.Erdos3.RetainedCoefficientSlice.sliceWeight_nonneg line 31
  5. theorem OAI.Erdos3.RetainedCoefficientSlice.total_pos line 33
  6. def OAI.Erdos3.RetainedCoefficientSlice.law line 36
  7. def OAI.Erdos3.RetainedCoefficientSlice.finiteSlice line 39
  8. theorem OAI.Erdos3.RetainedCoefficientSlice.length_pos_of_size line 46
  9. def OAI.Erdos3.RetainedCoefficientSlice.normalizer line 49
  10. theorem OAI.Erdos3.RetainedCoefficientSlice.normalizer_eq_mean line 55
  11. theorem OAI.Erdos3.RetainedCoefficientSlice.normalizer_lower line 68
  12. def OAI.Erdos3.RetainedCoefficientSlice.normalized line 72
  13. theorem OAI.Erdos3.RetainedCoefficientSlice.normalized_coefficientDensity line 79
  14. theorem OAI.Erdos3.RetainedCoefficientSlice.normalized_coefficientWeights line 83
  15. theorem OAI.Erdos3.RetainedCoefficientSlice.affine_abs_le line 89