OAI/Combinatorics/Progressions/Polynomial/PolynomialPatchShearOrbit.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialSubstitutionPoint line 15
  2. theorem OAI.Erdos3.polynomialSubstitutionPoint_aeval line 19
  3. theorem OAI.Erdos3.polynomialSubstitutionPoint_comp line 25
  4. def OAI.Erdos3.polynomialPointEquiv line 32
  5. theorem OAI.Erdos3.polynomialPointEquiv_apply line 49
  6. def OAI.Erdos3.polynomialPointAction line 53
  7. def OAI.Erdos3.weightedLoweringPointAction line 66
  8. theorem OAI.Erdos3.polynomial_map_aeval line 70
  9. theorem OAI.Erdos3.integerCoefficientPolynomials_aeval line 88
  10. theorem OAI.Erdos3.integerTupleRatCast_injective line 94
  11. def OAI.Erdos3.integerWeightedLoweringPoint line 101
  12. theorem OAI.Erdos3.integerWeightedLoweringPoint_cast line 106
  13. theorem OAI.Erdos3.integerWeightedLoweringPoint_inv line 114
  14. def OAI.Erdos3.integerWeightedLoweringPointEquiv line 124
  15. theorem OAI.Erdos3.integerWeightedLoweringPointEquiv_cast line 136
  16. theorem OAI.Erdos3.polynomialShear_integral_iff line 154
  17. theorem OAI.Erdos3.polynomialShear_integralVector_iff line 173
  18. theorem OAI.Erdos3.polynomialShear_denominatorGrid_iff line 184
  19. theorem OAI.Erdos3.polynomialShear_scaledGrid_normalize line 191
  20. theorem OAI.Erdos3.polynomialShearMonomial_pderiv line 214
  21. theorem OAI.Erdos3.polynomialShearMonomial_monomial line 228
  22. theorem OAI.Erdos3.polynomialShearMonomial_bracket_X line 236
  23. def OAI.Erdos3.polynomialShearBracketCoefficient line 246
  24. theorem OAI.Erdos3.polynomialShear_structureConstants line 255
  25. theorem OAI.Erdos3.polynomialShearBracketCoefficient_natAbs_le line 267
  26. theorem OAI.Erdos3.polynomialShear_structureConstants_height line 284
  27. def OAI.Erdos3.polynomialShearLattice line 306
  28. theorem OAI.Erdos3.mem_polynomialShearLattice line 310
  29. theorem OAI.Erdos3.polynomialShearLattice_inner_grid line 317
  30. theorem OAI.Erdos3.polynomialShearLattice_outer_grid line 330
  31. def OAI.Erdos3.polynomialShearRealLattice line 341
  32. theorem OAI.Erdos3.polynomialShearRealLattice_closed_discrete line 350
  33. theorem OAI.Erdos3.polynomialShearRealLattice_quotient_compact line 357
  34. def OAI.Erdos3.polynomialShearIndexOrder line 375
  35. def OAI.Erdos3.polynomialShearOrderedBasis line 381
  36. def OAI.Erdos3.polynomialShearOrderedWeight line 385
  37. theorem OAI.Erdos3.polynomialShearOrderedWeight_monotone line 389
  38. theorem OAI.Erdos3.polynomialShearOrderedWeight_pos line 393
  39. theorem OAI.Erdos3.polynomialShearOrderedWeight_le line 397
  40. theorem OAI.Erdos3.polynomialShearOrderedBasis_layers line 401
  41. theorem OAI.Erdos3.polynomialShearOrderedBasis_central line 409
  42. theorem OAI.Erdos3.polynomialShearOrderedBasis_structure_height line 415
  43. theorem OAI.Erdos3.polynomialShearOrderedBasis_inner_grid line 421
  44. theorem OAI.Erdos3.polynomialShearOrderedBasis_outer_grid line 427
  45. theorem OAI.Erdos3.polynomialShearIndex_card_le line 433
  46. def OAI.Erdos3.polynomialShearRealPointAction line 450
  47. theorem OAI.Erdos3.polynomialShearRealPointAction_rational line 454
  48. theorem OAI.Erdos3.polynomialShearRealLattice_integer_permutation line 471
  49. def OAI.Erdos3.polynomialShearOrbitSum line 495
  50. theorem OAI.Erdos3.polynomialShearOrbitSum_lattice line 499
  51. def OAI.Erdos3.polynomialShearQuotientSum line 508
  52. theorem OAI.Erdos3.polynomialShearQuotientSum_mk line 515
  53. def OAI.Erdos3.PolynomialSlots.shearGroupLift line 534
  54. theorem OAI.Erdos3.PolynomialSlots.shearGroupLift_point line 539
  55. def OAI.Erdos3.PolynomialPatch.shearKernel line 553
  56. def OAI.Erdos3.PolynomialPatch.shearObservable line 556
  57. theorem OAI.Erdos3.PolynomialPatch.value_eq_shearOrbitSum line 561
  58. theorem OAI.Erdos3.PolynomialPatch.value_eq_shearObservable line 569
  59. theorem OAI.Erdos3.polynomialShearRealificationEquiv_repr line 589
  60. theorem OAI.Erdos3.polynomialShearRealificationEquiv_symm_repr line 600
  61. theorem OAI.Erdos3.polynomialShearRealAutEquiv_symm_coord line 606
  62. theorem OAI.Erdos3.PolynomialSlots.shearGroupLift_coordinate line 618
  63. def OAI.Erdos3.PolynomialSlots.shearCoordinatePolynomial line 641
  64. theorem OAI.Erdos3.PolynomialSlots.shearCoordinatePolynomial_degree line 645
  65. theorem OAI.Erdos3.PolynomialSlots.shearCoordinatePolynomial_eval line 650
  66. def OAI.Erdos3.PolynomialSlots.shearLogPolynomial line 673
  67. theorem OAI.Erdos3.PolynomialSlots.shearLogPolynomial_coordinate line 678
  68. theorem OAI.Erdos3.PolynomialSlots.shearLogPolynomial_adapted line 684
  69. theorem OAI.Erdos3.PolynomialSlots.shearLogPolynomial_eval line 704
  70. def OAI.Erdos3.PolynomialSlots.shearPolynomialOrbit line 714
  71. theorem OAI.Erdos3.PolynomialSlots.shearPolynomialOrbit_realEval line 719
  72. theorem OAI.Erdos3.PolynomialSlots.shearPolynomialOrbit_integerEval line 726
  73. def OAI.Erdos3.PolynomialPatch.shearOrbit line 744
  74. theorem OAI.Erdos3.PolynomialPatch.shearOrbit_realEval line 750
  75. theorem OAI.Erdos3.PolynomialPatch.shearOrbit_integerEval line 756
  76. theorem OAI.Erdos3.PolynomialPatch.value_eq_shearOrbit_observable line 762
  77. theorem OAI.Erdos3.PolynomialPatch.value_integer_eq_shearOrbit_observable line 769