Prove2Me

Some moment sequences have more than one solution

Proved
HamburgerMoment.exists_nonunique_solution

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

hankel-matrixmoment-problem

There exist a real sequence m=(mn)n≥0m=(m_n)_{n\ge0} and two different positive Borel measures μ≠ν\mu\ne\nu on R\mathbb R that both solve its Hamburger moment problem:

∫−∞∞xn dμ(x)=∫−∞∞xn dν(x)=mn(n≥0),\int_{-\infty}^{\infty}x^n\,d\mu(x)=\int_{-\infty}^{\infty}x^n\,d\nu(x)=m_n\qquad(n\ge0),

with all these integrals finite.

So the moment sequence does not determine the measure in general; a classical example is the log-normal distribution.

Preamble
import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory
Formal statement
namespace HamburgerMoment

theorem exists_nonunique_solution :
    ∃ (m : ℕ → ℝ) (μ ν : Measure ℝ), IsMomentMeasure m μ ∧ IsMomentMeasure 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 "Uniqueness of solutions", sentence "There are examples where the solution is not unique" (Chihara 1978, p. 73)
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