OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoMaxReduction.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X line 21
  2. def OAI.InternalCatalan.barrierCase2Y line 25
  3. theorem OAI.InternalCatalan.barrierCase2X_eq line 28
  4. theorem OAI.InternalCatalan.barrier_case2_p_tail_base_lt_one line 33
  5. theorem OAI.InternalCatalan.barrier_case2_v_tail_base_lt_one line 38
  6. theorem OAI.InternalCatalan.barrier_case2_pT_hasDerivAt line 43
  7. theorem OAI.InternalCatalan.barrier_case2_vT_hasDerivAt line 55
  8. theorem OAI.InternalCatalan.barrier_case2_vS_hasDerivAt line 67
  9. theorem OAI.InternalCatalan.barrier_realEnergyField_two_hasDerivAt line 78
  10. theorem OAI.InternalCatalan.barrier_case2_column_hasDerivAt line 99
  11. theorem OAI.InternalCatalan.barrierCase2X_hasDerivAt line 114
  12. theorem OAI.InternalCatalan.barrierCase2Y_hasDerivAt line 128
  13. theorem OAI.InternalCatalan.barrier2_atBot_add_finite line 145
  14. theorem OAI.InternalCatalan.barrier2_log_one_sub_tendsto line 152
  15. theorem OAI.InternalCatalan.barrier2_continuousOn_tendsto_one_left line 164
  16. theorem OAI.InternalCatalan.barrier2_continuousOn_continuousAt_zero line 176
  17. def OAI.InternalCatalan.barrierCase2XRegular line 180
  18. theorem OAI.InternalCatalan.barrierCase2XRegular_continuousOn line 184
  19. theorem OAI.InternalCatalan.barrierCase2V2T_continuousOn line 195
  20. theorem OAI.InternalCatalan.barrierCase2X_split line 199
  21. theorem OAI.InternalCatalan.barrierCase2X_zero_remainder line 206
  22. theorem OAI.InternalCatalan.barrierCase2X_tendsto_zero_left line 214
  23. theorem OAI.InternalCatalan.barrierCase2X_tendsto_zero_right line 228
  24. theorem OAI.InternalCatalan.barrierCase2X_tendsto_one_left line 242
  25. theorem OAI.InternalCatalan.barrierCase2Y_tendsto_zero_right line 256
  26. theorem OAI.InternalCatalan.barrierCase2Y_tendsto_one_left line 272
  27. theorem OAI.InternalCatalan.barrierCase2X_continuousWithinAt line 286
  28. theorem OAI.InternalCatalan.barrierCase2X_continuousOn_negative line 300
  29. theorem OAI.InternalCatalan.barrierCase2X_continuousOn_positive line 308
  30. theorem OAI.InternalCatalan.barrierCase2Y_continuousOn line 316
  31. def OAI.InternalCatalan.barrierCase2XPLogTerm line 336
  32. def OAI.InternalCatalan.barrierCase2XVLogTerm line 339
  33. def OAI.InternalCatalan.barrierCase2YVLogTerm line 342
  34. def OAI.InternalCatalan.barrierCase2XRat line 345
  35. def OAI.InternalCatalan.barrierCase2YRat line 348
  36. theorem OAI.InternalCatalan.barrierFiniteT_sum_cast line 351
  37. theorem OAI.InternalCatalan.barrierFiniteS_sum_cast line 357
  38. theorem OAI.InternalCatalan.barrierList_scaled_re_sum line 363
  39. theorem OAI.InternalCatalan.barrierCase2X_eval_rat line 374
  40. theorem OAI.InternalCatalan.barrierCase2Y_eval_rat line 402
  41. theorem OAI.InternalCatalan.barrierCase2X_deriv_eq_zero_iff line 424
  42. theorem OAI.InternalCatalan.barrierCase2Y_deriv_eq_zero_iff line 433
  43. theorem OAI.InternalCatalan.barrierCase2XPLogTerm_conj line 449
  44. theorem OAI.InternalCatalan.barrierCase2XVLogTerm_conj line 458
  45. theorem OAI.InternalCatalan.barrierCase2YVLogTerm_conj line 465
  46. theorem OAI.InternalCatalan.barrierCase2X_le_of_bracket_bounds line 478
  47. theorem OAI.InternalCatalan.barrierCase2Y_le_of_bracket_bounds line 504