OAI/Combinatorics/Progressions/Polynomial/FormalPolynomialCorrectionStep.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.pderiv_map line 15
  2. theorem OAI.Erdos3.VectorPolynomial.pderiv_mem_submodule line 24
  3. theorem OAI.Erdos3.basisGradeProjection_other line 33
  4. theorem OAI.Erdos3.NilpotentLieFiltration.real_sub_horizontal_mem_of_lower_grades line 51
  5. theorem OAI.Erdos3.NilpotentLieFiltration.real_polynomial_derivative_lower_layers line 79
  6. theorem OAI.Erdos3.NilpotentLieFiltration.real_current_layer_polynomial_derivative_equation line 125
  7. theorem OAI.Erdos3.coefficientSubmodule_invariant line 203
  8. theorem OAI.Erdos3.formalLogDerivative_mem_coefficientSubmodule line 223
  9. theorem OAI.Erdos3.dualAdjoint_mem_coefficientSubmodule line 234
  10. theorem OAI.Erdos3.polynomial_derivative_removal_preserves_coefficients line 244
  11. def OAI.Erdos3.gradedPolynomialSubmodule line 280
  12. theorem OAI.Erdos3.monomial_mem_gradedPolynomialSubmodule line 292
  13. def OAI.Erdos3.gradedPolynomialSubalgebra line 302
  14. theorem OAI.Erdos3.homogeneous_mem_gradedPolynomialSubmodule line 322
  15. theorem OAI.Erdos3.gradedPolynomialSubmodule_projection_homogeneous line 332
  16. theorem OAI.Erdos3.bchRemove_mem_gradedPolynomialSubmodule line 342
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_mem_gradedPolynomialSubmodule line 353
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientSubmodule_sup line 386
  19. theorem OAI.Erdos3.VectorPolynomial.coefficients_lie_constant line 409
  20. theorem OAI.Erdos3.VectorPolynomial.polynomialLayer_eq_coefficientSubmodule line 420
  21. theorem OAI.Erdos3.VectorPolynomial.mem_coefficient_sup_polynomialLayer line 425
  22. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbit_log_mul_mem_graded line 449
  23. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbit_log_inv_mem_graded line 456
  24. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbit_log_one_mem_graded line 461
  25. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbit_log_list_prod_mem_graded line 465
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbit_log_mul_mem_graded line 482
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbit_log_inv_mem_graded line 490
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbit_log_one_mem_graded line 495
  29. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbit_log_list_prod_mem_graded line 500
  30. def OAI.Erdos3.shiftedGradedPolynomialSubmodule line 522
  31. theorem OAI.Erdos3.monomial_mem_shiftedGradedPolynomialSubmodule line 535
  32. theorem OAI.Erdos3.shiftedGradedPolynomialSubmodule_invariant line 546
  33. theorem OAI.Erdos3.pderiv_mem_shiftedGradedPolynomialSubmodule line 567
  34. theorem OAI.Erdos3.shiftedGradedPolynomialSubmodule_projection_homogeneous line 577
  35. theorem OAI.Erdos3.shifted_one_projection_homogeneous line 589
  36. theorem OAI.Erdos3.dualAdjoint_mem_shiftedGradedPolynomialSubmodule line 600
  37. theorem OAI.Erdos3.formalLogDerivative_mem_shiftedGradedPolynomialSubmodule line 611
  38. theorem OAI.Erdos3.polynomial_derivative_removal_preserves_shifted_grading line 620
  39. theorem OAI.Erdos3.formal_polynomial_correction_step line 653