OAI/Combinatorics/HoneycombChords/TaylorInterpolation.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Translated Taylor minors and physical interpolation residual bounds.

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_X_pow_above line 15
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_X_pow_sum line 19
  3. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm line 25
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm_above line 28
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm_bound line 32
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm_norm_row_bound line 47
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm_summable line 61
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelTaylorTerm_row_sum line 76
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_translation_summable line 89
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_translation line 94
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_at_zero_all line 114
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder_initial_zero line 123
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_sum_coeff line 132
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_shifted_power line 141
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_coeff_det_zero_missing line 146
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedKernelMatrix line 192
  17. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelComplementMatrix line 194
  18. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelOriginFunctional line 198
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_origin_modified_hasSum line 202
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_origin_det_bounds line 222

    Source documentation

    Infinite Cauchy--Binet bound for the exact translated kernel. The only input on g is the previously proved sparse polynomial-functional inequality.

    lemma kernel_origin_det_bounds {n q : ℕ} {a R : ℝ}
    (ha : 0 ≤ a) (hR : 0 < R) (hphase : Real.sqrt R*Real.sqrt a < Real.pi/2)
    (b v : ℕ → ℝ) (g : ℝ → ℝ)
    (hb : Monotone (fun i : Fin (n+1)=>b i)) (hball : ∀ i,0 ≤ b i ∧ b i ≤ R)
    (hq : q ≤ n) (hbzero : ∀ i,i ≤ q → b i=0)
    (hv : ∀ i : Fin (n+1),0 < v i) (hord : StrictMono (fun i : Fin (n+1)=>v i))
    {L U : ℝ}
    (hbound : ∀ e : Fin n → ℕ,StrictMono e →
      (∀ k,1 ≤ k → k ≤ q → ∃ i,e i+1=k) → L ≤ sparseEval v e g ∧ sparseEval v e g ≤ U) :
    L*(translatedKernelMatrix (n:=n+1) b a v).det ≤ (kernelComplementMatrix (n:=n+1) b a v g).det ∧
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.g, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparseEval, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedKernelMatrix, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelComplementMatrix

  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedKernelMatrix_det_pos line 273
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_origin_bounds line 284
  23. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroShiftProduct line 308
  24. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oneShiftProduct line 311
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalizedFast_tail_poles line 314
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalizedFast_tail_coeff line 317
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalizedFast_tail_zero line 320
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_zero_shift_bounds line 324
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sparse_one_shift_bounds line 347
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_zero_shift_bounds line 386
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_one_shift_bounds line 397
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_ofReal_re line 418
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZero_ofReal_re line 423
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_ofReal_re line 431
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZero_re_pos line 435
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_re_pos line 440
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedPole_normalization line 448
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedNumerator_normalization line 458
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pair_shift_ratio line 468
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.triple_shift_ratio line 476
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroShiftProduct_eq_prod line 489
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oneShiftProduct_eq_prod line 496
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroShiftProduct_ratio line 502
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.oneShiftProduct_ratio line 506
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_zeroShiftProduct line 511
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_oneShiftProduct line 522
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelOriginFunctional_tendsto line 545
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_hZero_bounds line 561
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_hOne_bounds line 577
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.source_translation_phase line 593
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.source_hZero_kernel_bounds line 606

    Source documentation

    Physical sorted flag specialization; all original confluent nodes remain.

    lemma source_hZero_kernel_bounds {N : ℕ} (hN : 1 ≤ N) {u : ℝ}
    (hu : 0 ≤ u) (hu4 : u ≤ 4) {t : ℝ} (ht : 0<t) (htL : t<angle)
    (x : ℕ → ℝ) (hx : ∀ i,0<x i) (hord : StrictMono (fun i : Fin (2*N+1)=>x i)) :
    poleProduct (fun j=>x j+u) (shiftedPole u 0) (2*N+1) ≤
      kernelOriginFunctional (n:=2*N+1) (interiorKnotLabels N t) u (fun j=>x j+u)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleProduct, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.shiftedPole, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelOriginFunctional, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnotLabels

  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.source_hOne_kernel_bounds line 625