OAI/Combinatorics/Progressions/Estimates/HomogeneousQuotientSymbolLiftBounds.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart line 14
  2. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_tmul line 18
  3. theorem OAI.Erdos3.VectorPolynomial.coefficients_weightedHomogeneousPart line 23
  4. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_monomial line 37
  5. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_homogeneous line 55
  6. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_eq_self line 60
  7. theorem OAI.Erdos3.VectorPolynomial.coordinate_weightedHomogeneousPart line 71
  8. theorem OAI.Erdos3.VectorPolynomial.map_weightedHomogeneousPart line 81
  9. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedHomogeneousPart line 89
  10. theorem OAI.Erdos3.VectorPolynomial.eval_weightedHomogeneousPart line 102
  11. def OAI.Erdos3.VectorPolynomial.weightedRadialPolynomial line 128
  12. theorem OAI.Erdos3.VectorPolynomial.weightedRadialPolynomial_eval line 134
  13. theorem OAI.Erdos3.VectorPolynomial.weightedRadialPolynomial_coefficient line 149
  14. theorem OAI.Erdos3.VectorPolynomial.weightedRadialPolynomial_eq_zero line 159
  15. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedHomogeneousPart_eq_zero_on line 169
  16. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedHomogeneousPart_eq_on line 180
  17. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedHomogeneousPart_decomposition_on line 193
  18. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedHomogeneousPart_mem_on line 207
  19. def OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial line 238
  20. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_coefficient line 243
  21. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_eval line 252
  22. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_graded line 260
  23. def OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift line 272
  24. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_coordinate line 278
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_homogeneousQuotientSymbolLift line 289
  26. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_eval line 298
  27. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_pure line 308
  28. theorem OAI.Erdos3.linearMap_abs_repr_le line 329
  29. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_coordinateBound line 353
  30. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_coordinateGrid line 367
  31. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.map line 385
  32. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.gradeProjection line 398
  33. theorem OAI.Erdos3.VectorPolynomial.CoefficientGrid.gradeProjection line 408
  34. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.weightedHomogeneousPart line 415
  35. theorem OAI.Erdos3.VectorPolynomial.CoefficientGrid.weightedHomogeneousPart line 422
  36. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_coefficientBound line 437
  37. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_coefficientGrid line 457
  38. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_rational_coefficientGrid line 475
  39. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_rational_coefficientGrid_of_columns line 490
  40. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientGradedPolynomial_rational_coefficientBound line 506
  41. theorem OAI.Erdos3.VectorPolynomial.coefficient_coordinateGrid_of_scalar line 539
  42. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_coordinateBound line 563
  43. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_coordinateGrid line 582
  44. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousQuotientSymbolLift_coordinateGrid_of_scalar line 604