OAI/NumberTheory/Catalan/Determinants/TwoAdicSmoothedMinor.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.rawColumn_card line 20
  2. def OAI.InternalCatalan.rawMatrixRat line 26
  3. def OAI.InternalCatalan.rawFilterInt line 30
  4. theorem OAI.InternalCatalan.filteredEntryRat_eq_sum_contactRange line 34
  5. theorem OAI.InternalCatalan.filteredMatrixRat_eq_raw_mul_filter line 53
  6. theorem OAI.InternalCatalan.determinantRat_eq_det_raw_mul_filter line 66
  7. def OAI.InternalCatalan.rawMinorRat line 71
  8. theorem OAI.InternalCatalan.rawMinorRat_eq_zero_of_not_injective line 75
  9. theorem OAI.InternalCatalan.determinantRat_eq_sum_raw_choices line 87
  10. theorem OAI.InternalCatalan.determinantRat_eq_sum_raw_minors line 111
  11. def OAI.InternalCatalan.intPolynomialSeries line 136
  12. theorem OAI.InternalCatalan.coeff_intPolynomialSeries line 139
  13. theorem OAI.InternalCatalan.intPolynomialSeries_mul line 143
  14. def OAI.InternalCatalan.contactSeries line 147
  15. theorem OAI.InternalCatalan.coeff_X_centralKernelSeries line 150
  16. theorem OAI.InternalCatalan.contactSeries_coeff_eq_sum line 162
  17. theorem OAI.InternalCatalan.series_coeff_mul_congr_below line 186
  18. theorem OAI.InternalCatalan.contactSeries_mul line 196
  19. theorem OAI.InternalCatalan.reversedChebyshev_contact_series line 200
  20. theorem OAI.InternalCatalan.row_contact_of_gt_g line 209
  21. theorem OAI.InternalCatalan.row_contact line 241
  22. def OAI.InternalCatalan.smoothingColumn line 262
  23. def OAI.InternalCatalan.exceptionColumn line 266
  24. def OAI.InternalCatalan.boundaryColumn line 272
  25. theorem OAI.InternalCatalan.rawEntryRat_two_adic_decomposition line 278
  26. def OAI.InternalCatalan.rawColumnTerm line 371
  27. theorem OAI.InternalCatalan.rawColumnTerm_sum line 376
  28. theorem OAI.InternalCatalan.rawMinorRat_cast_two_adic line 381
  29. theorem OAI.InternalCatalan.rawMinorRat_two_adic_column_expansion line 389
  30. theorem OAI.InternalCatalan.determinantRat_two_adic_column_expansion line 409
  31. theorem OAI.InternalCatalan.padic_two_norm_int_le_of_pow_dvd line 433
  32. theorem OAI.InternalCatalan.smoothingColumn_term_norm_le line 446
  33. theorem OAI.InternalCatalan.smoothingColumn_norm_le line 474
  34. theorem OAI.InternalCatalan.padic_two_det_norm_le_prod_column line 489
  35. theorem OAI.InternalCatalan.smoothing_full_minor_norm_le line 508