OAI/NumberTheory/Catalan/Estimates/ExceptionalScalarBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.two_adic_sum_lower line 14
  2. theorem OAI.InternalCatalan.harmonicRat_two_adic_lower line 30
  3. theorem OAI.InternalCatalan.zetaRat_two_adic_lower_of_le line 47
  4. theorem OAI.InternalCatalan.zetaRat_two_adic_lower line 81
  5. theorem OAI.InternalCatalan.zetaRat_two_adic_floor_lower line 88
  6. def OAI.InternalCatalan.exceptionScalar line 107
  7. def OAI.InternalCatalan.boundaryScalar line 113
  8. theorem OAI.InternalCatalan.exceptionalScalar_index_lt_H line 119
  9. theorem OAI.InternalCatalan.contract_rowFactor_reversed line 125
  10. theorem OAI.InternalCatalan.exceptionColumn_eq_sum_exceptionScalar line 171
  11. theorem OAI.InternalCatalan.boundaryColumn_eq_sum_boundaryScalar line 183
  12. theorem OAI.InternalCatalan.padic_two_norm_rat_le_zpow_of_valuation line 206
  13. theorem OAI.InternalCatalan.centralCoeff_norm_le line 215
  14. theorem OAI.InternalCatalan.centralCoeffKernel_norm_le line 220
  15. theorem OAI.InternalCatalan.zetaRat_norm_le line 229
  16. theorem OAI.InternalCatalan.exceptionScalar_norm_le line 239
  17. theorem OAI.InternalCatalan.boundaryScalar_norm_le line 262