Hausdorff moment problem

DefinitionClosed unit cube#✓fully proved

For \(d \in \mathbb{N}\), the closed unit cube \(I^d = [0,1]^d\) is the set of points \(x \in \mathbb{R}^d\) with \(0 \le x_i \le 1\) for every coordinate \(i\).

def cube (d : ℕ) : Set (EuclideanSpace ℝ (Fin d)) :=
  {x | ∀ i, x i ∈ Set.Icc (0 : ℝ) 1}

Used by 2

Used byHausdorff's absolute continuity criterion · Moments of a measure on the unit cube

DefinitionMultivariate monomial#✓fully proved

For a multi-index \(n = (n_1, \dots, n_d) \in \mathbb{N}^d\) and a point \(x \in \mathbb{R}^d\), the monomial \(x^n\) is the real number \(\prod_{i=1}^{d} x_i^{n_i}\).

def monomial {d : ℕ} (n : Fin d → ℕ) (x : EuclideanSpace ℝ (Fin d)) : ℝ :=
  ∏ i, (x i) ^ (n i)

Used by 1

Used byMoments of a measure on the unit cube

DefinitionMoments of a measure on the unit cube#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^d\) and a multi-index \(n \in \mathbb{N}^d\), the \(n\)-th moment of \(\mu\) is the real number \(\int_{I^d} x^n \, d\mu(x)\), the integral over the closed unit cube \(I^d = [0,1]^d\) of the monomial \(x^n = \prod_{i=1}^{d} x_i^{n_i}\), taken to be \(0\) when the monomial is not \(\mu\)-integrable on \(I^d\).

noncomputable def momentOf {d : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin d)))
    (n : Fin d → ℕ) : ℝ :=
  ∫ x in cube d, monomial n x ∂μ

Uses 2 · Used by 1

Statement usesClosed unit cube · Multivariate monomial

Used byHausdorff's absolute continuity criterion

DefinitionMulti-index binomial coefficient#✓fully proved

For multi-indices \(n, k \in \mathbb{N}^d\), the binomial coefficient \(\binom{n}{k}\) is the natural number \(\prod_{i=1}^{d} \binom{n_i}{k_i}\).

def multiChoose {d : ℕ} (n k : Fin d → ℕ) : ℕ := ∏ i, (n i).choose (k i)

Used by 1

Used byIterated backward difference of a multi-sequence

DefinitionIterated backward difference of a multi-sequence#✓fully proved

For a function \(a : \mathbb{N}^d \to \mathbb{R}\) and multi-indices \(k, n \in \mathbb{N}^d\),

\[(\Delta^k a)_n = \sum_{j \le k} (-1)^{|k| - |j|} \binom{k}{j} \, a_{n - j},\]

where \(j\) runs over the multi-indices with \(j_i \le k_i\) for every \(i\), \(|k| = \sum_i k_i\), \(\binom{k}{j} = \prod_i \binom{k_i}{j_i}\) is the multi-index binomial coefficient, and \(n - j\) is taken coordinatewise, with \(n_i - j_i\) replaced by \(0\) when \(j_i > n_i\).

When \(k \le n\) coordinatewise, \(\Delta^k\) is the composite of \(k_i\) applications of \((\Delta_i a)_n = a_{n - e_i} - a_n\) in each coordinate \(i\), where \(e_i\) is the \(i\)-th unit multi-index.

noncomputable def diff {d : ℕ} (a : (Fin d → ℕ) → ℝ) (k n : Fin d → ℕ) : ℝ :=
  ∑ j ∈ Finset.Iic k,
    (-1 : ℝ) ^ (∑ i, (k i - j i)) * (multiChoose k j : ℝ) * a (n - j)

Uses 1 · Used by 1

Statement usesMulti-index binomial coefficient

Used byHausdorff's absolute continuity criterion

DefinitionUniformly absolutely continuous measures#✓fully proved

A measure \(\mu\) on \(\mathbb{R}^d\) is uniformly absolutely continuous with respect to a measure \(\nu\) on \(\mathbb{R}^d\) if there is a real constant \(C \ge 0\) with \(\mu(S) \le C \, \nu(S)\) for every measurable set \(S\).

When \(\nu\) is \(\sigma\)-finite, this says that \(\mu\) has an essentially bounded Radon–Nikodym density with respect to \(\nu\).

def UniformlyAbsolutelyContinuous {d : ℕ}
    (μ ν : Measure (EuclideanSpace ℝ (Fin d))) : Prop :=
  ∃ C : ℝ≥0, μ ≤ C • ν

Used by 1

Used byHausdorff's absolute continuity criterion

TheoremHausdorff's absolute continuity criterion#●ready to prove

Let \(\mu\) be a probability measure on \(\mathbb{R}^d\) with \(\mu(\mathbb{R}^d \setminus I^d) = 0\), where \(I^d = [0,1]^d\) is the closed unit cube, and let \(\lambda\) be Lebesgue measure restricted to \(I^d\). For a measure \(\rho\) write \(m_\rho(n) = \int_{I^d} x^n \, d\rho(x)\) for its moments, indexed by multi-indices \(n \in \mathbb{N}^d\). Then \(\mu\) is uniformly absolutely continuous with respect to \(\lambda\) if and only if there is a real constant \(C\) such that \((\Delta^k m_\mu)_n \le C \, (\Delta^k m_\lambda)_n\) for all multi-indices \(k \le n\) (coordinatewise), where \(\Delta^k\) is the iterated backward difference.

