OAI/NumberTheory/Catalan/Estimates/ManuscriptSharpDerivativeBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.ManuscriptSharpHeight.quotient_norm_le line 12
  2. theorem OAI.InternalCatalan.ManuscriptSharpHeight.numerator_norm_le line 19
  3. theorem OAI.InternalCatalan.ManuscriptSharpHeight.norm_map_sum_le line 24
  4. theorem OAI.InternalCatalan.ManuscriptSharpHeight.actual_tail_bounds line 36
  5. theorem OAI.InternalCatalan.ManuscriptSharpHeight.abs_div_le_const line 83
  6. theorem OAI.InternalCatalan.ManuscriptSharpHeight.abs_sub_le_pair line 88
  7. theorem OAI.InternalCatalan.ManuscriptSharpHeight.abs_four_sub_le line 91
  8. theorem OAI.InternalCatalan.ManuscriptSharpHeight.X_formula_abs_lt line 99
  9. theorem OAI.InternalCatalan.ManuscriptSharpHeight.Y_formula_abs_lt line 142
  10. theorem OAI.InternalCatalan.ManuscriptSharpHeight.actual_X_deriv_abs_lt line 176
  11. theorem OAI.InternalCatalan.ManuscriptSharpHeight.actual_Y_deriv_abs_lt line 184
  12. theorem OAI.InternalCatalan.ManuscriptSharpHeight.abs_five_sub_le line 191
  13. theorem OAI.InternalCatalan.ManuscriptSharpHeight.case1_X_deriv_abs_lt line 197
  14. theorem OAI.InternalCatalan.ManuscriptSharpHeight.case1_Y_deriv_abs_lt line 236