OAI/Combinatorics/Progressions/Lattices/AlgebraicMajorWeightedAffineTopPullback.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.majorSlowDilationPullback line 14
  2. theorem OAI.Erdos3.majorSlowDilationPullback_eval line 19
  3. theorem OAI.Erdos3.majorSlowDilationPullback_totalDegree_le line 33
  4. theorem OAI.Erdos3.algebraic_major_dilation_pullback_identity line 38
  5. theorem OAI.Erdos3.majorSlowDilationPullback_mass_le line 60
  6. theorem OAI.Erdos3.algebraic_major_dilation_pullback_decomposition line 72
  7. theorem OAI.Erdos3.majorSlowDilationPullback_mem_weightedSupportLE line 113
  8. theorem OAI.Erdos3.algebraic_major_weighted_dilation_pullback_decomposition line 119
  9. theorem OAI.Erdos3.homogeneousComponent_polynomialTranslate line 176
  10. theorem OAI.Erdos3.polynomial_dilation_monomial line 191
  11. theorem OAI.Erdos3.coeff_polynomial_dilation line 203
  12. theorem OAI.Erdos3.homogeneousComponent_polynomial_dilation line 221
  13. theorem OAI.Erdos3.residueAffinePolynomial_eq_dilation_translate line 233
  14. theorem OAI.Erdos3.residueAffinePolynomial_homogeneousComponent line 246
  15. theorem OAI.Erdos3.residueAffinePolynomial_homogeneousComponent_eval line 265
  16. theorem OAI.Erdos3.residueAffinePolynomial_weightedHomogeneousComponent_eval line 285
  17. def OAI.Erdos3.jointResidueAffinePolynomial line 306
  18. theorem OAI.Erdos3.jointResidueAffinePolynomial_eval line 311
  19. theorem OAI.Erdos3.jointResidueAffine_variables_degree line 321
  20. theorem OAI.Erdos3.jointResidueAffinePolynomial_degree line 334
  21. theorem OAI.Erdos3.jointResidueAffinePolynomial_sub_axes_lower line 341
  22. theorem OAI.Erdos3.jointResidueAffinePolynomial_weightedHomogeneousComponent line 371
  23. theorem OAI.Erdos3.jointResidueAffinePolynomial_weightedHomogeneousComponent_eval line 397
  24. theorem OAI.Erdos3.algebraic_major_affine_top_dilation_identity line 412
  25. theorem OAI.Erdos3.algebraic_major_affine_top_pullback_decomposition line 439
  26. theorem OAI.Erdos3.algebraic_major_weighted_affine_top_pullback_decomposition line 484