The solutions of the Hamburger moment problem form a convex set

Proved

HamburgerMoment.isMomentMeasure_convex

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

hankel-matrixmoment-problem

Let $m=(m_n)_{n\ge0}$ be a real sequence and let $\mu,\nu$ be two solutions of its Hamburger moment problem (positive Borel measures on $\mathbb R$ with $x^n$ integrable and $\int x^n\,d\mu=\int x^n\,d\nu=m_n$ for all $n$ ). Then for every $t\in[0,1]$ the measure

t\,\mu+(1-t)\,\nu

is again a solution.

Formalization Note The scalars $t$ and $1-t$ act on measures through ENNReal.ofReal.

Preamble

import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory

Formal statement

namespace HamburgerMoment

theorem isMomentMeasure_convex (m : ℕ → ℝ) (μ ν : Measure ℝ)
    (hμ : IsMomentMeasure m μ) (hν : IsMomentMeasure m ν) (t : ℝ) (ht0 : 0 ≤ t)
    (ht1 : t ≤ 1) :
    IsMomentMeasure m (ENNReal.ofReal t • μ + ENNReal.ofReal (1 - t) • ν) := 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 "Uniqueness of solutions", first sentence

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