OAI/Combinatorics/Progressions/Polynomial/AdaptedBinomialFactorization.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialSupportBox line 20
  2. theorem OAI.Erdos3.monomial_mem_polynomialSupportBox line 33
  3. theorem OAI.Erdos3.polynomialSupportBox_mono line 40
  4. theorem OAI.Erdos3.mul_mem_polynomialSupportBox line 44
  5. theorem OAI.Erdos3.prod_mem_polynomialSupportBox line 52
  6. theorem OAI.Erdos3.finsupp_weight_mono line 66
  7. theorem OAI.Erdos3.weightedDegree_le_of_mem_polynomialSupportBox line 72
  8. theorem OAI.Erdos3.polynomial_aeval_X_mem_supportBox line 79
  9. def OAI.Erdos3.binomialVariable line 107
  10. theorem OAI.Erdos3.binomialVariable_zero line 110
  11. def OAI.Erdos3.multivariateBinomial line 113
  12. theorem OAI.Erdos3.multivariateBinomial_zero line 116
  13. theorem OAI.Erdos3.multivariateBinomial_single line 119
  14. theorem OAI.Erdos3.multivariateBinomial_add_of_disjoint line 124
  15. theorem OAI.Erdos3.binomialVariable_mem_supportBox line 129
  16. theorem OAI.Erdos3.multivariateBinomial_mem_supportBox line 133
  17. theorem OAI.Erdos3.multivariateBinomial_weightedDegree line 140
  18. theorem OAI.Erdos3.binomialVariable_eval_nat line 144
  19. theorem OAI.Erdos3.multivariateBinomial_eval_nat line 149
  20. theorem OAI.Erdos3.binomialPolynomial_aeval_choose line 164
  21. theorem OAI.Erdos3.binomialPolynomial_eval_int line 175
  22. theorem OAI.Erdos3.multivariateBinomial_aeval_choose line 181
  23. theorem OAI.Erdos3.multivariateBinomial_eval_int line 187
  24. def OAI.Erdos3.binomialSpan line 207
  25. theorem OAI.Erdos3.multivariateBinomial_mem_binomialSpan line 210
  26. theorem OAI.Erdos3.binomialSpan_mono line 214
  27. theorem OAI.Erdos3.mul_mem_binomialSpan_of_disjoint line 217
  28. theorem OAI.Erdos3.monomial_single_mem_binomialSpan line 235
  29. theorem OAI.Erdos3.monomial_mem_binomialSpan line 251
  30. theorem OAI.Erdos3.binomialSpan_eq_supportBox line 266
  31. def OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval line 294
  32. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval_coord line 299
  33. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval_integer line 303
  34. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval_coordinates line 311
  35. theorem OAI.Erdos3.NilpotentLieFiltration.contMDiff_polynomialOrbitRealEval line 323
  36. theorem OAI.Erdos3.NilpotentLieFiltration.real_adapted_iff_quotient_coordinates line 350
  37. structure OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial line 374
  38. def OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.logarithm line 383
  39. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.coe_logarithm line 387
  40. def OAI.Erdos3.NilpotentLieFiltration.adaptedBCHToOrbit line 392
  41. def OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.orbit line 402
  42. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.orbit_log line 405
  43. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.eval_coord line 408
  44. theorem OAI.Erdos3.NilpotentLieFiltration.exists_layerwise_monomial_sum line 415
  45. theorem OAI.Erdos3.NilpotentLieFiltration.exists_monomial_factorization line 440
  46. theorem OAI.Erdos3.NilpotentLieFiltration.exists_monomial_factorization_eval line 456
  47. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedMonomial.evalReal_coord line 468
  48. theorem OAI.Erdos3.NilpotentLieFiltration.exists_monomial_factorization_evalReal line 474
  49. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbitChangeFiltration line 499
  50. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbitChangeFiltration_log line 503
  51. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbitChangeFiltration_realEval line 507
  52. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialOrbitChangeFiltration_eval line 515
  53. theorem OAI.Erdos3.NilpotentLieFiltration.tensor_adapted_of_supportBox line 537
  54. theorem OAI.Erdos3.NilpotentLieFiltration.tensor_mem_polynomialLayer line 548
  55. structure OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial line 554
  56. def OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.logarithm line 563
  57. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.coe_logarithm line 569
  58. def OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.scale line 573
  59. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.logarithm_scale line 578
  60. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.logarithm_mem_layer line 585
  61. def OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.orbit line 590
  62. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.orbit_log line 593
  63. def OAI.Erdos3.NilpotentLieFiltration.binomialLayerGenerators line 611
  64. theorem OAI.Erdos3.NilpotentLieFiltration.smul_mem_binomialLayerGenerators line 614
  65. theorem OAI.Erdos3.NilpotentLieFiltration.monomial_mem_binomialLayerSpan line 622
  66. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_mem_binomialLayerSpan line 635
  67. theorem OAI.Erdos3.NilpotentLieFiltration.exists_layerwise_binomial_sum line 644
  68. theorem OAI.Erdos3.NilpotentLieFiltration.exists_binomial_factorization line 685
  69. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_iff_binomial_factorization line 701
  70. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.eval_coord line 712
  71. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.eval_eq_choose line 718
  72. theorem OAI.Erdos3.NilpotentLieFiltration.exists_binomial_factorization_eval line 725
  73. theorem OAI.Erdos3.NilpotentLieFiltration.exists_integer_binomial_factorization line 733
  74. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.evalReal_coord line 743
  75. theorem OAI.Erdos3.NilpotentLieFiltration.AdaptedBinomial.evalReal_eq_choose line 749
  76. theorem OAI.Erdos3.NilpotentLieFiltration.exists_binomial_factorization_evalReal line 756
  77. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_binomial_factorization line 765