OAI/Combinatorics/Progressions/Polynomial/FullChartPolynomialLiftControl.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.realChartSubstitute_sharp line 14
  2. def OAI.Erdos3.VectorPolynomial.weightedDegreeTruncate line 60
  3. theorem OAI.Erdos3.VectorPolynomial.coefficients_weightedDegreeTruncate line 64
  4. theorem OAI.Erdos3.VectorPolynomial.degreeLE_weightedDegreeTruncate line 71
  5. theorem OAI.Erdos3.VectorPolynomial.weightedDegreeTruncate_eq_self line 76
  6. theorem OAI.Erdos3.VectorPolynomial.degreeLE_one_weightedDegreeTruncate line 87
  7. theorem OAI.Erdos3.VectorPolynomial.realChartSubstitute_weightedDegreeTruncate line 101
  8. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.weightedDegreeTruncate line 114
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_truncate_of_degreeLE line 137
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_degreeLE line 158
  11. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.exists_degree_bounded_chart line 174
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolLift_coordinate line 232
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolLift_slow_iff line 242
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolLift_rationalGrid_iff line 250
  15. theorem OAI.Erdos3.NilpotentLieFiltration.coefficientBound_gradedBasisSplitting line 264
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolLift_chart_pullback_bound line 277
  17. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.exists_fullPolynomial_lifts line 309
  18. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.restricted_left_slowBound line 346