OAI/Combinatorics/HoneycombChords/NewtonKernel.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Total positivity and convergence of Newton interpolation kernels.

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TotallyNonnegative line 16
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.lowerBidiagonal_totallyNonnegative line 20
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.totallyNonnegative_one line 46
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sorted_injective_fin line 54
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TotallyNonnegative.mul line 68
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TotallyNonnegative.adjacent_row line 96
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TotallyNonnegative.prefix_recursive line 139
  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftNewton line 175
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftNewton_zero_zero line 179
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftNewton_zero_succ line 180
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftNewton_succ_zero line 181
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftNewton_succ_succ line 182
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TotallyNonnegative.lift_newton line 184
  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton line 259
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_zero line 264
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_eq_zero line 268
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_totallyNonnegative line 276
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_det_nonneg line 306
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis_head line 319
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_expansion line 324
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_expansion_truncated line 348
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis_eval_zero line 356
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_evaluation line 364

    Source documentation

    Evaluation factors through the first m Newton coefficients, even for a sparse power whose degree is much larger than m.

    lemma powerNewton_evaluation {m : ℕ} (v : ℕ → ℝ) (n : ℕ) (j : Fin m) :
    v j^n=∑ k : Fin m,powerNewton v n k*(newtonBasis v k).eval (v j) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonBasis

  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_bound line 389
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_powerNewton line 410
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_jet_evaluation line 420
  27. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernelTerm line 437
  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel line 439
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernelTerm_bound line 442
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernelTerm_summable line 453
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_newton line 459
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuousOn_newtonKernel line 476
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_det_newton line 487
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_nonneg line 507
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_mono line 515
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder_const line 527
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_newtonBasis_const line 530
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.powerNewton_const line 536
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_const line 543
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_nonneg line 550
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_le_jet line 559
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_exp_bound line 575
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonJetMatrix_det_ne_zero line 592
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_as_combination line 600
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_newtonKernel line 612
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_newtonKernel_of_bounded line 622