Hankel form as an integral: $\sum m_{j+k}c_j\overline{c_k}=\int|\sum c_jx^j|^2\,d\mu$

Proved

HamburgerMoment.hankelForm_eq_integral

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

hankel-matrixmoment-problem

Let $\mu$ be a solution of the Hamburger moment problem for the real sequence $m$ , i.e. a positive Borel measure on $\mathbb R$ with $x^n$ integrable and $\int x^n\,d\mu=m_n$ for all $n\ge0$ . Then for every finitary complex sequence $(c_j)_{j\ge0}$ ,

\sum_{j,k\ge0}m_{j+k}\,c_j\,\overline{c_k}=\int_{-\infty}^{\infty}\Big|\sum_{j\ge0}c_jx^j\Big|^2\,d\mu(x).

This identity is the computation behind the "only if" part of Hamburger's theorem.

Preamble

import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory

Formal statement

namespace HamburgerMoment

theorem hankelForm_eq_integral (m : ℕ → ℝ) (μ : Measure ℝ) (hμ : IsMomentMeasure m μ)
    (c : ℕ →₀ ℂ) :
    hankelForm m c =
      ((∫ x, ‖∑ j ∈ c.support, c j * (x : ℂ) ^ j‖ ^ 2 ∂μ : ℝ) : ℂ) := 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", displayed identity in the "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

Hankel form as an integral: ∑mj+kcjck‾=∫∣∑cjxj∣2 dμ\sum m_{j+k}c_j\overline{c_k}=\int|\sum c_jx^j|^2\,d\mu∑mj+k​cj​ck​​=∫∣∑cj​xj∣2dμ

Hankel form as an integral: $\sum m_{j+k}c_j\overline{c_k}=\int|\sum c_jx^j|^2\,d\mu$