OAI/Combinatorics/HoneycombChords/LaplaceProducts.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Euler products and positive rational approximants of the strip test functions.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.prod_range_even_odd line 16
  2. def OAI.CriticalHoneycomb.FiniteFunctional.cosineEulerProduct line 25
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.cosineEulerProduct_relation line 28
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.tendsto_cosineEulerProduct line 50
  5. def OAI.CriticalHoneycomb.FiniteFunctional.cEulerProduct line 73
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.cEulerProduct_eq_cosineEulerProduct line 76
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.tendsto_cEulerProduct line 85
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.restrict_admissibleDensity line 139
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_in_pairingDomain line 171
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.div_D_in_pairingDomain line 180
  11. def OAI.CriticalHoneycomb.FiniteFunctional.hZero line 189
  12. def OAI.CriticalHoneycomb.FiniteFunctional.hOne line 190
  13. def OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection line 191
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZero_in_pairingDomain line 193
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_in_pairingDomain line 197
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_in_pairingDomain line 202
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection_in_pairingDomain line 207
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_re_pos line 221
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_two_mul line 231
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_three_mul line 241
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_mul_cOne line 251
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.half_angle_pole_condition line 259
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.three_half_angle_pole_condition line 263
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.cOne_ne_zero line 268
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_ne_zero line 273
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_ne_zero_on_source line 278
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZero_cosh_ratio line 284
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_cosh_ratio line 289
  29. def OAI.CriticalHoneycomb.FiniteFunctional.physicalPole line 295

    Source documentation

    The actual nearest pole is 64/9, with every third pole cancelled.

    noncomputable def physicalPole (n : ℕ) : ℝ := (64/9)*(2*(n:ℝ)+1)^2
  30. def OAI.CriticalHoneycomb.FiniteFunctional.poleFactor line 296
  31. def OAI.CriticalHoneycomb.FiniteFunctional.hZeroProduct line 297
  32. def OAI.CriticalHoneycomb.FiniteFunctional.hOneProduct line 299
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.physicalPole_pos line 302
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.physicalPole_ge line 303
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleFactor_re_pos line 307
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleFactor_ne_zero line 314
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.cEulerProduct_three_half line 320
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.cEulerProduct_half line 331
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.prod_range_three line 345
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZeroProduct_eq_ratio line 357
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOneProduct_eq_ratio line 367
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.tendsto_hZeroProduct line 377
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.tendsto_hOneProduct line 386