hausdorff_positivity_criterion.toml

id = "hausdorff_positivity_criterion"
title = "The Hausdorff positivity (complete-monotonicity) criterion"
test = false
module = "LeanEval.Analysis.HausdorffMoments"
holes = ["hausdorff_positivity"]
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."