OAI/Combinatorics/Progressions/Geometry/InhomogeneousFullChartLift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection line 16
2. theorem OAI.Erdos3.NilpotentLieFiltration.coefficients_gradedPolynomialProjection line 24
3. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection_mem line 39
4. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection_eq_self line 46
5. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection_degreeLE line 54
6. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection_coefficientBound line 61
7. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfGradedPolynomial_homogeneousChart line 74
8. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialProjection_realChartSubstitute line 115
9. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.exists_graded_degree_bounded_chart line 125
10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_inhomogeneous_chart_lift_algebraic line 198
11. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_inhomogeneous_chart_lift line 246
12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_inhomogeneous_chart_lift line 269
13. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.exists_inhomogeneous_left_lift line 303