OAI/Combinatorics/Progressions/Estimates/RealSymbolGradeQuotientSplitting.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realifyFunctional_eq_sum_basis line 14
  2. def OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial line 33
  3. theorem OAI.Erdos3.NilpotentLieFiltration.coeff_scalarSymbolPolynomial line 38
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_slow_coordinates line 45
  5. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_slow_coefficients line 58
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_rational_coordinates line 82
  7. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_rational_coefficients line 101
  8. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_slow_coefficients_of_height line 118
  9. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_exists_coefficient_grid line 129
  10. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_mul line 156
  11. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_eq_zero_of_fast line 172
  12. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_approximation_of_factorization line 184
  13. theorem OAI.Erdos3.real_quotient_section_residual line 227
  14. theorem OAI.Erdos3.real_graded_quotient_section_residual line 247
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeEvaluation_quotientLift line 268
  16. theorem OAI.Erdos3.NilpotentLieFiltration.restricted_symbol_grade_terminal line 280
  17. theorem OAI.Erdos3.NilpotentLieFiltration.restricted_symbol_grade_matching line 305
  18. def OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial line 394
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_eval line 402
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_homogeneous line 409
  21. theorem OAI.Erdos3.NilpotentLieFiltration.restricted_symbol_major_grade_step line 416
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_gradeProjection_eq_weightedHomogeneousPart line 477
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_quotient_eq_zero_of_fast line 504
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_normalized_splitting line 521
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_coordinate_normalized_splitting line 551
  26. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_weightedComponent_normalized_splitting line 569
  27. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_homogeneous_normalized_splitting line 607