OAI/Combinatorics/HoneycombChords/Meixner.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

Meixner and Pollaczek generating coefficients

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff line 17
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_zero line 19
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_one line 20
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_congr line 21
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_add line 23
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_sub line 26
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_const_mul line 30
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_deriv line 35
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_monomial_mul line 41
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_monomial_mul_low line 57
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_id_mul line 67
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_sq_deriv line 70
  13. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff_ode_recurrence line 81

    Source documentation

    Coefficient recurrence for the exact generating differential equation. This is local at zero; no global power series assumption is made.

    theorem taylorCoeff_ode_recurrence {f : ๐•œ โ†’ ๐•œ} (hf : ContDiffAt ๐•œ โŠค f 0) (a e : ๐•œ)
    (hode : (fun t => (1-e*t^2)*deriv f t) =แถ [๐“ 0] (fun t => (a+e*t)*f t)) (n : โ„•) :
    (n+2)*taylorCoeff f (n+2)=a*taylorCoeff f (n+1)+e*(n+1)*taylorCoeff f n := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff

  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff line 105
  15. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseFactor line 109
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.factorError line 110
  17. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct line 111
  18. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.upperProduct line 112
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseFactor_pos line 113
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.factorError_nonneg line 115
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct_pos line 117
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.upperProduct_pos line 119
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct_succ line 121
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.upperProduct_succ line 123
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_pair_step line 125
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pair_rowsums line 138
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_pair_lower line 146
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_pair_upper line 173
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseFactor_ge_half line 213
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.factorError_le line 217
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocal_square_sum_bound line 226
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocal_square_sum_le_two line 242
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.upperProduct_le_exp line 247
  34. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_even_product_bounds line 269

    Source documentation

    Uniform bounds on the exact recurrence; the finite products have exponent s-1/2, obtained by Euler's Gamma limit in ProductGammaAsymptotic.

    theorem meixner_even_product_bounds {s : โ„} (hs : 0 < s) (n : โ„•) :
    min 1 (2*s)*baseProduct s n โ‰ค meixnerCoeff s (2*n) โˆง
    meixnerCoeff s (2*n) โ‰ค (max 1 (2*s)*Real.exp (2*(2*s-1)^2))*baseProduct s n := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff

  35. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio line 287
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_formula line 289
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_gamma_identity line 295
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_normalized_tendsto line 306
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_eventual_bounds line 322

    Source documentation

    Constant-factor, not epsilon-loss, asymptotics for the rising-factorial product needed by the polynomial determinant compression.

    lemma pochRatio_eventual_bounds {a : โ„} (ha : 0 < a) :
    โˆƒ c C : โ„,0 < c โˆง 0 < C โˆง โˆ€แถ  n : โ„• in atTop,
      c*((n:โ„)+1)^(a-1) โ‰ค pochRatio a (n+1) โˆง
      pochRatio a (n+1) โ‰ค C*((n:โ„)+1)^(a-1) := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio

  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_sequence_global_bounds line 343
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct_eq_poch line 352
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_pos line 359
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_succ line 361
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct_square_normalized_tendsto line 363
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.baseProduct_square_poch_bounds line 382
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_even_square_poch_bounds line 393
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sum_pochRatio line 414
  48. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenCoefficientKernel line 423
  49. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenCoefficientKernel_bounds line 428

    Source documentation

    The exact squared-coefficient sum needed for the negative-axis Christoffel kernel. The link with the orthogonal polynomial generating function is a separate obligation, not an assumed kernel identification.

    theorem evenCoefficientKernel_bounds {s : โ„} (hs : 0 < s) :
    โˆƒ c C : โ„,0 < c โˆง 0 < C โˆง โˆ€แถ  n : โ„• in atTop,
      c*((n:โ„)+1)^(2*s) โ‰ค evenCoefficientKernel s n โˆง
      evenCoefficientKernel s n โ‰ค C*((n:โ„)+1)^(2*s) := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenCoefficientKernel

  50. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator line 464
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_smooth line 466
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_zero line 470
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_ode line 471
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_one_coeff line 489
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_taylor line 493

    Source documentation

    The recurrence coefficients equal the Taylor coefficients of the generating function.

    lemma meixnerGenerator_taylor (s : โ„) (n : โ„•) :
    taylorCoeff (meixnerGenerator s) n=meixnerCoeff s n := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylorCoeff, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff

  56. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerEvenGenerator line 505
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator_exp line 507
  58. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerEvenGenerator_eq line 520
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerEvenGenerator_taylor line 535
  60. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenOddPolynomials line 560
  61. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly line 567
  62. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oddPoly line 568
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly_zero line 569
  64. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oddPoly_zero line 570
  65. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly_succ line 571
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oddPoly_succ line 573
  67. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.eval_evenPoly_succ line 575
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.eval_oddPoly_succ line 578
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_even_step line 581
  70. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_odd_step line 584
  71. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenOdd_plus_eval line 589

    Source documentation

    The even Pollaczek polynomials form a basis.

    lemma evenOdd_plus_eval (s : โ„) (n : โ„•) :
    (evenPoly 1 n).eval (s^2)=meixnerCoeff s (2*n) โˆง
    s*(oddPoly 1 n).eval (s^2)=meixnerCoeff s (2*n+1) := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oddPoly

  72. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenOdd_sign_eval line 599
  73. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly_negative_eval line 610

    Source documentation

    Evaluation on the negative axis gives alternating Meixner coefficients.

    lemma evenPoly_negative_eval (s : โ„) (n : โ„•) :
    (evenPoly (-1) n).eval (-(s^2))=(-1)^n*meixnerCoeff s (2*n) := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff

  74. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly_negative_eval_sq line 613
  75. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator line 625
  76. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_smooth line 627
  77. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_analytic line 633
  78. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_zero line 635
  79. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_ode line 636
  80. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff line 649
  81. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_taylor line 653
  82. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_even_step line 669
  83. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_odd_step line 672
  84. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_evenOdd line 676
  85. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_nonneg line 686
  86. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_abs_le line 691
  87. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scalarSeries_taylor line 713
  88. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.binomialProductCoeff line 722
  89. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.binomialProduct_hasSum line 724
  90. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.binomialProduct_series line 746
  91. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_eq_binomialProduct line 753
  92. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_hasSum line 758

    Source documentation

    The generating series converges absolutely for arguments of absolute value less than one.

    lemma meixnerCoeff_hasSum (s : โ„) {u : โ„} (hu : |u| < 1) :
    HasSum (fun n => meixnerCoeff s n*u^n) (meixnerGenerator s u) := by
โ€ฆ

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerGenerator

  93. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_summable_norm line 770
  94. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_radius line 775
  95. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_hasSum line 782
  96. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant line 803
  97. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.quarter_artanh_bounds line 804
  98. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant_pos line 811
  99. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant_continuous line 814
  100. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant_exp line 817
  101. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exp_div_cosh_integrable line 821
  102. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant_sq_integrable line 837
  103. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_majorant line 847
  104. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_majorant line 857
  105. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_continuous line 870
  106. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_continuous_p line 875