Prove2Me

If det⁡Δn=0\det\Delta_n=0 for some nn, the solution is unique and finitely supported

Proved
HamburgerMoment.unique_finite_support_of_det_eq_zero

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

hankel-matrixmoment-problem

Let m=(mn)n≥0m=(m_n)_{n\ge0} be a real sequence whose Hankel kernel is positive definite, and suppose that

det⁡(Δn)=0\det(\Delta_n)=0

for some n≥0n\ge0, where Δn=(mi+j)0≤i,j≤n\Delta_n=(m_{i+j})_{0\le i,j\le n}. Then the Hamburger moment problem for mm has exactly one solution μ\mu, and μ\mu has finite support: there is a finite set S⊂RS\subset\mathbb R with μ(R∖S)=0\mu(\mathbb R\setminus S)=0.

Preamble
import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory
Formal statement
namespace HamburgerMoment

theorem unique_finite_support_of_det_eq_zero (m : ℕ → ℝ) (hm : HankelPosDef m) (n : ℕ)
    (hdet : (hankelMatrix m n).det = 0) :
    ∃ μ : Measure ℝ, (∀ ν : Measure ℝ, IsMomentMeasure m ν ↔ ν = μ) ∧
      ∃ S : Finset ℝ, μ (↑S)ᶜ = 0 := 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 "If det(Δn) = 0, for some n, then (H, ⟨,⟩) is finite-dimensional and T is self-adjoint. So in this case the solution to the Hamburger moment problem is unique and μ ... has finite support"
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