OAI/Combinatorics/Progressions/Estimates/CoefficientNormalization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanCoefficientTail line 12
  2. theorem OAI.Erdos3.booleanCoefficientTail_eval line 19
  3. theorem OAI.Erdos3.booleanCoefficientTail_mass_le line 30
  4. theorem OAI.Erdos3.booleanCoefficientTail_totalDegree_le line 55
  5. def OAI.Erdos3.booleanJetColumnPolynomial line 84
  6. theorem OAI.Erdos3.booleanJetColumnPolynomial_eval line 88
  7. theorem OAI.Erdos3.booleanJetColumnPolynomial_mass_le line 95
  8. theorem OAI.Erdos3.booleanJetColumnPolynomial_degree_le line 106
  9. theorem OAI.Erdos3.booleanJetColumns_apply_coefficients line 115
  10. theorem OAI.Erdos3.polynomialParameterPoint_some line 137
  11. def OAI.Erdos3.normalizedCoefficientTail line 141
  12. def OAI.Erdos3.normalizedCoefficientTailValue line 149
  13. theorem OAI.Erdos3.normalizedCoefficientTail_eval line 157
  14. theorem OAI.Erdos3.normalizedCoefficientTail_mass_le line 167
  15. theorem OAI.Erdos3.normalizedCoefficientTail_totalDegree_le line 187
  16. theorem OAI.Erdos3.normalizedMonomialTerm line 209
  17. theorem OAI.Erdos3.normalizedProductTerm line 220
  18. theorem OAI.Erdos3.booleanMonomialArray_rescaling line 228
  19. theorem OAI.Erdos3.normalizedSmallCoefficientArray line 243