OAI/NumberTheory/Catalan/Determinants/RealColumnDeterminant.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.reversedRow line 21
  2. def OAI.InternalCatalan.rowP line 24
  3. def OAI.InternalCatalan.rowD line 28
  4. theorem OAI.InternalCatalan.reversedRow_zero line 33
  5. theorem OAI.InternalCatalan.reversedRow_coeff line 36
  6. theorem OAI.InternalCatalan.reversedRow_coeff_eq_zero_of_ge line 55
  7. theorem OAI.InternalCatalan.reversedRow_natDegree_le line 59
  8. theorem OAI.InternalCatalan.reversedRow_coeff_eq_zero_of_lt line 66
  9. theorem OAI.InternalCatalan.coeff_mul_eq_zero_below_right line 73
  10. theorem OAI.InternalCatalan.natDegree_one_sub_X line 82
  11. theorem OAI.InternalCatalan.rowFactor_natDegree_le line 86
  12. theorem OAI.InternalCatalan.rowP_natDegree_le line 92
  13. theorem OAI.InternalCatalan.rowD_natDegree_le line 103
  14. theorem OAI.InternalCatalan.rowP_coeff_eq_zero_of_lt line 119
  15. theorem OAI.InternalCatalan.rowD_eq_zero_of_distance_zero line 129
  16. theorem OAI.InternalCatalan.rowD_coeff_eq_zero_of_lt line 133
  17. theorem OAI.InternalCatalan.rowP_coeff_eq_zero_of_ge line 146
  18. theorem OAI.InternalCatalan.rowD_coeff_eq_zero_of_ge line 153
  19. theorem OAI.InternalCatalan.rowP_support line 160
  20. theorem OAI.InternalCatalan.rowD_support line 171
  21. def OAI.InternalCatalan.realPoly line 182
  22. def OAI.InternalCatalan.filteredColumn line 184
  23. def OAI.InternalCatalan.mixedMoment line 186
  24. def OAI.InternalCatalan.zetaMoment line 190
  25. def OAI.InternalCatalan.determinantEntry line 194
  26. def OAI.InternalCatalan.determinant line 198
  27. def OAI.InternalCatalan.normalizedLog line 201
  28. def OAI.InternalCatalan.finiteLowerConstant line 204
  29. def OAI.InternalCatalan.realUpperConstant line 207
  30. def OAI.InternalCatalan.contradictionThreshold line 209
  31. theorem OAI.InternalCatalan.fixedTyped_reversedRow_add line 211
  32. theorem OAI.InternalCatalan.fixedTyped_reversedRow_monomial line 217
  33. theorem OAI.InternalCatalan.fixedTyped_rowFactor line 224
  34. theorem OAI.InternalCatalan.fixedTyped_rowP_of_parameters line 228
  35. theorem OAI.InternalCatalan.fixedTyped_rowD_of_parameters line 235
  36. theorem OAI.InternalCatalan.fixed_rowDistance_le44 line 243
  37. theorem OAI.InternalCatalan.fixed_rowP_coeff_eq_zero_below18 line 248
  38. theorem OAI.InternalCatalan.fixed_rowD_coeff_eq_zero_below19 line 261
  39. def OAI.InternalCatalan.rawEntryRat line 282
  40. def OAI.InternalCatalan.filterCoeffRat line 288
  41. def OAI.InternalCatalan.filteredEntryRat line 290
  42. def OAI.InternalCatalan.determinantRat line 294
  43. def OAI.InternalCatalan.fixedBaseEntryRat line 297
  44. theorem OAI.InternalCatalan.rawEntryRat_zero line 300
  45. def OAI.InternalCatalan.rawCatalanCoeffRat line 307
  46. theorem OAI.InternalCatalan.rawEntryRat_affine line 311
  47. theorem OAI.InternalCatalan.rowDistance_of_le_g line 334
  48. theorem OAI.InternalCatalan.rowP_coeff_eq_zero_of_lt_left_contact line 339
  49. theorem OAI.InternalCatalan.rowD_coeff_eq_zero_of_lt_left_contact line 355
  50. theorem OAI.InternalCatalan.row_contact_of_le_g line 375
  51. theorem OAI.InternalCatalan.polynomial_support_subset_range line 387
  52. theorem OAI.InternalCatalan.polynomial_eq_sum_range line 394
  53. theorem OAI.InternalCatalan.reversedRow_eval₂ line 403
  54. theorem OAI.InternalCatalan.rowP_eval₂ line 425
  55. theorem OAI.InternalCatalan.rowD_eval₂ line 437
  56. theorem OAI.InternalCatalan.filteredColumn_det_eq_vandermonde line 456
  57. theorem OAI.InternalCatalan.filteredColumn_det_eq_prod line 473