OAI/Combinatorics/Progressions/Polynomial/JointPolynomialDilationGrid.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scaleMvPolynomialAxes line 15
  2. theorem OAI.Erdos3.scaleMvPolynomialAxes_coeff line 19
  3. theorem OAI.Erdos3.scaleMvPolynomialAxes_support_subset line 29
  4. theorem OAI.Erdos3.scaleMvPolynomialAxes_totalDegree_le line 35
  5. theorem OAI.Erdos3.scaleMvPolynomialAxes_eval line 39
  6. theorem OAI.Erdos3.scaleMvPolynomialAxes_mass_le line 50
  7. theorem OAI.Erdos3.abs_monomialScale_le_pow line 71
  8. theorem OAI.Erdos3.scaleMvPolynomialAxes_mass_le_of_abs_le line 85
  9. theorem OAI.Erdos3.jointPolynomialDilation_mass_le line 104
  10. theorem OAI.Erdos3.abs_prod_sub_prod_unit_sum line 122
  11. theorem OAI.Erdos3.abs_eval_sub_eval_unit_mass_bound line 157
  12. theorem OAI.Erdos3.abs_eval_sub_eval_normalized_mass_bound line 195
  13. theorem OAI.Erdos3.scaleMvPolynomialAxes_eq_aeval line 227
  14. theorem OAI.Erdos3.scaleMvPolynomialAxes_mem_weightedSupportLE line 238
  15. theorem OAI.Erdos3.rationalAxisScaling_map_real line 245
  16. theorem OAI.Erdos3.rationalAxisScaling_support_subset line 256
  17. theorem OAI.Erdos3.rationalAxisScaling_totalDegree_le line 274
  18. theorem OAI.Erdos3.rationalAxisScaling_mem_weightedSupportLE line 280
  19. theorem OAI.Erdos3.jointPolynomialDilation_coefficientGrid line 297
  20. theorem OAI.Erdos3.jointPolynomialDilation_totalDegree_le line 316
  21. def OAI.Erdos3.jointRationalPolynomialDilation line 322
  22. theorem OAI.Erdos3.jointRationalPolynomialDilation_map line 326
  23. theorem OAI.Erdos3.jointRationalPolynomialDilation_eval₂ line 335
  24. theorem OAI.Erdos3.jointRationalPolynomialDilation_totalDegree_le line 344
  25. theorem OAI.Erdos3.jointRationalPolynomialDilation_denominatorGrid line 349
  26. theorem OAI.Erdos3.jointRationalPolynomialDilation_mem_weightedSupportLE line 365