OAI/Combinatorics/Progressions/Estimates/SymmetricEvaluationLowerBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.continuous_momentProduct line 14
  2. theorem OAI.Erdos3.exists_momentProduct_unit_lower line 19
  3. theorem OAI.Erdos3.momentProduct_smul line 34
  4. theorem OAI.Erdos3.exists_momentProduct_lower line 50
  5. def OAI.Erdos3.momentLowerConstant line 79
  6. theorem OAI.Erdos3.momentLowerConstant_pos line 82
  7. theorem OAI.Erdos3.momentLowerConstant_bound line 85
  8. abbrev OAI.Erdos3.SymmetricEvaluationIndex line 100
  9. def OAI.Erdos3.symmetricEvaluation line 102
  10. theorem OAI.Erdos3.symmetricEvaluation_permute line 106
  11. theorem OAI.Erdos3.symmetricEvaluation_smul line 112
  12. theorem OAI.Erdos3.symmetricEvaluation_const_mul line 118
  13. theorem OAI.Erdos3.symmetricEvaluationIndex_card line 125
  14. theorem OAI.Erdos3.symmetricEvaluation_lower line 139