public theorem_wanted hausdorff_absolute_continuity {d : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin d)))
    [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

Sources

• F. Hausdorff (1921–1923); see Shohat–Tamarkin, The Problem of Moments. Knill, Some fundamental theorems in mathematics, §115. Problem hausdorff_absolute_continuity of the lean-eval benchmark.

Uses 4

Statement usesUniformly absolutely continuous measures · Closed unit cube · Iterated backward difference of a multi-sequence · Moments of a measure on the unit cube

DefinitionUnit cube of the Hausdorff moment problem#✓fully proved

For \(d \in \mathbb{N}\), the closed unit cube \(I^d = [0,1]^d\) is the set of points \(x \in \mathbb{R}^d\) with \(0 \le x_i \le 1\) for every coordinate \(i\).

def cube (d : ℕ) : Set (EuclideanSpace ℝ (Fin d)) := {x | ∀ i, x i ∈ Set.Icc (0 : ℝ) 1}

Used by 1

Used byMoments on the unit cube

DefinitionMulti-index monomial#✓fully proved

For a multi-index \(n \in \mathbb{N}^d\), the monomial \(x^n\) is the real function on \(\mathbb{R}^d\) given by \(x^n = \prod_i x_i^{n_i}\).

def monomial {d : ℕ} (n : Fin d → ℕ) (x : EuclideanSpace ℝ (Fin d)) : ℝ := ∏ i, (x i) ^ (n i)

Used by 1

Used byMoments on the unit cube

DefinitionMoments on the unit cube#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^d\) and a multi-index \(n \in \mathbb{N}^d\), the \(n\)-th moment of \(\mu\) on the unit cube is the real number \(\int_{[0,1]^d} x^n \, d\mu(x)\), where \(x^n = \prod_i x_i^{n_i}\).

When \(x^n\) is not \(\mu\)-integrable on \([0,1]^d\), this integral is taken to be \(0\).

noncomputable def momentOf {d : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin d))) (n : Fin d → ℕ) : ℝ :=
  ∫ x in cube d, monomial n x ∂μ

Uses 2 · Used by 2

Statement usesUnit cube of the Hausdorff moment problem · Multi-index monomial

Used byMoment sequences of signed measures on the cube · Moment sequences of positive measures on the cube

DefinitionMoment sequences of signed measures on the cube#✓fully proved

A real sequence \(a\) indexed by \(\mathbb{N}^d\) is a moment configuration if there are finite measures \(\mu\) and \(\nu\) on \(\mathbb{R}^d\) such that for every multi-index \(n \in \mathbb{N}^d\),

\[a_n = \int_{[0,1]^d} x^n \, d\mu(x) - \int_{[0,1]^d} x^n \, d\nu(x),\]

where \(x^n = \prod_i x_i^{n_i}\).

This encodes a signed measure of bounded variation on the cube by its Jordan decomposition \(\mu - \nu\).

def IsMomentConfiguration {d : ℕ} (a : (Fin d → ℕ) → ℝ) : Prop :=
  ∃ μ ν : Measure (EuclideanSpace ℝ (Fin d)), IsFiniteMeasure μ ∧ IsFiniteMeasure ν ∧
    ∀ n, a n = momentOf μ n - momentOf ν n

Uses 1 · Used by 1

Statement usesMoments on the unit cube

Used byHausdorff–Hildebrandt–Schoenberg moment theorem

DefinitionMulti-index binomial coefficient#✓fully proved

For multi-indices \(n, k \in \mathbb{N}^d\), the binomial coefficient \(\binom{n}{k}\) is the natural number \(\prod_i \binom{n_i}{k_i}\).

def multiChoose {d : ℕ} (n k : Fin d → ℕ) : ℕ := ∏ i, (n i).choose (k i)

Used by 2

Used byIterated backward difference · Hausdorff-bounded sequences

DefinitionIterated backward difference#✓fully proved

For a real sequence \(a\) indexed by \(\mathbb{N}^d\) and multi-indices \(k, n \in \mathbb{N}^d\), the iterated backward difference of \(a\) is the real number

\[(\Delta^k a)_n = \sum_{j \le k} (-1)^{|k| - |j|} \binom{k}{j} a_{n - j},\]

where \(j\) ranges over the multi-indices with \(j \le k\) coordinatewise, \(|j| = \sum_i j_i\), \(\binom{k}{j} = \prod_i \binom{k_i}{j_i}\), and \(n - j\) is computed coordinatewise in \(\mathbb{N}\), with \(n_i - j_i = 0\) when \(j_i > n_i\).

