OAI/Combinatorics/Progressions/Estimates/RealSymbolGradedCoefficientBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_iff_gradedCoefficientBound line 19
2. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_homogeneousPullback line 29
3. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_homogeneousPullback_coord line 40
4. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_homogeneousPullback_of_coefficientBound line 50
5. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_homogeneousPullback_of_chart line 61
6. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.homogeneousPullback_slow line 75