OAI/Combinatorics/Progressions/Polynomial/WeightedLinearPolynomialRestriction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.linearCoordinatePolynomial line 14
  2. def OAI.Erdos3.polynomialLinearRestriction line 19
  3. theorem OAI.Erdos3.linearMap_apply_sum_coordinates line 25
  4. theorem OAI.Erdos3.polynomialLinearRestriction_X line 37
  5. theorem OAI.Erdos3.polynomialLinearRestriction_C line 43
  6. theorem OAI.Erdos3.eval_linearCoordinatePolynomial line 49
  7. theorem OAI.Erdos3.scalarDirectionalDerivative_linearCoordinatePolynomial line 57
  8. theorem OAI.Erdos3.eval_polynomialLinearRestriction line 67
  9. theorem OAI.Erdos3.scalarDirectionalDerivative_linearRestriction line 75
  10. theorem OAI.Erdos3.coeff_zero_polynomialLinearRestriction line 85
  11. theorem OAI.Erdos3.polynomialTranslate_linearCoordinatePolynomial line 92
  12. theorem OAI.Erdos3.polynomialLinearRestriction_translate line 104
  13. theorem OAI.Erdos3.polynomialTranslationPath_linearCoordinatePolynomial line 126
  14. theorem OAI.Erdos3.polynomialLinearRestriction_translationPath line 139
  15. theorem OAI.Erdos3.polynomialLinearRestriction_exponentialPath line 151
  16. theorem OAI.Erdos3.polynomialLinearRestriction_exponentialCoordinate line 161
  17. theorem OAI.Erdos3.linearCoordinatePolynomial_eq_sum line 182
  18. theorem OAI.Erdos3.linearCoordinatePolynomial_isWeightedHomogeneous line 196
  19. theorem OAI.Erdos3.polynomialLinearRestriction_monomial_homogeneous line 209
  20. theorem OAI.Erdos3.polynomialLinearRestriction_isWeightedHomogeneous line 223
  21. theorem OAI.Erdos3.polynomialLinearRestriction_weightedHomogeneousComponent line 235
  22. theorem OAI.Erdos3.polynomialLinearRestriction_mem_weightedSupportDrop line 251
  23. theorem OAI.Erdos3.polynomialLinearRestriction_mem_weightedSupportLT line 265
  24. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_polynomial_eq_component line 277
  25. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_eq_zero_of_lt line 300