OAI/Combinatorics/Progressions/Polynomial/RealPolynomialChartSubstitution.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.dualScalarEval line 16
  2. theorem OAI.Erdos3.dualScalarEval_X line 19
  3. theorem OAI.Erdos3.dualScalarEval_fst line 24
  4. theorem OAI.Erdos3.dualScalarEval_snd line 31
  5. def OAI.Erdos3.VectorPolynomial.dualEvalLie line 50
  6. theorem OAI.Erdos3.VectorPolynomial.dualEvalLie_tmul line 53
  7. theorem OAI.Erdos3.VectorPolynomial.dualEvalLie_base line 56
  8. def OAI.Erdos3.VectorPolynomial.directionalDerivative line 62
  9. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_tmul line 66
  10. theorem OAI.Erdos3.VectorPolynomial.dualEvalLie_tangent line 72
  11. theorem OAI.Erdos3.VectorPolynomial.dualEvalLie_eq_value_add_derivative line 80
  12. theorem OAI.Erdos3.VectorPolynomial.pderiv_lie line 100
  13. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_lie line 120
  14. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_direction_add line 130
  15. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_direction_smul line 136
  16. abbrev OAI.Erdos3.NilpotentLieBCHGroup.PolynomialGroup line 155
  17. def OAI.Erdos3.NilpotentLieBCHGroup.polynomialValueHom line 158
  18. def OAI.Erdos3.NilpotentLieBCHGroup.polynomialFirstJetHom line 162
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.polynomialFirstJet_base line 165
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.polynomialFirstJet_coord line 170
  21. def OAI.Erdos3.NilpotentLieBCHGroup.polynomialLogDerivative line 175
  22. theorem OAI.Erdos3.NilpotentLieBCHGroup.polynomialLogDerivative_mul line 178
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.polynomialLogDerivative_triple line 183
  24. theorem OAI.Erdos3.NilpotentLieBCHGroup.polynomialFirstJet_insertion_identity line 189
  25. def OAI.Erdos3.NilpotentLieBCHGroup.formalPolynomialJetLie line 209
  26. def OAI.Erdos3.NilpotentLieBCHGroup.formalPolynomialJetHom line 227
  27. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalPolynomialJet_base line 231
  28. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalPolynomialJet_tangent line 237
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalPolynomialJet_baseHom line 244
  30. def OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative line 248
  31. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative_mul line 251
  32. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative_one line 256
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative_inv line 260
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative_remove line 264
  35. theorem OAI.Erdos3.NilpotentLieBCHGroup.formalLogDerivative_mem_of_invariant line 272
  36. def OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystem line 283
  37. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystem.remove line 287
  38. def OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialValueHom line 314
  39. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialValueHom_coord line 318
  40. def OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialJet line 321
  41. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialJet_base line 326
  42. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialJet_tangent line 331
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialJet_baseHom line 337
  44. theorem OAI.Erdos3.NilpotentLieBCHGroup.eval₂_formalLogDerivative line 341
  45. theorem OAI.Erdos3.NilpotentLieBCHGroup.eval₂_dualAdjoint line 350
  46. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystem.real_evaluation line 357
  47. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystem.of_real_evaluation line 365
  48. def OAI.Erdos3.VectorPolynomial.realCoefficientEquiv line 390
  49. theorem OAI.Erdos3.VectorPolynomial.coefficients_realCoefficientEquiv line 395
  50. theorem OAI.Erdos3.VectorPolynomial.coefficients_realCoefficientEquiv_symm line 399
  51. theorem OAI.Erdos3.VectorPolynomial.realCoefficientEquiv_monomial line 403
  52. theorem OAI.Erdos3.VectorPolynomial.eval_realCoefficientEquiv line 408
  53. theorem OAI.Erdos3.VectorPolynomial.eval₂_realCoefficientEquiv_symm line 414
  54. def OAI.Erdos3.VectorPolynomial.realChartSubstitute line 419
  55. theorem OAI.Erdos3.VectorPolynomial.coefficients_realChartSubstitute line 424
  56. theorem OAI.Erdos3.VectorPolynomial.eval₂_realChartSubstitute line 434
  57. theorem OAI.Erdos3.VectorPolynomial.realChartSubstitute_comp line 442
  58. theorem OAI.Erdos3.VectorPolynomial.realChartSubstitute_X line 459
  59. theorem OAI.Erdos3.VectorPolynomial.eval₂_normalizedRealPolynomialChart line 466
  60. theorem OAI.Erdos3.VectorPolynomial.realChartSubstitute_lie line 481
  61. def OAI.Erdos3.VectorPolynomial.lieHomOfLinearMap line 497
  62. def OAI.Erdos3.VectorPolynomial.realChartSubstituteLie line 502
  63. def OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution line 516
  64. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_coord line 520
  65. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_mul line 524
  66. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_list_prod line 530
  67. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_foldl line 536
  68. theorem OAI.Erdos3.NilpotentLieBCHGroup.realPolynomialChartSubstitution_value line 547