Prove2Me

∫p(x)2 dμ=∑j,kajakmj+k≥0\int p(x)^2\,d\mu=\sum_{j,k}a_ja_km_{j+k}\ge0 for real polynomials pp

Proved
HamburgerMoment.integral_poly_sq_eq_and_nonneg

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

hankel-matrixmoment-problem

Let μ\mu be a solution of the Hamburger moment problem for the real sequence mm. Then for every n≥0n\ge0 and every real polynomial

p(x)=∑j=0najxj(a0,…,an∈R)p(x)=\sum_{j=0}^{n}a_jx^j\qquad(a_0,\dots,a_n\in\mathbb R)

one has

∫p(x)2 dμ=∫(∑j,k=0najakxj+k)dμ=∑j,k=0najakmj+k ≥ 0.\int p(x)^2\,d\mu=\int\Big(\sum_{j,k=0}^{n}a_ja_kx^{j+k}\Big)d\mu=\sum_{j,k=0}^{n}a_ja_km_{j+k}\ \ge\ 0.

This is the statement that each real Hankel matrix Δn\Delta_n of a moment sequence is positive semidefinite.

Formalization Note The coefficients are given as a function a : ℕ → ℝ, of which only a0,…,ana_0,\dots,a_n are used.

Preamble
import Mathlib
import Definitions.Def_HamburgerMoment_Defs

open MeasureTheory
Formal statement
namespace HamburgerMoment

theorem integral_poly_sq_eq_and_nonneg (m : ℕ → ℝ) (μ : Measure ℝ)
    (hμ : IsMomentMeasure m μ) (n : ℕ) (a : ℕ → ℝ) :
    ∫ x, (∑ j ∈ Finset.range (n + 1), a j * x ^ j) ^ 2 ∂μ =
        ∑ j ∈ Finset.range (n + 1), ∑ k ∈ Finset.range (n + 1), a j * a k * m (j + k) ∧
      0 ≤ ∑ j ∈ Finset.range (n + 1), ∑ k ∈ Finset.range (n + 1), a j * a k * m (j + k) := 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 "Polynomials", displayed identity
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