OAI/Combinatorics/Progressions/Polynomial/PolynomialTranslationSeries.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialExponentialPath line 20
  2. theorem OAI.Erdos3.polynomialExponentialPath_derivative line 24
  3. theorem OAI.Erdos3.polynomialExponentialPath_eval_zero line 29
  4. theorem OAI.Erdos3.polynomialExponentialPath_unique line 33
  5. theorem OAI.Erdos3.polynomialExponentialPath_potential line 39
  6. theorem OAI.Erdos3.polynomialExponentialPath_eval_potential line 48
  7. def OAI.Erdos3.polynomialExponentialCoordinate line 55
  8. theorem OAI.Erdos3.polynomialExponentialCoordinate_formula line 59
  9. theorem OAI.Erdos3.polynomialExponentialCoordinate_potential line 68
  10. theorem OAI.Erdos3.weightedPolynomialPotential_exponentialCoordinate line 77
  11. theorem OAI.Erdos3.polynomialTranslationPath_zero line 101
  12. theorem OAI.Erdos3.polynomialExponentialPath_C line 108
  13. theorem OAI.Erdos3.polynomialExponentialPath_zero line 112
  14. theorem OAI.Erdos3.polynomialExponentialCoordinate_C line 116
  15. theorem OAI.Erdos3.polynomialExponentialCoordinate_zero line 120
  16. theorem OAI.Erdos3.polynomialTranslationPath_translate_reflection line 136
  17. theorem OAI.Erdos3.polynomialExponentialPath_translate_reflection line 154
  18. theorem OAI.Erdos3.polynomialTranslate_exponentialCoordinate line 170
  19. theorem OAI.Erdos3.polynomialTranslate_comp line 194
  20. structure OAI.Erdos3.PolynomialTranslationGroup line 204
  21. instance OAI.Erdos3.PolynomialTranslationGroup.(instance at line 210) line 210
  22. instance OAI.Erdos3.PolynomialTranslationGroup.(instance at line 213) line 213
  23. instance OAI.Erdos3.PolynomialTranslationGroup.(instance at line 216) line 216
  24. theorem OAI.Erdos3.PolynomialTranslationGroup.base_mul line 219
  25. theorem OAI.Erdos3.PolynomialTranslationGroup.polynomial_mul line 222
  26. theorem OAI.Erdos3.PolynomialTranslationGroup.base_one line 225
  27. theorem OAI.Erdos3.PolynomialTranslationGroup.polynomial_one line 226
  28. theorem OAI.Erdos3.PolynomialTranslationGroup.base_inv line 227
  29. theorem OAI.Erdos3.PolynomialTranslationGroup.polynomial_inv line 228
  30. instance OAI.Erdos3.PolynomialTranslationGroup.(instance at line 231) line 231
  31. def OAI.Erdos3.PolynomialTranslationGroup.potentialElement line 246
  32. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_base line 249
  33. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_polynomial line 252
  34. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_zero line 255
  35. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_add line 259
  36. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_neg line 267
  37. def OAI.Erdos3.PolynomialTranslationGroup.potentialSubgroup line 275
  38. theorem OAI.Erdos3.PolynomialTranslationGroup.mem_potentialSubgroup line 288
  39. def OAI.Erdos3.PolynomialTranslationGroup.exponentialElement line 297
  40. theorem OAI.Erdos3.PolynomialTranslationGroup.exponentialElement_potential line 300
  41. def OAI.Erdos3.PolynomialTranslationGroup.potentialFlow line 306
  42. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialFlow_eq line 310
  43. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialFlow_zero line 318
  44. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialFlow_add line 322
  45. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialFlow_initial_tangent line 326
  46. theorem OAI.Erdos3.PolynomialTranslationGroup.potential_identity_of_mem_closure line 331
  47. structure OAI.Erdos3.PolynomialPotentialRelation line 358
  48. theorem OAI.Erdos3.scalarDirectionalDerivative_zero line 364
  49. theorem OAI.Erdos3.scalarDirectionalDerivative_single line 368
  50. theorem OAI.Erdos3.PolynomialPotentialRelation.pure_eq_zero line 381
  51. theorem OAI.Erdos3.PolynomialPotentialRelation.compatible_partials line 390
  52. theorem OAI.Erdos3.PolynomialPotentialRelation.linear_combination_mem line 395
  53. theorem OAI.Erdos3.PolynomialPotentialRelation.polynomial_eq_linear_combination line 405
  54. theorem OAI.Erdos3.PolynomialPotentialRelation.weighted_potential_derivative line 411
  55. theorem OAI.Erdos3.PolynomialPotentialRelation.exists_weighted_potential line 421
  56. theorem OAI.Erdos3.PolynomialPotentialRelation.exponential_potential_identity line 429
  57. def OAI.Erdos3.PolynomialTranslationGroup.actionHom line 450
  58. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_X_inl line 455
  59. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_X_inr line 458
  60. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_C line 462
  61. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_rename line 465
  62. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_one line 473
  63. theorem OAI.Erdos3.PolynomialTranslationGroup.actionHom_mul line 480
  64. def OAI.Erdos3.PolynomialTranslationGroup.action line 495
  65. def OAI.Erdos3.PolynomialTranslationGroup.actionMonoidHom line 506
  66. theorem OAI.Erdos3.PolynomialTranslationGroup.actionMonoidHom_injective line 512
  67. theorem OAI.Erdos3.scalarDirectionalDerivative_neg line 543
  68. theorem OAI.Erdos3.polynomialTranslationPath_neg_derivative line 549
  69. theorem OAI.Erdos3.polynomialTranslationPath_neg_coeff line 555
  70. theorem OAI.Erdos3.scalarDirectionalDerivative_pow_eq_zero_of_weightedSupport line 581
  71. theorem OAI.Erdos3.polynomialTranslationPath_neg_support_of_nilpotent line 593
  72. theorem OAI.Erdos3.polynomialExponentialCoordinate_neg_series_of_nilpotent line 606