For \(k \le n\) no truncation occurs, and \(\Delta^k a\) is the iterate of the backward partial differences \((\Delta_i a)_n = a_{n - e_i} - a_n\), applied \(k_i\) times in each coordinate \(i\), where \(e_i \in \mathbb{N}^d\) is the \(i\)-th unit multi-index.

noncomputable def diff {d : ℕ} (a : (Fin d → ℕ) → ℝ) (k n : Fin d → ℕ) : ℝ :=
  ∑ j ∈ Finset.Iic k,
    (-1 : ℝ) ^ (∑ i, (k i - j i)) * (multiChoose k j : ℝ) * a (n - j)

Uses 1 · Used by 2

Statement usesMulti-index binomial coefficient

Used byHausdorff-bounded sequences · Hausdorff positivity criterion

DefinitionHausdorff-bounded sequences#✓fully proved

A real sequence \(a\) indexed by \(\mathbb{N}^d\) is Hausdorff bounded if there is a real constant \(M\) such that for every multi-index \(n \in \mathbb{N}^d\),

\[\sum_{k \le n} \left| \binom{n}{k} (\Delta^k a)_n \right| \le M,\]

where \(k\) ranges over the multi-indices with \(k \le n\) coordinatewise, \(\binom{n}{k} = \prod_i \binom{n_i}{k_i}\) is the multi-index binomial coefficient, and \(\Delta^k a\) is the iterated backward difference of \(a\).

def HausdorffBounded {d : ℕ} (a : (Fin d → ℕ) → ℝ) : Prop :=
  ∃ C : ℝ, ∀ n : Fin d → ℕ,
    ∑ k ∈ Finset.Iic n, |(multiChoose n k : ℝ) * diff a k n| ≤ C

Uses 2 · Used by 1

Statement usesIterated backward difference · Multi-index binomial coefficient

Used byHausdorff–Hildebrandt–Schoenberg moment theorem

DefinitionMoment sequences of positive measures on the cube#✓fully proved

A real sequence \(a\) indexed by \(\mathbb{N}^d\) is a positive moment configuration if there is a finite measure \(\mu\) on \(\mathbb{R}^d\) such that \(a_n = \int_{[0,1]^d} x^n \, d\mu(x)\) for every multi-index \(n \in \mathbb{N}^d\), where \(x^n = \prod_i x_i^{n_i}\).

def IsPositiveMomentConfiguration {d : ℕ} (a : (Fin d → ℕ) → ℝ) : Prop :=
  ∃ μ : Measure (EuclideanSpace ℝ (Fin d)), IsFiniteMeasure μ ∧ ∀ n, a n = momentOf μ n

Uses 1 · Used by 1

Statement usesMoments on the unit cube

Used byHausdorff positivity criterion

TheoremHausdorff–Hildebrandt–Schoenberg moment theorem#●ready to prove

A real sequence \(a\) indexed by \(\mathbb{N}^d\) is a moment configuration, that is, there are finite measures \(\mu\) and \(\nu\) on \(\mathbb{R}^d\) with \(a_n = \int_{[0,1]^d} x^n \, d\mu(x) - \int_{[0,1]^d} x^n \, d\nu(x)\) for every multi-index \(n \in \mathbb{N}^d\), where \(x^n = \prod_i x_i^{n_i}\), if and only if \(a\) is Hausdorff bounded.

public theorem_wanted hausdorff_hildebrandt_schoenberg {d : ℕ} (a : (Fin d → ℕ) → ℝ) :
    IsMomentConfiguration a ↔ HausdorffBounded a

Sources

• F. Hausdorff (1921, 1923); T. H. Hildebrandt and I. J. Schoenberg, On linear functional operations and the moment problem for a finite interval in one or several dimensions, Ann. of Math. 34 (1933). Knill, Some fundamental theorems in mathematics, §115. Problem hausdorff_hildebrandt_schoenberg of the lean-eval benchmark.

Uses 2

Statement usesHausdorff-bounded sequences · Moment sequences of signed measures on the cube

TheoremHausdorff positivity criterion#●ready to prove

A real sequence \(a\) indexed by \(\mathbb{N}^d\) is a positive moment configuration, that is, there is a finite measure \(\mu\) on \(\mathbb{R}^d\) with \(a_n = \int_{[0,1]^d} x^n \, d\mu(x)\) for every multi-index \(n \in \mathbb{N}^d\), where \(x^n = \prod_i x_i^{n_i}\), if and only if \((\Delta^k a)_n \ge 0\) for all multi-indices \(k, n\) with \(k \le n\) coordinatewise, where \(\Delta^k a\) is the iterated backward difference of \(a\).

public theorem_wanted hausdorff_positivity {d : ℕ} (a : (Fin d → ℕ) → ℝ) :
    IsPositiveMomentConfiguration a ↔ ∀ k n : Fin d → ℕ, k ≤ n → 0 ≤ diff a k n

Sources

• F. Hausdorff, Summationsmethoden und Momentfolgen I, II, Math. Z. 9 (1921). Knill, Some fundamental theorems in mathematics, §115. Problem hausdorff_positivity_criterion of the lean-eval benchmark.

Uses 2

Statement usesMoment sequences of positive measures on the cube · Iterated backward difference

14 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.