OAI/NumberTheory/Catalan/Estimates/MomentEvaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.momentScalar_step line 14
  2. theorem OAI.InternalCatalan.momentScalar_cast_step line 33
  3. theorem OAI.InternalCatalan.sum_range_sub_add_two line 38
  4. theorem OAI.InternalCatalan.hasSum_sub_add_two_value line 47
  5. theorem OAI.InternalCatalan.mixedMoment_X_pow_zero_step line 58
  6. theorem OAI.InternalCatalan.mixedMoment_X_one_zero line 85
  7. theorem OAI.InternalCatalan.mixedMoment_zero_X_pow_step line 102
  8. theorem OAI.InternalCatalan.mixedMoment_minus_decomposition line 149
  9. theorem OAI.InternalCatalan.mixedMoment_plus_succ_decomposition line 178
  10. theorem OAI.InternalCatalan.mixedMoment_X_pow_decomposition line 212
  11. theorem OAI.InternalCatalan.mixedMoment_X_pow_evaluation line 265