OAI/Combinatorics/Progressions/Estimates/WeightedAxisScaling.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.translationDirectionalDerivative line 16
  2. theorem OAI.Erdos3.translationDirectionalDerivative_apply line 20
  3. def OAI.Erdos3.translationDirectionalSeries line 26
  4. theorem OAI.Erdos3.degreeOf_rename_inl_inr line 42
  5. theorem OAI.Erdos3.translationDirectionalDerivative_degreeOf_le line 50
  6. theorem OAI.Erdos3.translationDirectionalDerivative_pow_degreeOf_le line 63
  7. theorem OAI.Erdos3.realPolynomialMass_translationDirectionalDerivative line 73
  8. theorem OAI.Erdos3.realPolynomialMass_translationDirectionalDerivative_pow line 92
  9. theorem OAI.Erdos3.translationDirectionalSeries_coefficient_abs_le_one line 110
  10. theorem OAI.Erdos3.realPolynomialMass_translationDirectionalSeries line 117
  11. theorem OAI.Erdos3.isWeightedHomogeneous_aeval_monomial line 161
  12. theorem OAI.Erdos3.isWeightedHomogeneous_algHom line 174
  13. theorem OAI.Erdos3.weightedHomogeneousComponent_eq_of_sub_lower line 188
  14. theorem OAI.Erdos3.aeval_isWeightedHomogeneous line 205
  15. theorem OAI.Erdos3.aeval_weightedHomogeneousComponent line 214
  16. theorem OAI.Erdos3.isWeightedHomogeneous_mul_pderiv line 240
  17. theorem OAI.Erdos3.translationDirectionalDerivative_isWeightedHomogeneous line 261
  18. theorem OAI.Erdos3.translationDirectionalDerivative_pow_isWeightedHomogeneous line 276
  19. theorem OAI.Erdos3.translationDirectionalSeries_isWeightedHomogeneous line 289
  20. theorem OAI.Erdos3.scaleMvPolynomialAxes_weightedHomogeneousComponent line 310