OAI/Combinatorics/Progressions/Estimates/ProjectedPointwiseCoefficient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialSymbol line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialSymbol_coordinate line 23
  3. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPolynomialSymbol_gradedSymbolPolynomial line 32
  4. def OAI.Erdos3.NilpotentLieFiltration.homogeneousSymbolLift line 38
  5. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousSymbolLift_apply line 43
  6. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousSymbolLift_coordinate line 49
  7. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_homogeneousSymbolLift line 56
  8. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousSymbolLift_coefficient line 81
  9. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_coefficient_symbol line 110
  10. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_filteredMap_coefficient line 134
  11. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_filteredMap line 144
  12. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_basis_repr line 153
  13. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_gradeProjection line 164
  14. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousSymbolLift_filteredMap line 174
  15. theorem OAI.Erdos3.NilpotentLieFiltration.symbol_mem_pointwise_iff_refiltered_coefficients line 200
  16. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedHorizontalSymbolCoefficient_mem line 221
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.real_projectedHorizontalSymbolCoefficient_mem line 236