OAI/Combinatorics/Progressions/Estimates/GradedUnitEvaluation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedSndMap line 16
  2. def OAI.Erdos3.NilpotentLieFiltration.fastGradedDiagonal line 21
  3. def OAI.Erdos3.NilpotentLieFiltration.fullFastGradedDiagonal line 26
  4. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedDiagonal_top line 31
  5. def OAI.Erdos3.NilpotentLieFiltration.fastPointwiseSquare line 48
  6. theorem OAI.Erdos3.NilpotentLieFiltration.fastGradedDiagonal_graded line 54
  7. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedDiagonal_graded line 63
  8. theorem OAI.Erdos3.NilpotentLieFiltration.fastPointwiseDiagonal_eq line 72
  9. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastPointwise_image_le line 86
  10. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastPointwise_subgroup_le line 102
  11. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastPointwise_eq_comap line 110
  12. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastPointwise_subgroup_eq line 122
  13. theorem OAI.Erdos3.NilpotentLieFiltration.fullFast_horizontal_derivative_mem line 163
  14. theorem OAI.Erdos3.NilpotentLieFiltration.fullFast_horizontal_correction_mem line 177
  15. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPieceProjection_basis line 201
  16. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifference_basis line 222
  17. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference line 232
  18. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_basis line 237
  19. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_projection line 243
  20. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_gradeProjection line 267
  21. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_normalized line 305
  22. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_reducedSquare_symbol line 312
  23. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_reducedSquare_coefficient line 346
  24. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_reducedSquare line 355
  25. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_reducedSquare_homogeneous line 365
  26. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedSnd_coefficient line 377
  27. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_homogeneousSymbolLift line 390
  28. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_unit_eval line 418
  29. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedGradedPolynomialLie_unit_eval line 429
  30. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_normalized_lie line 441
  31. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_unit line 453
  32. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_relative_lie line 461