OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoBracketHeight.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.Case2Height.linear_den_norm_lower line 17
  2. theorem OAI.InternalCatalan.Case2Height.quadratic_den_norm_lower line 26
  3. theorem OAI.InternalCatalan.Case2Height.quotient_norm_le line 52
  4. theorem OAI.InternalCatalan.Case2Height.numerator_norm_le line 59
  5. theorem OAI.InternalCatalan.Case2Height.norm_map_sum_le line 64
  6. theorem OAI.InternalCatalan.Case2Height.actual_finite_bounds line 76
  7. theorem OAI.InternalCatalan.Case2Height.actual_tail_bounds line 85
  8. theorem OAI.InternalCatalan.Case2Height.abs_div_le_const line 132
  9. theorem OAI.InternalCatalan.Case2Height.abs_sub_le_pair line 137
  10. theorem OAI.InternalCatalan.Case2Height.abs_four_sub_le line 140
  11. theorem OAI.InternalCatalan.Case2Height.X_formula_abs_le line 148
  12. theorem OAI.InternalCatalan.Case2Height.Y_formula_abs_le line 191
  13. theorem OAI.InternalCatalan.Case2Height.X_closed_bracket_margins line 231
  14. theorem OAI.InternalCatalan.Case2Height.Y_closed_bracket_margins line 254
  15. theorem OAI.InternalCatalan.Case2Height.height_of_abs_variation line 272
  16. theorem OAI.InternalCatalan.barrierCase2X_bracket_height line 292
  17. theorem OAI.InternalCatalan.barrierCase2Y_bracket_height line 311