OAI/Combinatorics/Progressions/Estimates/ShiftedGradedCalculus.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.NilpotentLieFiltration.FilteredFirstJet line 16
  2. def OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetMap line 18
  3. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetMap_surjective line 21
  4. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetMap_eq_zero_iff line 24
  5. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetMap_eq_iff line 28
  6. def OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetSymbol line 34
  7. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetSymbol_map line 46
  8. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetSymbol_surjective line 49
  9. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_kernel_lie_eq_zero line 54
  10. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_lowerCentralSeries_eq_bot line 69
  11. abbrev OAI.Erdos3.NilpotentLieFiltration.FilteredFirstJetGroup line 73
  12. def OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetHom line 76
  13. def OAI.Erdos3.NilpotentLieFiltration.filteredFirstJetSymbolHom line 79
  14. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_kernel_mul line 82
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.common_derivative_identity line 100
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.common_derivative_mod_submodule line 118
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.common_derivative_difference line 129
  18. theorem OAI.Erdos3.VectorPolynomial.coefficients_pderiv line 152
  19. theorem OAI.Erdos3.VectorPolynomial.coefficients_directionalDerivative line 166
  20. theorem OAI.Erdos3.NilpotentLieFiltration.directionalDerivative_mem_shifted line 182
  21. theorem OAI.Erdos3.NilpotentLieFiltration.directionalDerivative_mem_next line 194
  22. theorem OAI.Erdos3.NilpotentLieBCHGroup.common_derivative_defect line 213
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.common_derivative_mod_of_defect line 225
  24. def OAI.Erdos3.VectorPolynomial.taylorRemainder line 251
  25. theorem OAI.Erdos3.VectorPolynomial.taylorRemainder_apply line 255
  26. theorem OAI.Erdos3.VectorPolynomial.coefficients_taylorRemainder_monomial line 267
  27. theorem OAI.Erdos3.VectorPolynomial.coefficients_taylorRemainder line 273
  28. theorem OAI.Erdos3.NilpotentLieFiltration.taylorRemainder_mem_shifted line 288
  29. def OAI.Erdos3.NilpotentLieFiltration.adaptedDirectionalDerivative line 319
  30. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedDirectionalDerivative_coe line 326
  31. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedDirectionalDerivative_mem_shifted line 329
  32. def OAI.Erdos3.NilpotentLieFiltration.symbolFirstDerivative line 335
  33. theorem OAI.Erdos3.NilpotentLieFiltration.symbolFirstDerivative_map line 343
  34. theorem OAI.Erdos3.NilpotentLieFiltration.symbolFirstDerivative_in_kernel line 347
  35. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_translate line 354
  36. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_constant_eq line 385
  37. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_normalizedShift line 393
  38. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJet line 439
  39. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJet_base line 443
  40. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJet_tangent line 448
  41. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJet_baseHom line 453
  42. def OAI.Erdos3.NilpotentLieFiltration.normalizedShiftAdapted line 459
  43. def OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeLog line 465
  44. def OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative line 469
  45. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_normalizedRelativeLog line 472
  46. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedDirectionalDerivative_lie line 522
  47. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJetLie line 528
  48. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJetHom line 546
  49. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialJetHom_apply line 551
  50. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_mul line 555
  51. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_triple line 564
  52. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_common_derivative_identity line 571
  53. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_common_derivative_mod_submodule line 582
  54. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_tangent line 605
  55. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_constant line 619
  56. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_constant_unit line 643
  57. def OAI.Erdos3.NilpotentLieFiltration.adaptedDirectionalTangent line 665
  58. def OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivativeLinear line 672
  59. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivativeLinear_apply line 679
  60. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_direction_sub line 683
  61. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_common_derivative_difference line 688
  62. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPieceProjection_lie line 713
  63. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedGradedPolynomial_lie line 725
  64. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedGradedPolynomial_directionalDerivative line 742