Stieltjes densities: nonzero L2, radial asymptotics, and polynomials

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.stieltjes_basic

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d\geq1$ and let $\rho\neq0$ be a positive Borel measure on $[0,\infty)$ . Define the extended nonnegative density $\Theta(x)=\int_0^\infty(y^2+\|x\|^2)^{-1}\,d\rho(y)$ and $\nu=\Theta\,dx$ on $\mathbb R^d$ . The following are equivalent: $\Theta(x)<\infty$ for some nonzero $x$ ; it is finite at every nonzero $x$ ; $L^2(\nu)\neq\{0\}$ ; and $\int_0^\infty(1+y^2)^{-1}\,d\rho(y)<\infty$ . Under these conditions, $\rho$ is tempered and

\lim_{\|x\|\to\infty}\Theta(x)\|x\|^2=\rho([0,\infty))>0.

The limit is allowed to be infinite. There is a nonzero polynomial in $L^2(\nu)$ exactly when $d=1$ and $\nu$ is finite; every polynomial in $L^2(\nu)$ is constant. In dimension one,

\nu(\mathbb R)=\pi\int_0^\infty y^{-1}\,d\rho(y).

All reciprocals and integrals here are extended nonnegative quantities, so the reciprocal at zero is infinite.

This result identifies the nontrivial and polynomial parts of the Stieltjes-measure Hilbert model.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P92

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P92

open scoped ComplexConjugate BigOperators NNReal ENNReal

open MeasureTheory

attribute [local instance] Classical.propDecidable

universe u v

variable (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {E}

/-- Lemma A.1, PDF pp. 42--43, all equivalences and both additional clauses.
The radial limit and reciprocal at y=0 are extended nonnegative values.
The final total-mass identity is asserted only in dimension one. -/
theorem stieltjes_basic (d : ℕ) (hd : 0 < d) (rho : Measure ℝ≥0) (hRho : rho ≠ 0) :
    ((∃ x : EuclideanSpace ℝ (Fin d), x ≠ 0 ∧ stieltjesDensity d rho x < ⊤) ↔
      ∀ x : EuclideanSpace ℝ (Fin d), x ≠ 0 → stieltjesDensity d rho x < ⊤) ∧
    ((∀ x : EuclideanSpace ℝ (Fin d), x ≠ 0 → stieltjesDensity d rho x < ⊤) ↔
      Nontrivial (Lp ℂ 2 (stieltjesMeasure d rho))) ∧
    (Nontrivial (Lp ℂ 2 (stieltjesMeasure d rho)) ↔ IsTame rho) ∧
    (IsTame rho →
      IsTemperedMeasure (Measure.map (fun y : ℝ≥0 => (y : ℝ)) rho) ∧
      0 < rho Set.univ ∧
      Filter.Tendsto
        (fun x : EuclideanSpace ℝ (Fin d) =>
          stieltjesDensity d rho x * ENNReal.ofReal (‖x‖ ^ 2))
        (Filter.comap (fun x : EuclideanSpace ℝ (Fin d) => ‖x‖) Filter.atTop)
        (nhds (rho Set.univ)) ∧
      ((∃ p : MvPolynomial (Fin d) ℂ, p ≠ 0 ∧
          MemLp (polynomialValue p) 2 (stieltjesMeasure d rho)) ↔
        d = 1 ∧ stieltjesMeasure d rho Set.univ < ⊤) ∧
      (∀ p : MvPolynomial (Fin d) ℂ,
        MemLp (polynomialValue p) 2 (stieltjesMeasure d rho) →
          ∃ c : ℂ, p = MvPolynomial.C c) ∧
      (d = 1 → stieltjesMeasure d rho Set.univ =
        ENNReal.ofReal Real.pi * (∫⁻ y, (y : ℝ≥0∞)⁻¹ ∂rho))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 42, Lemma A.1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $d$ be a natural number with $d>0$ , and let $\rho$ be a nonzero measure on $[0,\infty)$ . Define

f(x)=\int_{[0,\infty)}(y^2+\|x\|^2)^{-1}\,d\rho(y), \qquad \mu(A)=\int_A f(x)\,dx

for measurable subsets $A$ of real Euclidean $d$ -space, using extended nonnegative integrals and $0^{-1}=+\infty$ . Then there exists a nonzero $x$ with $f(x)<+\infty$ if and only if every nonzero $x$ satisfies $f(x)<+\infty$ ; every nonzero $x$ satisfies this finiteness condition if and only if the complex space $L^2(\mu)$ , whose elements are square-integrable functions modulo almost-everywhere equality, has at least two distinct elements; and $L^2(\mu)$ has at least two distinct elements if and only if

\int_{[0,\infty)}(1+y^2)^{-1}\,d\rho(y)<+\infty.

If this last integral is finite, all of the following also hold: the pushforward $\nu$ of $\rho$ under the inclusion $[0,\infty)\hookrightarrow\mathbb R$ satisfies

\exists N\in\mathbb N,\qquad \int_{\mathbb R}(1+|z|^2)^{-N}\,d\nu(z)<+\infty;

the total mass obeys $0<\rho([0,\infty))$ ; and, as $\|x\|$ tends to $+\infty$ ,

f(x)\,\|x\|^2\longrightarrow\rho([0,\infty))

in the topology of the extended nonnegative reals, so the limit is allowed to be $+\infty$ . Under the same finiteness assumption, there exists a nonzero complex polynomial $p$ in $d$ variables whose evaluation on real Euclidean $d$ -space belongs to $L^2(\mu)$ if and only if $d=1$ and $\mu$ has finite total mass; every polynomial whose evaluation belongs to $L^2(\mu)$ is equal, as a polynomial, to a constant polynomial $c$ for some $c\in\mathbb C$ ; and, if $d=1$ , then

\mu(\mathbb R^d) =\pi\int_{[0,\infty)}y^{-1}\,d\rho(y).

Here polynomial evaluation embeds each real coordinate into $\mathbb C$ , and membership in $L^2$ means almost-everywhere strong measurability together with finiteness of the integral of the squared absolute value. The integer $N$ may be zero, the total masses in the assertions need not be finite unless explicitly stated, and all displayed inverses, products, and nonnegative integrals use extended nonnegative arithmetic, including $0\cdot(+\infty)=0$ . The assumptions exclude $d=0$ and $\rho=0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph