OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOneBracketHeight.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase1X line 20
  2. def OAI.InternalCatalan.barrierCase1Y line 24
  3. theorem OAI.InternalCatalan.barrier_realEnergyField_one_hasDerivAt line 27
  4. theorem OAI.InternalCatalan.barrier_realEnergyColumnField_hasDerivAt line 50
  5. theorem OAI.InternalCatalan.barrier_realEnergyCaseField_hasDerivAt line 66
  6. theorem OAI.InternalCatalan.barrierCase1X_hasDerivAt line 79
  7. theorem OAI.InternalCatalan.barrierCase1Y_hasDerivAt line 95
  8. theorem OAI.InternalCatalan.Case1Height.abs_U_eval_le line 112
  9. theorem OAI.InternalCatalan.Case1Height.finiteU_abs_le_mass line 126
  10. theorem OAI.InternalCatalan.Case1Height.finitePower_abs_le_mass line 143
  11. theorem OAI.InternalCatalan.Case1Height.actual_finite_bounds line 159
  12. theorem OAI.InternalCatalan.Case1Height.abs_div_le_const line 168
  13. theorem OAI.InternalCatalan.Case1Height.abs_sub_le_pair line 173
  14. theorem OAI.InternalCatalan.Case1Height.abs_five_sub_le line 176
  15. theorem OAI.InternalCatalan.Case1Height.actual_X_deriv_abs_le line 185
  16. theorem OAI.InternalCatalan.Case1Height.actual_Y_deriv_abs_le line 224
  17. theorem OAI.InternalCatalan.barrier_atBot_add_finite line 260
  18. theorem OAI.InternalCatalan.barrier_log_one_sub_tendsto line 267
  19. def OAI.InternalCatalan.barrierCase1XRegular line 279
  20. theorem OAI.InternalCatalan.barrierCase1XRegular_continuousAt line 284
  21. theorem OAI.InternalCatalan.barrierCase1V1T_continuousAt line 302
  22. theorem OAI.InternalCatalan.barrierCase1X_split line 307
  23. theorem OAI.InternalCatalan.barrierCase1X_zero_remainder line 313
  24. theorem OAI.InternalCatalan.barrierCase1X_one_remainder line 320
  25. theorem OAI.InternalCatalan.barrierCase1X_tendsto_zero_left line 327
  26. theorem OAI.InternalCatalan.barrierCase1X_tendsto_zero_right line 341
  27. theorem OAI.InternalCatalan.barrierCase1X_tendsto_one_left line 355
  28. theorem OAI.InternalCatalan.barrierCase1Y_tendsto_zero_right line 366
  29. theorem OAI.InternalCatalan.barrierCase1Y_tendsto_one_left line 382
  30. theorem OAI.InternalCatalan.barrierCase1X_continuousAt_neg_one line 396
  31. def OAI.InternalCatalan.barrierCase1XRat line 402
  32. def OAI.InternalCatalan.barrierCase1YRat line 406
  33. theorem OAI.InternalCatalan.barrierCase1X_eval_rat line 409
  34. theorem OAI.InternalCatalan.barrierCase1Y_eval_rat line 421
  35. theorem OAI.InternalCatalan.barrierCase1X_deriv_eq_zero_iff line 432
  36. theorem OAI.InternalCatalan.barrierCase1Y_deriv_eq_zero_iff line 438
  37. theorem OAI.InternalCatalan.barrierCase1X_stationary_in_each_bracket line 444
  38. theorem OAI.InternalCatalan.barrierCase1Y_stationary_in_each_bracket line 460
  39. theorem OAI.InternalCatalan.Case1Height.X_closed_bracket_margins line 476
  40. theorem OAI.InternalCatalan.Case1Height.Y_closed_bracket_margins line 491
  41. theorem OAI.InternalCatalan.Case1Height.regular_of_margins line 506
  42. theorem OAI.InternalCatalan.Case1Height.abs_sub_le_on_Icc line 515
  43. theorem OAI.InternalCatalan.Case1Height.actual_bracket_width line 526
  44. theorem OAI.InternalCatalan.Case1Height.height_of_abs_variation line 532
  45. theorem OAI.InternalCatalan.barrierCase1X_bracket_height line 552
  46. theorem OAI.InternalCatalan.barrierCase1Y_bracket_height line 568