Hausdorff moment problem: absolute-continuity criterion

hausdorff_absolute_continuity

Submitter: Kim Morrison.

Notes: A positive probability measure μ supported on the unit cube (μ ((cube d)ᶜ) = 0) is uniformly absolutely continuous w.r.t. Lebesgue measure iff its iterated moment differences are dominated by those of Lebesgue measure (∃ C, (Δᵏμ)ₙ ≤ C·(Δᵏν)ₙ for k ≤ n). Trusted helpers (cube, monomial, momentOf, multiChoose, diff, UniformlyAbsolutelyContinuous) are non-holes. Companion of the §115 realizability and positivity criteria (already submitted). Mathlib has SignedMeasure and set integrals but no moment-problem machinery. Candidate from §115 (additional 2).

Source: F. Hausdorff (1921–1923); see Shohat–Tamarkin, *The Problem of Moments*. Knill, *Some fundamental theorems in mathematics*, §115.

Informal solution: Hausdorff's absolute-continuity criterion for the cube moment problem. Forward: if μ ≤ C·ν then the Bernstein/difference functionals satisfy (Δᵏμ)ₙ = ∫ x^{n−k}(1−x)ᵏ dμ ≤ C ∫ x^{n−k}(1−x)ᵏ dν = C·(Δᵏν)ₙ since the kernels are nonnegative. Converse: the dominated-difference condition says the Bernstein polynomials approximating dμ/dν are uniformly bounded, so the Radon–Nikodym density is essentially bounded by C; pass to the weak-* limit of the Bernstein densities (Helly) to conclude μ ≤ C·ν. The Bernstein-density machinery for the cube is not in Mathlib.

theorem declaration uses `sorry`hausdorff_absolute_continuity {d : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin d)))
    [IsProbabilityMeasure μ] (hμ : μ ((LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d)ᶜ) = 0) :
    LeanEval.Analysis.HausdorffAbsoluteContinuity.UniformlyAbsolutelyContinuous μ (volume.restrict (LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d)) ↔
      ∃ C : ℝ, ∀ k n : Fin d → ℕ, k ≤ n →
        diff (momentOf μ) k n ≤ C * diff (momentOf (volume.restrict (LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d))) k n := byd:ℕμ:Measure (EuclideanSpace ℝ (Fin d))inst✝:IsProbabilityMeasure μhμ:μ (cube d)ᶜ = 0⊢ UniformlyAbsolutelyContinuous μ (volume.restrict (cube d)) ↔
  ∃ C, ∀ (k n : Fin d → ℕ), k ≤ n → diff (momentOf μ) k n ≤ C * diff (momentOf (volume.restrict (cube d))) k n
  sorryAll goals completed! 🐙

Solved by

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