OAI/Combinatorics/Progressions/Estimates/GradedNormalizedRelativeLog.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.adaptedGradedEvaluation line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedGradedEvaluation_apply line 27
  3. def OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedEvaluation line 33
  4. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedEvaluation_apply line 43
  5. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedEvaluation_lie line 47
  6. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedEvaluation_constant line 65
  7. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedGradedJet_evaluation line 75
  8. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedGradedEvaluation_logDerivative line 91
  9. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedGradedEvaluation_adjoint line 118
  10. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedGradedPolynomial_one_eq_of_firstJet_eq line 152
  11. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquareSymbol_eq_iff_shiftedGraded line 164
  12. theorem OAI.Erdos3.NilpotentLieFiltration.graded_normalizedRelativeLog line 180