OAI/Combinatorics/HoneycombChords/SparseInterpolation.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Sparse Newton interpolation and positive reciprocal product comparisons.

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonEvaluation line 16
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonEvaluation_det_pos line 19
  3. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseCofactorMatrix line 28
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseCofactorMatrix_det_nonneg line 32
  5. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseTestMatrix line 51
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseTestMatrix_factor line 55
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseTestMatrix_det_nonneg line 68
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_newton_numerator_nonneg line 77

    Source documentation

    The alternating-Newton polynomial divided-difference numerator is nonnegative against the sparse interpolation weights at the origin.

    lemma sparse_newton_numerator_nonneg {n : ℕ} (v : ℕ → ℝ) (hv : ∀ i,0≤v i)
    (hord : StrictMono (fun i : Fin (n+1)=>v i))
    (e : Fin n → ℕ) (he : StrictMono e) (k : Fin (n+1)) :
    0≤Matrix.det (Fin.cases (fun j : Fin (n+1)=>v j*((-1)^k.val*(newtonBasis v k).eval (v j)))
      (fun i j=>(v j)^(e i+1))) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis

  9. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseExponent line 105
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseExponent_strictMono line 108
  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseMatrix line 113
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseMatrix_eq line 116
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseMatrix_det_pos line 121
  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseWeight line 126
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseWeight_eval line 129
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseWeight_sum line 147
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseWeight_power line 153
  18. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.backwardNewton line 163
  19. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeProd line 165
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.backwardNewton_eval line 167
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeProd_pos line 174
  22. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coxianWeight line 177
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coxianWeight_nonneg line 180
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.backwardNewton_telescope line 190
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.backwardNewton_node line 204
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coxianWeight_sum line 208
  27. inductive OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr line 239
  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.eval line 246
  29. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.PolesAbove line 252
  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.CoeffNonneg line 258
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.eval_nonneg line 264
  32. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.difference line 272
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.difference_poles line 278
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.difference_coeff_nonneg line 286
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.difference_identity line 295
  36. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr line 317
  37. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonCoefficient line 320
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr_poles line 323
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr_coeff_nonneg line 329
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonCoefficient_nonneg line 336
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newton_expansion line 341
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newton_evaluation line 357
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr_add line 363
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr_scale line 368
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonCoefficient_add line 373
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonCoefficient_scale line 376
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonExpr_eval_congr line 380
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.newtonCoefficient_congr line 400
  49. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval line 419
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_add line 422
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_scale line 425
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_rational line 429
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_rational_nonneg line 444
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_polynomial_zero line 454
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.coxianWeight_eq_zero line 472
  56. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleProduct line 496
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleProduct_pos line 499
  58. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleProduct_antitone line 501
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonExpr_head line 508
  60. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonExpr_zero line 518
  61. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonExpr_reciprocal line 524
  62. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonCoefficient_reciprocal line 536
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_reciprocal line 543
  64. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_reciprocal_lower line 556
  65. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_reciprocal_upper line 568
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.poles_mono line 595
  67. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.mulExpr line 603
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.mulExpr_eval line 609
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.mulExpr_poles line 617
  70. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.mulExpr_coeff line 624
  71. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.normalizedPole line 632
  72. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.normalizedPole_eval line 633
  73. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.normalizedPole_poles line 635
  74. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.normalizedPole_coeff line 636
  75. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.lower_product_identity line 639

    Source documentation

    The positive remainder giving the lower complementary-product bound.

    lemma lower_product_identity {A : ReciprocalExpr} {a x : ℝ}
    (ha : 0 < a) (hA : A.PolesAbove 0) (hz : A.eval 0 = 1) (hx : 0 ≤ x) :
    1-a/(a+x)*A.eval x = x/(a+x)+x*(scale a (pole a (A.difference 0))).eval x := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.eval

  76. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.upper_product_identity line 651

    Source documentation

    The upper comparison is the double positive divided difference at -a,0.

    lemma upper_product_identity {A : ReciprocalExpr} {a x : ℝ}
    (ha : 0 < a) (hA : A.PolesAbove a) (hz : A.eval 0 = 1) (hx : 0 ≤ x) :
    A.eval (-a)*(x/(a+x))-(1-a/(a+x)*A.eval x) =
      x*(scale a ((A.difference (-a)).difference 0)).eval x := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.difference, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.eval

  77. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr.complementary_identity line 668
  78. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval_congr_nodes line 676
  79. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_complement_nonneg line 683
  80. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_product_lower line 695
  81. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_product_upper line 710

    Source documentation

    Exact sparse prefix-node upper product. The harmless constant is the remaining normalized product evaluated at its slowest pole.

    lemma sparse_product_upper {n q : ℕ} {A : ReciprocalExpr}
    (v : ℕ → ℝ) (e : Fin n → ℕ) (hv : ∀ i,0 < v i)
    (hord : StrictMono (fun i : Fin (n+1) => v i)) (he : StrictMono e)
    (hq : ∀ m,1 ≤ m → m ≤ q → ∃ i,e i+1=m)
    {a : ℝ} (ha : 0 < a) (hA : A.PolesAbove a) (hp : A.CoeffNonneg) (hz : A.eval 0=1) :
    sparseEval v e (fun x => 1-a/(a+x)*A.eval x) ≤ A.eval (-a)*poleProduct v a (q+1) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ReciprocalExpr, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleProduct

  82. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_complement_upper line 740
  83. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_mixture_bounds line 759