The Hausdorff positivity (complete-monotonicity) criterion

hausdorff_positivity_criterion

Submitter: Kim Morrison.

Notes: A multi-indexed real sequence is a positive moment configuration on the unit cube Iᵈ (realized by a positive finite measure) iff it is completely monotone: all iterated backward differences are nonnegative, (Δᵏa)ₙ ≥ 0 for all k ≤ n. Shares the §115 trusted scaffolding (cube, monomial, momentOf, multiChoose, diff, IsPositiveMomentConfiguration). Not in Mathlib (no completely-monotone sequences / Hausdorff moment problem). Companion candidate from §115 of the Knill survey.

Source: F. Hausdorff, *Summationsmethoden und Momentfolgen I, II*, Math. Z. 9 (1921). Knill, *Some fundamental theorems in mathematics*, §115.

Informal solution: Classical Hausdorff moment problem (positive case). Forward: if aₙ = ∫ xⁿ dμ with μ ≥ 0, then (Δᵏa)ₙ = ∫ x^{n−k}(1−x)ᵏ dμ ≥ 0 since the integrand is nonnegative on the cube. Converse (complete monotonicity ⇒ positive realizing measure): the Bernstein/Hausdorff construction — the nonnegative numbers C(n,k)(Δᵏa)ₙ define positive masses on a refining sequence of cube partitions, giving a consistent family of positive measures of bounded total mass a_0; take a weak-* limit (Helly/Banach–Alaoglu + Riesz) to get a finite positive measure μ on Iᵈ with the prescribed moments.

theorem declaration uses `sorry`hausdorff_positivity {d : ℕ} (a : (Fin d → ℕ) → ℝ) :
    LeanEval.Analysis.IsPositiveMomentConfiguration a ↔ ∀ k n : Fin d → ℕ, k ≤ n → 0 ≤ diff a k n := byd:ℕa:(Fin d → ℕ) → ℝ⊢ IsPositiveMomentConfiguration a ↔ ∀ (k n : Fin d → ℕ), k ≤ n → 0 ≤ diff a k n
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026