OAI/Combinatorics/HoneycombChords/PositiveJets.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Positive confluent power and hyperbolic kernel determinants and Andreief integration.

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signVariations_lt_support line 15
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_roots_lt_support line 32
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_polynomial_eq_zero line 36
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_det_ne_zero line 70
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_det_pos_geometric line 86
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_det_pos line 100
  7. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis line 140
  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonQuot line 142
  9. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonCoeff line 145
  10. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder line 147
  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet line 149
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis_succ line 151
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newton_decomposition line 154
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonQuot_natDegree_le line 165
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coeff_divByMonic_linear_fixed line 170
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_newtonQuot_coeff line 180
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_newtonCoeff line 193
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.taylor_nodal_product line 208
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_nodal_product_self line 226
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_mul_nodal_product_zero line 234
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder_lt_count line 239
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_newtonBasis_gt line 251
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_newtonBasis_diagonal line 254
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_decomposition line 258
  25. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonJetMatrix line 280
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonJetMatrix_det line 282
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonJetMatrix_det_pos line 290
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_det_factorization line 300
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder_eq_zero_strict line 308
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_zero line 316
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newton_power_det_pos line 318
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newton_power_det_nonneg line 330
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_jet_det_nonneg line 355
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonQuot_natDegree line 361
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonQuot_leadingCoeff line 366
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonQuot_eq_zero_of_lt line 376
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonCoeff_X_pow_diagonal line 386
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonCoeff_X_pow_above line 396
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newton_consecutive_det line 400
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.consecutive_jet_det_pos line 406
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_rectangular_expansion line 419
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_rectangular_binet line 432
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sorted_injective_exponents line 464
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_jet_det_pair_nonneg line 481
  45. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelPartial line 507
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelPartial_det_lower line 510
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_X_pow line 552
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_hasDerivAt line 555
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_X_pow_bound line 563
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.summable_evenFactorial line 571
  51. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTerm line 575
  52. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet line 577
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTerm_bound line 578
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTerm_summable line 587
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_hasDerivAt_left line 590
  56. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_symm line 610
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_hasDerivAt_right line 616
  58. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_iteratedDeriv_left line 627
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_iteratedDeriv_right line 637
  60. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_mixed line 640
  61. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_zero_zero_cosh line 646
  62. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelPartial_tendsto line 655
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_det_pos line 659
  64. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix line 689
  65. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramMatrix line 690
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_evaluation_product_expansion line 692
  67. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integrable_det_evaluation_product line 704
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.andreief line 713
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sorted_injective_real line 753
  70. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetEvaluation line 770
  71. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetEvaluation_det_pos line 772
  72. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetEvaluation_det_product_pos line 792
  73. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetEvaluation_det_product_nonneg line 810