OAI/NumberTheory/Catalan/Determinants/RealDeterminantUpper.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realDeterminantSheetPrefactor line 22
  2. def OAI.InternalCatalan.realDeterminantPrefactor line 26
  3. theorem OAI.InternalCatalan.realDeterminantSheetPrefactor_nonneg line 29
  4. theorem OAI.InternalCatalan.realDeterminantPrefactor_nonneg line 34
  5. theorem OAI.InternalCatalan.realDeterminant_factorial_sq_one_le line 39
  6. theorem OAI.InternalCatalan.realDeterminantPrefactor_le_mass_mul_sheet line 45
  7. theorem OAI.InternalCatalan.realDeterminantPrefactor_le_power line 52
  8. theorem OAI.InternalCatalan.realDeterminantPrefactor_eventually_le_exp line 93
  9. theorem OAI.InternalCatalan.realDeterminant_uniform_exp_dual line 140
  10. theorem OAI.InternalCatalan.realDeterminant_eventually_log_dual line 199
  11. theorem OAI.InternalCatalan.realDeterminant_eventually_log_sup_dual line 238
  12. def OAI.InternalCatalan.realDeterminantCertificateSupBound line 255
  13. theorem OAI.InternalCatalan.realDeterminant_eventually_log_certificate_sup line 262
  14. theorem OAI.InternalCatalan.barrier_case1_row_sup_upper line 282
  15. theorem OAI.InternalCatalan.barrier_case1_column_sup_upper line 291
  16. theorem OAI.InternalCatalan.barrier_case2_row_sup_upper line 298
  17. theorem OAI.InternalCatalan.barrier_case2_column_sup_upper line 308
  18. theorem OAI.InternalCatalan.realDeterminantCaseOneDual_sharp_lt line 315
  19. theorem OAI.InternalCatalan.realDeterminantCaseTwoDual_sharp_lt line 323
  20. theorem OAI.InternalCatalan.realDeterminantCertificateSupBound_sharp_lt line 331
  21. theorem OAI.InternalCatalan.realDeterminantCertificateSupBound_lt line 338
  22. theorem OAI.InternalCatalan.eventually_realDeterminant_log_upper_sharp line 342
  23. theorem OAI.InternalCatalan.eventually_realDeterminant_abs_upper_sharp line 350
  24. theorem OAI.InternalCatalan.eventually_realDeterminant_log_upper line 373