OAI/Combinatorics/Progressions/Estimates/VectorAlgebraicMajorDecomposition.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomialTranslate_comp_ring line 16
  2. theorem OAI.Erdos3.polynomialTranslate_zero_ring line 25
  3. structure OAI.Erdos3.PolynomialTranslationGroupOver line 32
  4. instance OAI.Erdos3.PolynomialTranslationGroupOver.(instance at line 38) line 38
  5. instance OAI.Erdos3.PolynomialTranslationGroupOver.(instance at line 41) line 41
  6. instance OAI.Erdos3.PolynomialTranslationGroupOver.(instance at line 44) line 44
  7. theorem OAI.Erdos3.PolynomialTranslationGroupOver.base_mul line 47
  8. theorem OAI.Erdos3.PolynomialTranslationGroupOver.polynomial_mul line 50
  9. theorem OAI.Erdos3.PolynomialTranslationGroupOver.base_one line 53
  10. theorem OAI.Erdos3.PolynomialTranslationGroupOver.polynomial_one line 54
  11. theorem OAI.Erdos3.PolynomialTranslationGroupOver.base_inv line 55
  12. theorem OAI.Erdos3.PolynomialTranslationGroupOver.polynomial_inv line 56
  13. instance OAI.Erdos3.PolynomialTranslationGroupOver.(instance at line 59) line 59
  14. theorem OAI.Erdos3.PolynomialTranslationGroupOver.algebraic_major_identity line 74
  15. theorem OAI.Erdos3.PolynomialTranslationGroupOver.algebraic_major_decomposition line 101
  16. theorem OAI.Erdos3.PolynomialTranslationGroup.algebraic_major_identity line 115
  17. def OAI.Erdos3.specializeMajorParameters line 144
  18. theorem OAI.Erdos3.specializeMajorParameters_eval line 148
  19. theorem OAI.Erdos3.polynomialTranslate_eval_ring line 158
  20. def OAI.Erdos3.normalizedMajorLeft line 165
  21. def OAI.Erdos3.rationalMajorRight line 170
  22. def OAI.Erdos3.algebraicMajorSymbol line 175
  23. theorem OAI.Erdos3.algebraic_major_normalized_identity line 181
  24. theorem OAI.Erdos3.algebraic_major_normalized_slow_mass line 208
  25. theorem OAI.Erdos3.algebraic_major_normalized_decomposition line 218
  26. theorem OAI.Erdos3.majorFunctionAdd line 265
  27. theorem OAI.Erdos3.majorFunctionSub line 268
  28. theorem OAI.Erdos3.majorFunctionNeg line 271
  29. theorem OAI.Erdos3.PolynomialTranslationGroupOver.algebraic_major_eval_on_subspace line 276
  30. theorem OAI.Erdos3.algebraic_major_normalized_identity_on_subspace line 306
  31. theorem OAI.Erdos3.algebraic_major_normalized_decomposition_on_subspace line 334
  32. theorem OAI.Erdos3.specializeMajorParameters_translatedSlice line 384
  33. theorem OAI.Erdos3.specializeMajorParameters_zero_weightedSupportLE line 413
  34. theorem OAI.Erdos3.VectorPolynomial.exists_vector_algebraic_major_decomposition line 439