OAI/Combinatorics/HoneycombChords/StripProducts.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Polynomial characteristic products for the strip density

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity_moments line 17
  2. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripPolynomialChristoffel_bounds line 28

    Source documentation

    Christoffel estimates for the strip measure divided by (x + z²)².

    theorem stripPolynomialChristoffel_bounds {z y : ℝ} (hz : 0 < z) (hy : 0 < y) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*((n:ℝ)+1)^(3*y/4) ≤ weightedPolynomialChristoffel (squaredPoleDensity z) n (-(y^2)) ∧
      weightedPolynomialChristoffel (squaredPoleDensity z) n (-(y^2)) ≤ C*((n:ℝ)+1)^(3*y/4) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity

  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_compression_ratio line 88
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPole_restore line 99
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPole_tilt line 105
  6. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_polynomial_square_product line 113

    Source documentation

    Exact square-product identity, with the actual strip measure.

    theorem strip_polynomial_square_product (n : ℕ) {y z : ℝ} (hz : 0 < z) :
    (monomialGram n (fun p=>characteristicRatio y z p^2*stripDensity p)).det /
      (monomialGram n stripDensity).det =
      weightedPolynomialChristoffel (squaredPoleDensity z) n (-(y^2)) /
      weightedPolynomialChristoffel (squaredPoleDensity z) n (-(z^2)) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity

  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio_pos line 129
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio_bounds line 131
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomial_moments_bounded line 144
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_squaredPole_moments line 155
  11. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_stripPolynomialChristoffel_bounds line 163

    Source documentation

    Kernel exponent is unchanged by the bounded positive characteristic tilt.

    theorem tilted_stripPolynomialChristoffel_bounds {y z v : ℝ} (hy : 0 < y) (hz : 0 < z) (hv : 0 < v) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*((n:ℝ)+1)^(3*v/4) ≤ weightedPolynomialChristoffel
        (fun p=>characteristicRatio y z p*squaredPoleDensity z p) n (-(v^2)) ∧
      weightedPolynomialChristoffel
        (fun p=>characteristicRatio y z p*squaredPoleDensity z p) n (-(v^2)) ≤ C*((n:ℝ)+1)^(3*v/4) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity

  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_ratio_bounds line 199
  13. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_polynomial_square_product_bounds line 222

    Source documentation

    Polynomial square-product exponent for the genuine strip density.

    theorem strip_polynomial_square_product_bounds {y z : ℝ} (hy : 0 < y) (hz : 0 < z) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*((n:ℝ)+1)^(3*(y-z)/4) ≤
        (monomialGram n (fun p=>characteristicRatio y z p^2*stripDensity p)).det/(monomialGram n stripDensity).det ∧
      (monomialGram n (fun p=>characteristicRatio y z p^2*stripDensity p)).det/(monomialGram n stripDensity).det ≤
        C*((n:ℝ)+1)^(3*(y-z)/4) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_squaredPole_restore line 233
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_squaredPole_tilt line 240
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_strip_polynomial_square_product line 247
  17. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tilted_strip_polynomial_square_product_bounds line 258

    Source documentation

    The second square-product estimate needed for the Cauchy--Schwarz squeeze.

    theorem tilted_strip_polynomial_square_product_bounds {y z : ℝ} (hy : 0 < y) (hz : 0 < z) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*((n:ℝ)+1)^(3*(y-z)/4) ≤
        (monomialGram n (fun p=>characteristicRatio y z p^2*(characteristicRatio y z p*stripDensity p))).det /
          (monomialGram n (fun p=>characteristicRatio y z p*stripDensity p)).det ∧
      (monomialGram n (fun p=>characteristicRatio y z p^2*(characteristicRatio y z p*stripDensity p))).det /
          (monomialGram n (fun p=>characteristicRatio y z p*stripDensity p)).det ≤ C*((n:ℝ)+1)^(3*(y-z)/4) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  18. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialPointDensity line 278
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomial_gram_andreief line 280
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialPointDensity_tilt line 309
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialPointDensity_nonneg line 313
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integral_weighted_square line 321
  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram_tilt_square line 337

    Source documentation

    Cauchy--Schwarz for the genuine polynomial determinant density.

    theorem monomialGram_tilt_square (n : ℕ) (w r : ℝ → ℝ)
    (hw : ∀ p,0 < p → 0 < w p)
    (hi : ∀ k : ℕ,IntegrableOn (fun p : ℝ=>p^k*w p) (Set.Ioi 0))
    (hi1 : ∀ k : ℕ,IntegrableOn (fun p : ℝ=>p^k*(r p*w p)) (Set.Ioi 0))
    (hi2 : ∀ k : ℕ,IntegrableOn (fun p : ℝ=>p^k*(r p^2*w p)) (Set.Ioi 0)) :
    (monomialGram n (fun p=>r p*w p)).det^2 ≤
      (monomialGram n (fun p=>r p^2*w p)).det*(monomialGram n w).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram

  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_moments line 369
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristic_tilt_moments line 375
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.square_le_power_upper line 381
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_product_squeeze line 387
  28. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_polynomial_characteristic_product_bounds line 416

    Source documentation

    Characteristic product estimates for the strip density.

    theorem strip_polynomial_characteristic_product_bounds {y z : ℝ} (hy : 0 < y) (hz : 0 < z) :
    ∃ a C : ℝ,0 < a ∧ 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      a*((n:ℝ)+1)^(3*(y-z)/8) ≤
        (monomialGram n (fun p=>characteristicRatio y z p*stripDensity p)).det/(monomialGram n stripDensity).det ∧
      (monomialGram n (fun p=>characteristicRatio y z p*stripDensity p)).det/(monomialGram n stripDensity).det ≤
        C*((n:ℝ)+1)^(3*(y-z)/8) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixner_even_coefficient_uniform line 478

    Source documentation

    A parameter-uniform bound for growing arguments of order N^(3/4).

    lemma meixner_even_coefficient_uniform {s:ℝ} (hs : (1 : ℝ) / 2  ≤  s) (n j:ℕ) (hj : j  ≤  n) :
    meixnerCoeff s (2*j) ≤ ((n:ℝ)+1)*(4*((n:ℝ)+1))^(s+1/2) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meixnerCoeff

  30. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenCoefficientKernel_uniform line 519
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_exponential_lower line 541
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_slower_sech_upper line 551
  33. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledStripDensity line 576
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledStripDensity_sech_bounds line 577
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.growing_pole_denominator line 605
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.growing_squaredPole_lower line 624

    Source documentation

    Parameter-uniform pole comparison needed in strip-asymptotics:107. The constants do not depend on the pole z, which may grow with N.

    lemma growing_squaredPole_lower :
    ∃ c a : ℝ, 0<c ∧ 0<a ∧ ∀ z : ℝ, 1 ≤ z → ∀ p : ℝ, 0<p →
      (a/z^4)*sechWeight c p ≤ squaredPoleDensity z p := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechWeight, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity

  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPole_le_strip line 657
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.growing_squaredPole_kernel_lower line 661
  39. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_polynomial_square_product_uniform line 687

    Source documentation

    Growing-argument square-product bound for the literal strip measure. No fixed-parameter asymptotic is applied to a moving evaluation point.

    theorem strip_polynomial_square_product_uniform :
    ∃ c C : ℝ, 0<c ∧ 0<C ∧ ∀ y z : ℝ, 1 ≤ z → 1/2 ≤ c*y/Real.pi → ∀ n : ℕ,
      (monomialGram n (fun p=>characteristicRatio y z p^2*stripDensity p)).det /
        (monomialGram n stripDensity).det ≤
      C*z^4*((n:ℝ)+1)^3*(4*((n:ℝ)+1))^(2*c*y/Real.pi+1) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity