OAI/Geometry/Coboundary/Polynomial.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-vector leading terms, degree reduction, and normalized rational lattice representatives.

  1. abbrev OAI.CoboundaryExpanders.PolynomialVectors.V line 14
  2. def OAI.CoboundaryExpanders.PolynomialVectors.Leading line 16
  3. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_ne_zero line 19
  4. lemma OAI.CoboundaryExpanders.PolynomialVectors.weight_injective line 24
  5. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_unique line 33
  6. lemma OAI.CoboundaryExpanders.PolynomialVectors.exists_leading line 42
  7. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_monomial line 65
  8. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_smul line 77
  9. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_X_pow line 84
  10. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_add_of_lt line 98
  11. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_cancel line 106
  12. def OAI.CoboundaryExpanders.PolynomialVectors.HasPivots line 136
  13. lemma OAI.CoboundaryExpanders.PolynomialVectors.hasPivots_of_bound line 139
  14. def OAI.CoboundaryExpanders.PolynomialVectors.pivotDegree line 144
  15. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotDegree_min line 147
  16. def OAI.CoboundaryExpanders.PolynomialVectors.pivotRaw line 151
  17. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotRaw_mem line 154
  18. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotRaw_leading line 156
  19. def OAI.CoboundaryExpanders.PolynomialVectors.pivot line 160
  20. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivot_mem line 163
  21. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivot_leading line 166
  22. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivot_monic line 170
  23. lemma OAI.CoboundaryExpanders.PolynomialVectors.span_pivots line 174
  24. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_natDegree_le line 214
  25. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_mul line 224
  26. lemma OAI.CoboundaryExpanders.PolynomialVectors.independent_of_leading line 246
  27. lemma OAI.CoboundaryExpanders.PolynomialVectors.independent_pivots line 280
  28. lemma OAI.CoboundaryExpanders.PolynomialVectors.reflect_sum line 290
  29. lemma OAI.CoboundaryExpanders.PolynomialVectors.polynomial_eq_one_of_dvd_X_pow line 297
  30. def OAI.CoboundaryExpanders.PolynomialVectors.columnReflect line 313
  31. lemma OAI.CoboundaryExpanders.PolynomialVectors.columnReflect_det_eq_one line 316
  32. def OAI.CoboundaryExpanders.PolynomialVectors.pivotMatrix line 353
  33. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotMatrix_right_multiple line 356
  34. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotMatrix_reflect_constant_upper line 379
  35. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotMatrix_reflect_det_constant line 387
  36. theorem OAI.CoboundaryExpanders.PolynomialVectors.pivotMatrix_reflect_det line 397
  37. def OAI.CoboundaryExpanders.RationalLattices.polynomialEmbedding line 411
  38. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialEmbedding_apply line 414
  39. def OAI.CoboundaryExpanders.RationalLattices.polynomialLattice line 417
  40. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_map line 420
  41. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_bound line 435
  42. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialHasPivots line 449
  43. def OAI.CoboundaryExpanders.RationalLattices.diagonalExponents line 454
  44. def OAI.CoboundaryExpanders.RationalLattices.birkhoffSL line 457
  45. lemma OAI.CoboundaryExpanders.RationalLattices.birkhoffSL_constant line 464
  46. lemma OAI.CoboundaryExpanders.RationalLattices.positive_reflect_uniformizer line 479
  47. def OAI.CoboundaryExpanders.RationalLattices.exponentLattice line 486
  48. lemma OAI.CoboundaryExpanders.RationalLattices.birkhoffSL_column line 489
  49. theorem OAI.CoboundaryExpanders.RationalLattices.birkhoff_lattice line 502
  50. lemma OAI.CoboundaryExpanders.PolynomialVectors.span_of_minimal line 524
  51. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotDegree_antitone line 567
  52. lemma OAI.CoboundaryExpanders.PolynomialVectors.eq_of_le_same_pivots line 571
  53. def OAI.CoboundaryExpanders.PolynomialVectors.powerLinear line 578
  54. def OAI.CoboundaryExpanders.PolynomialVectors.powerShift line 583
  55. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_le line 586
  56. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_hasPivots line 590
  57. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotDegree_powerShift line 597
  58. lemma OAI.CoboundaryExpanders.PolynomialVectors.interval_pivot_increment line 620
  59. def OAI.CoboundaryExpanders.PolynomialVectors.incrementSet line 628
  60. lemma OAI.CoboundaryExpanders.PolynomialVectors.incrementSet_mono line 631
  61. lemma OAI.CoboundaryExpanders.PolynomialVectors.interval_incrementSet_eq_iff line 639
  62. theorem OAI.CoboundaryExpanders.PolynomialVectors.simultaneous_minimal_basis line 662
  63. lemma OAI.CoboundaryExpanders.PolynomialVectors.matrix_right_multiple_of_span line 720
  64. lemma OAI.CoboundaryExpanders.PolynomialVectors.monic_reflect_det line 744
  65. lemma OAI.CoboundaryExpanders.PolynomialVectors.full_chain_permutation line 770
  66. theorem OAI.CoboundaryExpanders.PolynomialVectors.full_flag_increment_permutation line 823
  67. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_weight_bound line 848
  68. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_pivot_natDegree line 855
  69. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_mulVec line 859
  70. lemma OAI.CoboundaryExpanders.PolynomialVectors.reflected_columns_leading line 901
  71. def OAI.CoboundaryExpanders.PolynomialVectors.matrixLinear line 925
  72. lemma OAI.CoboundaryExpanders.PolynomialVectors.image_hasPivots line 928
  73. theorem OAI.CoboundaryExpanders.PolynomialVectors.pivotDegree_image line 937
  74. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_mono line 968
  75. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_power_le line 972
  76. theorem OAI.CoboundaryExpanders.RationalLattices.lattice_flag_birkhoff line 983