OAI/NumberTheory/Catalan/Estimates/PalindromicBlockInverse.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedB0 line 18
  2. def OAI.InternalCatalan.fixedB1 line 21
  3. def OAI.InternalCatalan.fixedMatrix line 24
  4. theorem OAI.InternalCatalan.fixedMatrix_apply line 27
  5. theorem OAI.InternalCatalan.fixedMatrix_zero line 31
  6. theorem OAI.InternalCatalan.fixedMatrix_one line 32
  7. theorem OAI.InternalCatalan.fixedMatrix_neg_one line 34
  8. theorem OAI.InternalCatalan.fixed_rowD_four line 37
  9. theorem OAI.InternalCatalan.fixed_rowP_four line 41
  10. theorem OAI.InternalCatalan.fixed_rawEntry_four line 49
  11. def OAI.InternalCatalan.fixedFilteredMomentRat line 68
  12. def OAI.InternalCatalan.fixedFilteredZetaRat line 71
  13. theorem OAI.InternalCatalan.fixedBaseEntry_dot_filtered line 74
  14. theorem OAI.InternalCatalan.palindromicReversalMatrix_cube_mul line 117
  15. theorem OAI.InternalCatalan.palindromicReversalMatrix_cube line 132
  16. def OAI.InternalCatalan.palindromicReversalProjZero line 136
  17. def OAI.InternalCatalan.palindromicReversalProjPlus line 140
  18. def OAI.InternalCatalan.palindromicReversalProjMinus line 146
  19. theorem OAI.InternalCatalan.palindromicReversalProjections_sum line 152
  20. theorem OAI.InternalCatalan.palindromicReversalMatrix_mul_projZero line 162
  21. theorem OAI.InternalCatalan.palindromicReversalMatrix_mul_projPlus line 167
  22. theorem OAI.InternalCatalan.palindromicReversalMatrix_mul_projMinus line 175
  23. theorem OAI.InternalCatalan.palindromicReversalProjZero_mul_matrix line 181
  24. theorem OAI.InternalCatalan.palindromicReversalProjPlus_mul_matrix line 186
  25. theorem OAI.InternalCatalan.palindromicReversalProjMinus_mul_matrix line 194
  26. def OAI.InternalCatalan.palindromicRatResidue line 208
  27. def OAI.InternalCatalan.fixedB0Residue line 211
  28. def OAI.InternalCatalan.fixedB1Residue line 214
  29. theorem OAI.InternalCatalan.fixedB0Residue_apply line 217
  30. theorem OAI.InternalCatalan.fixedB1Residue_apply line 221
  31. theorem OAI.InternalCatalan.palindromicRatResidue_intCast line 225
  32. theorem OAI.InternalCatalan.palindromicRatResidue_mul line 229
  33. theorem OAI.InternalCatalan.palindromicRatResidue_add line 235
  34. theorem OAI.InternalCatalan.palindromicRatResidue_sub line 241
  35. theorem OAI.InternalCatalan.palindromicRatResidue_sum line 247
  36. theorem OAI.InternalCatalan.fixed_nat_inverse_pow_den line 253
  37. theorem OAI.InternalCatalan.harmonicRat_small_den_ne_zero line 263
  38. theorem OAI.InternalCatalan.zetaRat_small_den_ne_zero line 272
  39. theorem OAI.InternalCatalan.fixed_three_halves_den line 293
  40. theorem OAI.InternalCatalan.fixed_rawEntryRat_den_ne_zero line 301
  41. theorem OAI.InternalCatalan.filterCoeffRat_den_ne_zero line 322
  42. theorem OAI.InternalCatalan.palindromicRatResidue_int_sum line 329
  43. theorem OAI.InternalCatalan.fixed_rawEntryRat_residue line 343
  44. theorem OAI.InternalCatalan.filterCoeffRat_residue line 369
  45. theorem OAI.InternalCatalan.fixedBaseEntryRat_den_ne_zero line 375
  46. theorem OAI.InternalCatalan.fixedB0_den_ne_zero line 388
  47. theorem OAI.InternalCatalan.fixedB1_den_ne_zero line 392
  48. theorem OAI.InternalCatalan.fixedBaseEntryRat_residue line 396
  49. theorem OAI.InternalCatalan.fixedMatrix_one_residue line 418
  50. theorem OAI.InternalCatalan.fixedMatrix_neg_one_residue line 426
  51. def OAI.InternalCatalan.palindromicScaledResidueMatrix line 447
  52. def OAI.InternalCatalan.palindromicResidueBlockMatrix line 453
  53. theorem OAI.InternalCatalan.palindromicResidueBlockMatrix_kronecker line 458
  54. def OAI.InternalCatalan.palindromicResidueColumnChange line 465
  55. def OAI.InternalCatalan.palindromicReducedBlockMatrix line 470
  56. theorem OAI.InternalCatalan.palindromicReversedTransitionMatrix_transpose line 475
  57. theorem OAI.InternalCatalan.palindromicResidueBlockMatrix_factor line 480
  58. theorem OAI.InternalCatalan.palindromicResidueBlockMatrix_mul_columnChange line 489
  59. theorem OAI.InternalCatalan.det_palindromicResidueColumnChange line 500
  60. theorem OAI.InternalCatalan.det_palindromicResidueColumnChange_ne_zero line 508
  61. theorem OAI.InternalCatalan.det_palindromicResidueBlockMatrix line 513
  62. theorem OAI.InternalCatalan.det_palindromicResidueBlockMatrix_ne_zero_iff line 522
  63. def OAI.InternalCatalan.palindromicReducedBlockRightInverse line 543
  64. theorem OAI.InternalCatalan.palindromicReducedBlock_mul_projZero line 549
  65. theorem OAI.InternalCatalan.palindromicReducedBlock_mul_projPlus line 562
  66. theorem OAI.InternalCatalan.palindromicReducedBlock_mul_projMinus line 577
  67. theorem OAI.InternalCatalan.palindromicReducedBlock_mul_rightInverse line 600
  68. theorem OAI.InternalCatalan.det_palindromicReducedBlockMatrix_ne_zero_of_fixed line 614
  69. theorem OAI.InternalCatalan.det_palindromicResidueBlockMatrix_ne_zero_of_fixed line 624