OAI/Combinatorics/Progressions/Polynomial/RealPositivePolynomialEvaluation.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialAlgebra line 18
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_positivePolynomialAlgebra line 30
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_coefficient_mem line 33
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_constant line 36
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_support line 39
  6. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialEvaluation line 48
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialEvaluation_apply line 51
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_lowerCentralSeries_eq_bot line 54
  9. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialComponent line 74
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialComponent_coe line 93
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.sum_positivePolynomialComponent line 96
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialComponent_support line 105
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialEvaluation_component line 109
  14. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer line 128
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer_antitone line 133
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer_one line 137
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer_lie line 150
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer_terminal line 160
  19. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeFiltration line 176
  20. abbrev OAI.Erdos3.MultidegreeLieFiltration.BoxedDegreeIndex line 198
  21. def OAI.Erdos3.MultidegreeLieFiltration.boxedDegreeMonomial line 200
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedDegreeMonomial_apply line 203
  23. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialCoordinates line 210
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialCoordinates_injective line 216
  25. instance OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialFiniteDimensional line 234
  26. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_finrank_le line 238
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_finrank_le_total line 248
  28. def OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMap line 271
  29. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMap_coefficient_tmul line 276
  30. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMap_adapted line 282
  31. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMap_constant line 293
  32. def OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialTensor line 300
  33. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialTensor_coe line 309
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialTensor_injective line 312
  35. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeLayer line 332
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeLayer_antitone line 337
  37. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeLayer_zero line 342
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeLayer_lie line 347
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeLayer_terminal line 357
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialComponent_mem_layer line 371
  41. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeLayer_eq line 378
  42. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegree line 402
  43. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialEvaluation_mem_layer line 412
  44. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedDegreeMonomial_injective line 440
  45. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedDegreeMonomial_le line 446
  46. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_boxedDegreeMonomial line 453
  47. def OAI.Erdos3.MultidegreeLieFiltration.boxedPolynomial line 459
  48. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedPolynomial_coefficient line 463
  49. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedPolynomial_coefficient_outside line 468
  50. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialComponent_eq_zero line 491
  51. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal line 505
  52. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal_coefficient line 509
  53. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal_adapted line 518
  54. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal_constant line 524
  55. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal_projection line 529
  56. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDiagonal_eval line 537
  57. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_support_of_layers line 555
  58. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialLayer_le_outsideDownset line 564
  59. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetQuotient line 575
  60. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetQuotient_terminal line 580
  61. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_downset_pair_injective line 586
  62. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_positivePolynomial_orbit line 606
  63. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialEvaluation_commute line 643