OAI/Combinatorics/HoneycombChords/PolynomialKernels.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Matrix and polynomial Christoffel kernels

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel line 20
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_pos line 22
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetric_dot_mulVec line 25
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_bound line 29
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_ratio_bound line 50
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_ratio_attained line 60
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_variational line 70
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_single line 83
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_first_cofactor line 86
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel_congruence line 92
  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialVector line 110
  12. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram line 111
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ofFn_eval_eq_dot line 113
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomial_pair_integrable line 116
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram_quadratic line 120
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram_norm_integrable line 138
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_square_eval_ae_ne_zero line 153
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram_posDef line 166
  19. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisMatrix line 196
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisMatrix_det line 198
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisMatrix_eval_zero line 218
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisMatrix_eval_succ line 221
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisMatrix_eval_self line 227
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram_congruence_entry line 233
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rootBasisGram_minor line 254
  26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_compression_cofactor line 265

    Source documentation

    Gram cofactor identity used in the manuscript's polynomial comparison.

    theorem polynomial_compression_cofactor (n : ℕ) (a : ℝ) (w : ℝ → ℝ)
    (hi : ∀ k : ℕ,IntegrableOn (fun p : ℝ=>p^k*w p) (Set.Ioi 0)) :
    (monomialGram n (fun p=>(p^2-a)^2*w p)).det/(monomialGram (n+1) w).det=
      matrixChristoffel (monomialGram (n+1) w) (monomialVector (n+1) a) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.matrixChristoffel, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomialVector

  27. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialNorm line 282
  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel line 284
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialNorm_integrable line 286
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialNorm_nonneg line 292
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel_eq line 297
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomial_ratio_bound line 316
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomial_ratio_attained line 326
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialNorm_pos line 335
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedPolynomialChristoffel_comparison line 345