OAI/NumberTheory/Catalan/Energy/BarrierTailPairRational.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierComplex line 22
  2. def OAI.InternalCatalan.barrierConjugatePair line 24
  3. def OAI.InternalCatalan.barrierP2Finite line 27
  4. def OAI.InternalCatalan.barrierV2Finite line 30
  5. def OAI.InternalCatalan.barrierP1Finite line 33
  6. def OAI.InternalCatalan.barrierV1Finite line 36
  7. def OAI.InternalCatalan.barrierP2Tail line 39
  8. def OAI.InternalCatalan.barrierV2Tail line 47
  9. def OAI.InternalCatalan.barrierLambda2 line 58
  10. def OAI.InternalCatalan.barrierLambda1 line 59
  11. def OAI.InternalCatalan.barrierFiniteCoeff line 61
  12. def OAI.InternalCatalan.barrierTrial line 64
  13. def OAI.InternalCatalan.barrierP2 line 68
  14. def OAI.InternalCatalan.barrierV2 line 69
  15. def OAI.InternalCatalan.barrierP1 line 70
  16. def OAI.InternalCatalan.barrierV1 line 71
  17. theorem OAI.InternalCatalan.barrier_finite_lengths line 73
  18. theorem OAI.InternalCatalan.barrier_tail_lengths line 77
  19. theorem OAI.InternalCatalan.barrier_lambdas line 80
  20. theorem OAI.InternalCatalan.barrierP2_finite_abs_lt_one line 84
  21. theorem OAI.InternalCatalan.barrierV2_finite_abs_lt_one line 88
  22. theorem OAI.InternalCatalan.barrierP1_finite_abs_lt_one line 92
  23. theorem OAI.InternalCatalan.barrierV1_finite_abs_lt_one line 96
  24. theorem OAI.InternalCatalan.barrierP2_tail_norm_bounds line 100
  25. theorem OAI.InternalCatalan.barrierV2_tail_norm_bounds line 113
  26. theorem OAI.InternalCatalan.barrierFiniteCoeff_abs_le line 126
  27. def OAI.InternalCatalan.barrierTailLinearDen line 150
  28. def OAI.InternalCatalan.barrierTailQuadraticDen line 152
  29. theorem OAI.InternalCatalan.barrierTailLinearDen_ne_zero line 155
  30. theorem OAI.InternalCatalan.barrierTailQuadraticDen_ne_zero line 167
  31. theorem OAI.InternalCatalan.barrierTailLinearDen_prod_ne_zero line 190
  32. theorem OAI.InternalCatalan.barrierTailQuadraticDen_prod_ne_zero line 198
  33. def OAI.InternalCatalan.barrierCase2QXValue line 206
  34. def OAI.InternalCatalan.barrierCase2QYValue line 211
  35. theorem OAI.InternalCatalan.barrierP2_tail_base_lt_one line 215
  36. theorem OAI.InternalCatalan.barrierV2_tail_base_lt_one line 220
  37. theorem OAI.InternalCatalan.barrierCase2QXValue_ne_zero line 225
  38. theorem OAI.InternalCatalan.barrierCase2QYValue_ne_zero line 239
  39. theorem OAI.InternalCatalan.barrierComplex_real_pow line 248
  40. theorem OAI.InternalCatalan.barrierComplex_imaginary_pow line 254
  41. theorem OAI.InternalCatalan.barrierConjugatePair_power_re line 260
  42. def OAI.InternalCatalan.barrierAxisPhase line 270
  43. theorem OAI.InternalCatalan.barrierConjugatePair_imaginary_power_re line 273
  44. def OAI.InternalCatalan.barrierV2CoefficientFormula line 283
  45. theorem OAI.InternalCatalan.barrierV2_eq_coefficientFormula line 295
  46. def OAI.InternalCatalan.barrierP2NormRows line 306
  47. def OAI.InternalCatalan.barrierV2NormRows line 313
  48. def OAI.InternalCatalan.barrierNormMajorant line 322
  49. theorem OAI.InternalCatalan.norm_le_of_normSq_le line 325
  50. theorem OAI.InternalCatalan.normRows_of_sq line 330
  51. theorem OAI.InternalCatalan.barrierP2_normRows line 338
  52. theorem OAI.InternalCatalan.barrierV2_normRows line 345
  53. theorem OAI.InternalCatalan.barrier_tail_norm_majorant line 352
  54. theorem OAI.InternalCatalan.barrier_normMajorant_shift line 370
  55. theorem OAI.InternalCatalan.barrierTrial_abs_le_majorant line 388
  56. theorem OAI.InternalCatalan.barrierP2_tail_decay line 399
  57. theorem OAI.InternalCatalan.barrierV2_tail_decay line 414
  58. theorem OAI.InternalCatalan.barrier_conjugate_quotient_re line 431
  59. theorem OAI.InternalCatalan.barrierTailLinearDen_star line 441
  60. theorem OAI.InternalCatalan.barrierTailQuadraticDen_star line 445
  61. theorem OAI.InternalCatalan.barrierConjugatePair_linear_re line 449
  62. theorem OAI.InternalCatalan.barrierConjugatePair_quadratic_re line 463
  63. def OAI.InternalCatalan.barrierPairLinearQ line 483
  64. def OAI.InternalCatalan.barrierPairLinearA line 486
  65. def OAI.InternalCatalan.barrierPairQuadraticQ line 489
  66. def OAI.InternalCatalan.barrierPairQuadraticA line 493
  67. theorem OAI.InternalCatalan.barrierConjugatePair_linear_eq_ratPolynomial line 497
  68. theorem OAI.InternalCatalan.barrierConjugatePair_quadratic_eq_ratPolynomial line 509
  69. theorem OAI.InternalCatalan.barrierPairLinearQ_eval_eq_normSq line 521
  70. theorem OAI.InternalCatalan.barrierPairQuadraticQ_eval_eq_normSq line 528
  71. theorem OAI.InternalCatalan.barrierPairLinearQ_eval_pos line 535
  72. theorem OAI.InternalCatalan.barrierPairQuadraticQ_eval_pos line 541