Hamburger's theorem: $m$ is a moment sequence iff its Hankel kernel is positive definite

Proved

HamburgerMoment.hamburger_moment_problem

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

hankel-matrixmoment-problem

Let $m=(m_n)_{n\ge0}$ be a sequence of real numbers. The Hamburger moment problem for $m$ is solvable — that is, there is a positive Borel measure $\mu$ on $\mathbb R$ with all moments finite and

m_n=\int_{-\infty}^{\infty}x^n\,d\mu(x)\qquad(n\ge0)

— if and only if the Hankel kernel $A=(m_{j+k})_{j,k\ge0}$ is positive definite, i.e.

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

for every finitary sequence $(c_j)_{j\ge0}$ of complex numbers ( $c_j=0$ for all but finitely many $j$ ).

This is the main theorem of the mission: it reduces the existence of a representing measure to positivity conditions on the data.

Preamble

import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory

Formal statement

namespace HamburgerMoment

theorem hamburger_moment_problem (m : ℕ → ℝ) :
    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", first paragraph and displayed condition

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

Hamburger's theorem: mmm is a moment sequence iff its Hankel kernel is positive definite

Hamburger's theorem: $m$ is a moment sequence iff its Hankel kernel is positive definite