OAI/Combinatorics/HoneycombChords/PhysicalFactors.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Physical pole factors and positive mixtures of interpolation kernels.

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.physicalPole_strictMono line 15
  2. def OAI.CriticalHoneycomb.FiniteFunctional.poleTailRatio line 22
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleTailRatio_ge_one line 25
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleTailRatio_le line 32
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleTailProduct_le line 53
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleTailProduct_uniform line 66
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.poleTailSubset_uniform line 72
  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.rangeProduct line 92
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.rangeProduct_eval line 96
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.rangeProduct_poles line 101
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.rangeProduct_coeff line 106
  12. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleWeight line 112
  13. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleFactor line 113
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleWeight_pos line 117
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleWeight_lt_one line 121
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleFactor_coeff line 126
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleFactor_poles line 130
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleFactor_eval line 133
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.normalizedPole_zero line 142
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.tripleFactor_zero line 144
  21. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedPole line 151
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedPole_pos line 152
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedPole_strictMono line 155
  24. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairExpr line 158
  25. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleExpr line 161
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleExpr_poles line 164
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleExpr_coeff line 169
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleExpr_zero line 173
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.slowPole_eval line 188
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tripleFactor_le_pair line 195
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tailScalar_majorant line 203
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tailScalar_uniform line 227
  33. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairTail line 232
  34. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleTail line 234
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairExpr_poles line 237
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairExpr_coeff line 242
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairExpr_zero line 246
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairTail_poles line 250
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleTail_poles line 252
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairTail_coeff line 254
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleTail_coeff line 256
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairTail_zero line 258
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleTail_zero line 260
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalPairTail_uniform line 263
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalTripleTail_uniform line 274
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physical_first_weight_half line 294
  47. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.originPowerData line 311
  48. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coefficientMinor line 313
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.increasing_zero_sparse line 316
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.originPowerData_sparse line 336
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.originPowerData_sparse_det line 342
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coefficient_power_pair_permute line 352
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_mixture_finite_bounds line 367
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_square_cosh line 457
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_first_square line 461
  56. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_ode_zero line 473
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_ode line 489