OAI/Combinatorics/HoneycombChords/Pollaczek.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Pollaczek orthogonality and polynomial kernels

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair line 19
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_comm line 21
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generator_prefactor line 26
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generator_symmetric_product line 30
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.arctan_quarter_bound line 40
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_generator line 47
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_series_bound line 81
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_pair_hasSum line 108
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coefficients_unique line 155
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_coeff_generator line 163
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_orthogonal line 177
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff_pos line 200
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPoly_ne_zero line 205
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oddPoly_ne_zero line 211
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_evenOdd_degree line 220
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_span line 244
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_eq_pollaczek_sum line 256
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pow_sech_integrable line 282
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_sech_integrable line 298
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_sech_pair_integrable line 310
  21. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner line 313
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_eq line 315
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_orthogonal line 319
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_sum_left line 334
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_smul_left line 338
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_comm line 344
  27. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCombination line 354
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCombination_eval line 356
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCombination_inner line 359
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCombination_degree line 367
  31. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechChristoffelSum line 372
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechChristoffelSum_pos line 374
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSechInner_nonneg line 379
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_evaluation_bound line 385
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_evaluation_ratio_bound line 391
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_evaluation_ratio_attained line 398
  37. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialChristoffel line 407
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialChristoffel_eq_sum line 409
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialChristoffel_negative line 421
  40. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialChristoffel_bounds line 427

    Source documentation

    Source Christoffel estimate for the genuine normalized sech measure at c=pi, not just the formal generating coefficients.

    theorem polynomialChristoffel_bounds {s : ℝ} (hs : 0 < s) :
    ∃ c C : ℝ,0 < c ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      c*((n:ℝ)+1)^(2*s) ≤ polynomialChristoffel n (-(s^2)) ∧
      polynomialChristoffel n (-(s^2)) ≤ C*((n:ℝ)+1)^(2*s) := by
…

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

  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechExpectation_scale line 440
  42. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialDilate line 452
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialDilate_eval line 454
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialDilate_degree line 456
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialDilate_mul line 463
  46. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledSechInner line 470
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledSechInner_eq line 472
  48. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledPolynomialChristoffel line 477
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledPolynomialChristoffel_eq line 479
  50. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledPolynomialChristoffel_bounds line 498

    Source documentation

    Inverse Christoffel kernel for the actual normalized sech measure at arbitrary positive decay rate, evaluated at a fixed negative square.

    theorem scaledPolynomialChristoffel_bounds {c y : ℝ} (hc : 0 < c) (hy : 0 < y) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*(n+1:ℝ)^(2*c*y/Real.pi) ≤ scaledPolynomialChristoffel c n (-(y^2)) ∧
      scaledPolynomialChristoffel c n (-(y^2)) ≤ C*(n+1:ℝ)^(2*c*y/Real.pi) := by
…

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