"Only if": a moment sequence has a positive definite Hankel kernel

Proved

HamburgerMoment.hankelPosDef_of_isMomentSequence

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

hankel-matrixmoment-problem

Let $m=(m_n)_{n\ge0}$ be a real sequence that is the moment sequence of some positive Borel measure on $\mathbb R$ . Then its Hankel kernel is positive definite:

\sum_{j,k\ge0}m_{j+k}\,c_j\,\overline{c_k}\ \ge\ 0

for every finitary complex sequence $(c_j)_{j\ge0}$ .

This is the necessity half of Hamburger's characterization.

Preamble

import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory

Formal statement

namespace HamburgerMoment

theorem hankelPosDef_of_isMomentSequence (m : ℕ → ℝ) (hm : IsMomentSequence m) :
    HankelPosDef m := by sorry

end HamburgerMoment

Source

Wikipedia, "Hamburger moment problem", revision oldid=1356180072, https://en.wikipedia.org/w/index.php?title=Hamburger_moment_problem&oldid=1356180072, section "Characterization", "only if" paragraph

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph