OAI/NumberTheory/Catalan/Estimates/PalindromicReversalMultiplicities.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.IsPalindromicAt line 26
  2. theorem OAI.InternalCatalan.IsPalindromicAt.ext line 30
  3. theorem OAI.InternalCatalan.IsPalindromicAt.C_mul line 42
  4. theorem OAI.InternalCatalan.IsPalindromicAt.sum line 51
  5. theorem OAI.InternalCatalan.IsPalindromicAt.natDegree_le line 66
  6. theorem OAI.InternalCatalan.one_add_X_sq_natDegree_le line 83
  7. theorem OAI.InternalCatalan.one_add_X_sq_pow_natDegree_le line 89
  8. theorem OAI.InternalCatalan.reflect_one_add_X_sq line 94
  9. theorem OAI.InternalCatalan.reflect_one_add_X_sq_pow line 99
  10. theorem OAI.InternalCatalan.isPalindromicAt_of_reflect line 110
  11. theorem OAI.InternalCatalan.palindromicU_natDegree_le line 120
  12. theorem OAI.InternalCatalan.palindromicU_reflect line 130
  13. theorem OAI.InternalCatalan.palindromicU_isPalindromic line 141
  14. theorem OAI.InternalCatalan.palindromicQ_eq_sum line 146
  15. theorem OAI.InternalCatalan.palindromicQ_natDegree_le line 154
  16. theorem OAI.InternalCatalan.palindromicQ_reflect line 164
  17. theorem OAI.InternalCatalan.palindromicQ_isPalindromic line 186
  18. def OAI.InternalCatalan.palindromicUCombination line 204
  19. def OAI.InternalCatalan.palindromicUCoordinates line 207
  20. theorem OAI.InternalCatalan.palindromicUCombination_coeff line 210
  21. theorem OAI.InternalCatalan.palindromicUCombination_isPalindromic line 219
  22. theorem OAI.InternalCatalan.palindromicUCoordinates_spec line 225
  23. theorem OAI.InternalCatalan.palindromicU_expansion line 234
  24. def OAI.InternalCatalan.palindromicTransitionMatrix line 243
  25. theorem OAI.InternalCatalan.palindromicUCoordinates_Q line 246
  26. theorem OAI.InternalCatalan.palindromicUCoeffMatrix_mul_transition line 252
  27. theorem OAI.InternalCatalan.palindromicQ_eq_sum_U line 259
  28. theorem OAI.InternalCatalan.det_palindromicTransitionMatrix line 268
  29. theorem OAI.InternalCatalan.det_palindromicTransitionMatrix_ne_zero line 274
  30. def OAI.InternalCatalan.palindromicReverseIndex line 294
  31. theorem OAI.InternalCatalan.palindromicReverseIndex_val line 297
  32. theorem OAI.InternalCatalan.palindromicReverseIndex_pos line 300
  33. theorem OAI.InternalCatalan.palindromicReverseIndex_invol line 306
  34. def OAI.InternalCatalan.palindromicQPrime line 315
  35. theorem OAI.InternalCatalan.palindromicQPrime_zero line 318
  36. theorem OAI.InternalCatalan.palindromicQPrime_pos line 321
  37. def OAI.InternalCatalan.palindromicReversalMatrix line 326
  38. theorem OAI.InternalCatalan.palindromicReversalMatrix_column_zero line 329
  39. theorem OAI.InternalCatalan.palindromicReversalMatrix_column_pos line 333
  40. theorem OAI.InternalCatalan.mul_palindromicReversalMatrix_column_zero line 345
  41. theorem OAI.InternalCatalan.mul_palindromicReversalMatrix_column_pos line 350
  42. def OAI.InternalCatalan.palindromicReversedTransitionMatrix line 355
  43. theorem OAI.InternalCatalan.palindromicReversedTransitionMatrix_column_zero line 358
  44. theorem OAI.InternalCatalan.palindromicReversedTransitionMatrix_column_pos line 362
  45. theorem OAI.InternalCatalan.palindromicQPrime_eq_sum_U line 368
  46. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_basis line 385
  47. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_basis_zero line 391
  48. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_basis_pos line 398
  49. theorem OAI.InternalCatalan.palindromicReversalMatrix_mul_self line 406
  50. theorem OAI.InternalCatalan.palindromicTransitionMatrix_lower line 429
  51. theorem OAI.InternalCatalan.palindromicTransitionMatrix_below_index line 438
  52. theorem OAI.InternalCatalan.palindromicTransitionMatrix_diagonal_mul line 443
  53. theorem OAI.InternalCatalan.palindromicTransitionMatrix_diagonal line 463
  54. theorem OAI.InternalCatalan.palindromicTransitionMatrix_diagonal_ne_zero line 472
  55. theorem OAI.InternalCatalan.det_palindromicTransitionMatrix_exact line 477
  56. theorem OAI.InternalCatalan.palindromicQPrime_formula line 500
  57. theorem OAI.InternalCatalan.palindromicQ_add_X_pow_QPrime line 508
  58. theorem OAI.InternalCatalan.palindromicPairing_eq_sum_U line 524
  59. def OAI.InternalCatalan.palindromicResidueSum line 549
  60. theorem OAI.InternalCatalan.palindromicResidue_sub_not_dvd line 553
  61. theorem OAI.InternalCatalan.palindromicResidueSum_coeff line 565
  62. def OAI.InternalCatalan.palindromicPBase line 580
  63. def OAI.InternalCatalan.palindromicDBase line 583
  64. def OAI.InternalCatalan.palindromicPBaseCombination line 586
  65. def OAI.InternalCatalan.palindromicDBaseCombination line 590
  66. def OAI.InternalCatalan.palindromicPResidueSum line 594
  67. def OAI.InternalCatalan.palindromicDResidueSum line 600
  68. theorem OAI.InternalCatalan.palindromicPResidueSum_eq_X_pow_mul line 606
  69. theorem OAI.InternalCatalan.palindromicDResidueSum_eq line 616
  70. theorem OAI.InternalCatalan.palindromicPResidueSum_coeff line 622
  71. theorem OAI.InternalCatalan.palindromicDResidueSum_coeff line 633
  72. theorem OAI.InternalCatalan.palindromicPResidueSum_coeff_below line 642
  73. def OAI.InternalCatalan.palindromicStandardVector line 657
  74. def OAI.InternalCatalan.palindromicReversalPlusVector line 660
  75. def OAI.InternalCatalan.palindromicReversalMinusVector line 665
  76. theorem OAI.InternalCatalan.palindromicStandardVector_self line 670
  77. theorem OAI.InternalCatalan.palindromicStandardVector_ne_zero line 673
  78. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_zero line 679
  79. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_e0 line 684
  80. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_standard_pos line 690
  81. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_plus line 696
  82. theorem OAI.InternalCatalan.palindromicReversalMatrix_mulVec_minus line 706
  83. theorem OAI.InternalCatalan.palindromicReversalMatrix_eigenvalue_one line 716
  84. theorem OAI.InternalCatalan.palindromicReversalMatrix_eigenvalue_neg_one line 722
  85. theorem OAI.InternalCatalan.palindromicReverseIndex_ne line 728
  86. theorem OAI.InternalCatalan.palindromicReversalPlusVector_self line 737
  87. theorem OAI.InternalCatalan.palindromicReversalMinusVector_self line 743
  88. theorem OAI.InternalCatalan.palindromicReversalPlusVector_ne_zero line 749
  89. theorem OAI.InternalCatalan.palindromicReversalMinusVector_ne_zero line 757
  90. theorem OAI.InternalCatalan.palindromicReversalMatrix_transpose line 765
  91. theorem OAI.InternalCatalan.palindromicReversalMatrix_transpose_mulVec_plus line 780
  92. theorem OAI.InternalCatalan.palindromicReversalMatrix_transpose_mulVec_minus line 787
  93. theorem OAI.InternalCatalan.palindromic_prime_card_split line 794
  94. def OAI.InternalCatalan.palindromicPairMate line 808
  95. theorem OAI.InternalCatalan.palindromicPairMate_zero line 812
  96. theorem OAI.InternalCatalan.palindromicPairMate_of_pos line 816
  97. theorem OAI.InternalCatalan.palindromicPairMate_val line 820
  98. theorem OAI.InternalCatalan.palindromicPairMate_pos line 824
  99. theorem OAI.InternalCatalan.palindromicPairMate_invol line 830
  100. theorem OAI.InternalCatalan.palindromicPairMate_upper line 841
  101. theorem OAI.InternalCatalan.palindromicPairMate_lower line 849
  102. def OAI.InternalCatalan.palindromicEigenLambda line 858
  103. theorem OAI.InternalCatalan.palindromicEigenLambda_zero line 861
  104. theorem OAI.InternalCatalan.palindromicEigenLambda_lower line 865
  105. theorem OAI.InternalCatalan.palindromicEigenLambda_upper line 869
  106. def OAI.InternalCatalan.palindromicEigenCoordinatesLinear line 874
  107. def OAI.InternalCatalan.palindromicEigenSynthesisLinear line 890
  108. theorem OAI.InternalCatalan.palindromicEigenCoordinatesLinear_apply line 906
  109. theorem OAI.InternalCatalan.palindromicEigenSynthesisLinear_apply line 914
  110. theorem OAI.InternalCatalan.palindromicEigenSynthesis_coordinates line 922
  111. theorem OAI.InternalCatalan.palindromicEigenCoordinates_synthesis line 947
  112. def OAI.InternalCatalan.palindromicEigenCoordinates line 972
  113. def OAI.InternalCatalan.palindromicReversalEigenbasis line 980
  114. theorem OAI.InternalCatalan.palindromicReversalEigenbasis_equivFun line 984
  115. theorem OAI.InternalCatalan.palindromicReversalEigenbasis_apply line 989
  116. def OAI.InternalCatalan.palindromicEigenChange line 998
  117. def OAI.InternalCatalan.palindromicEigenChangeInv line 1002
  118. theorem OAI.InternalCatalan.palindromicEigenChange_mulVec line 1006
  119. theorem OAI.InternalCatalan.palindromicEigenChangeInv_mulVec line 1011
  120. theorem OAI.InternalCatalan.palindromicEigenChange_mul_inv line 1016
  121. theorem OAI.InternalCatalan.palindromicEigenChangeInv_mul line 1025
  122. theorem OAI.InternalCatalan.palindromicReversal_transpose_mulVec_apply line 1034
  123. theorem OAI.InternalCatalan.palindromicEigenCoordinates_reversal_synthesis line 1046
  124. theorem OAI.InternalCatalan.palindromicReversalEigenbasis_eigenvector line 1075
  125. theorem OAI.InternalCatalan.palindromicEigenChange_diagonalizes line 1093
  126. theorem OAI.InternalCatalan.palindromicEigenvalue_product line 1117
  127. theorem OAI.InternalCatalan.coordinate_zero_off_eigenvalue line 1176
  128. def OAI.InternalCatalan.eigenKernelCoordinateEquiv line 1193
  129. theorem OAI.InternalCatalan.finrank_eigenKernel_of_coordinates line 1249
  130. def OAI.InternalCatalan.palindromicReversalEigenKernel line 1263
  131. theorem OAI.InternalCatalan.palindromicEigenCoordinates_reversal line 1267
  132. theorem OAI.InternalCatalan.finrank_palindromicReversalEigenKernel line 1277
  133. theorem OAI.InternalCatalan.palindromic_neg_one_ne_one line 1286
  134. theorem OAI.InternalCatalan.palindromicEigenLambda_eq_zero_iff line 1295
  135. theorem OAI.InternalCatalan.palindromicEigenLambda_eq_one_iff line 1302
  136. theorem OAI.InternalCatalan.palindromicEigenLambda_eq_neg_one_iff line 1311
  137. def OAI.InternalCatalan.palindromicZeroEigenIndexEquiv line 1321
  138. def OAI.InternalCatalan.palindromicPlusEigenIndexEquiv line 1338
  139. def OAI.InternalCatalan.palindromicMinusEigenIndexEquiv line 1362
  140. theorem OAI.InternalCatalan.finrank_palindromicReversalEigenKernel_zero line 1389
  141. theorem OAI.InternalCatalan.finrank_palindromicReversalEigenKernel_one line 1396
  142. theorem OAI.InternalCatalan.finrank_palindromicReversalEigenKernel_neg_one line 1403
  143. theorem OAI.InternalCatalan.palindromicReversal_charpoly_eq_product line 1410
  144. theorem OAI.InternalCatalan.palindromicReversal_charpoly line 1427