Stieltjes moment problem

TheoremCarleman's inequality, summability form#✓fully proved

If \((a_n)_{n \ge 0}\) is a summable sequence of nonnegative real numbers, then the sequence of geometric means \((a_0 a_1 \cdots a_n)^{1/(n+1)}\), \(n \ge 0\), is summable.

public theorem summable_geometric_means {a : ℕ → ℝ} (ha : ∀ n, 0 ≤ a n)
    (hasum : Summable a) :
    Summable (fun n =>
      (∏ k ∈ Finset.range (n + 1), a k) ^ (((n + 1 : ℕ) : ℝ)⁻¹))

Used by 1

Used byCarleman's criterion for the Stieltjes moment problem

DefinitionStieltjes moment determinacy#✓fully proved

A measure \(\mu\) on \(\mathbb{R}\) is Stieltjes moment determinate when every probability measure \(\nu\) on \(\mathbb{R}\) such that \(\nu((-\infty, 0)) = 0\), \(\int |x|^k \, d\nu(x) < \infty\) for every integer \(k \ge 1\), and \(\int x^k \, d\nu(x) = \int x^k \, d\mu(x)\) for every integer \(k \ge 1\) is equal to \(\mu\).

The moments of \(\mu\) are Bochner integrals, which are \(0\) when \(x^k\) is not \(\mu\)-integrable, and the definition places no condition on \(\mu\) itself.

public def StieltjesMomentDeterminate (μ : MeasureTheory.Measure ℝ) : Prop :=
  ∀ (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν],
    ν (Set.Iio (0 : ℝ)) = 0 →
    (∀ k : ℕ, 0 < k → MeasureTheory.Integrable (fun x : ℝ => |x| ^ k) ν) →
    (∀ k : ℕ, 0 < k →
      ProbabilityTheory.moment (id : ℝ → ℝ) k ν =
        ProbabilityTheory.moment (id : ℝ → ℝ) k μ) →
    ν = μ

Sources

• Gwo Dong Lin, "Recent Developments on the Moment Problem", Journal of Statistical Distributions and Applications (2017), DOI 10.1186/s40488-017-0059-2, arXiv:1703.01027v3. Definition lines 57-75, criterion lines 297-321. JIS application, lines 152-177.

Used by 1

Used byCarleman's criterion for the Stieltjes moment problem

TheoremCarleman's criterion for the Stieltjes moment problem#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with \(\mu((-\infty, 0)) = 0\) such that \(\int |x|^k \, d\mu(x) < \infty\) for every integer \(k \ge 1\), and write \(m_k = \int x^k \, d\mu(x)\). If \(\sum_{k \ge 1} m_k^{-1/(2k)} = \infty\), where the terms are taken in \([0, \infty]\) (so a term with \(m_k = 0\) equals \(\infty\)), then \(\mu\) is Stieltjes moment determinate.

Proof: Symmetrize through the square-root map, apply Denjoy--Carleman quasi-analytic uniqueness to the difference of characteristic functions, then push forward by squaring.

public theorem carleman_stieltjes_criterion
    (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ]
    (hsupp : μ (Set.Iio (0 : ℝ)) = 0)
    (hint : ∀ k : ℕ, 0 < k →
      MeasureTheory.Integrable (fun x : ℝ => |x| ^ k) μ)
    (hcarleman : tsum (fun n : ℕ =>
      ENNReal.rpow
        (ENNReal.ofReal
          (ProbabilityTheory.moment (id : ℝ → ℝ) (n + 1) μ))
        (-1 / (2 * ((n + 1 : ℕ) : ℝ)))) = ⊤) :
    StieltjesMomentDeterminate μ

Sources

• Gwo Dong Lin, "Recent Developments on the Moment Problem" (2017), Theorem 2, (s6) implies (s7). Source spans: definition lines 57-75, criterion lines 297-321; JIS application lines 152-177.

Uses 2

Statement usesStieltjes moment determinacy

Proof usesCarleman's inequality, summability form

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.