Temperedness of a rotation-invariant Stieltjes measure

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.stieltjes_temperedness

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

prove2quantum

Let $d\geq1$ and let $\rho$ be a positive Borel measure on $[0,\infty)$ satisfying $\int_0^\infty(1+y^2)^{-1}\,d\rho(y)<\infty$ . Define $\Theta(x)=\int_0^\infty(y^2+\|x\|^2)^{-1}\,d\rho(y)$ and $\nu=\Theta\,dx$ on $\mathbb R^d$ . Then

\nu\text{ is tempered}\quad\Longleftrightarrow\quad d>2\;\text{ or }\;\left[d=1,\ \int_{[0,1]}y^{-1}\,d\rho(y)<\infty\right]\;\text{ or }\;\left[d=2,\ \int_{[0,1]}\log(y^{-1})\,d\rho(y)<\infty\right].

If $\nu$ is tempered and $d=1$ or $d=2$ , then $\rho(\{0\})=0$ . The reciprocal and logarithm at zero are infinite. Temperedness means finiteness of some polynomially weighted nonnegative integral.

This separates tail control, provided by tameness, from the dimension-dependent singularity at zero. The zero measure is allowed.

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}

/-- Proposition A.3, PDF pp. 43--44. Tameness alone does not imply absence of
an atom at zero; that conclusion is conditional on temperedness in d=1 or d=2. -/
theorem stieltjes_temperedness (d : ℕ) (hd : 0 < d) (rho : Measure ℝ≥0)
    (hTame : IsTame rho) :
    (IsTemperedMeasure (stieltjesMeasure d rho) ↔
      2 < d ∨
      (d = 1 ∧ (∫⁻ y in Set.Icc (0 : ℝ≥0) 1, (y : ℝ≥0∞)⁻¹ ∂rho) < ⊤) ∨
      (d = 2 ∧ (∫⁻ y in Set.Icc (0 : ℝ≥0) 1, logReciprocal y ∂rho) < ⊤)) ∧
    (IsTemperedMeasure (stieltjesMeasure d rho) → (d = 1 ∨ d = 2) → rho {0} = 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 43, Proposition A.3

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 any measure on $[0,\infty)$ satisfying

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

Let $\mu$ be the measure on real Euclidean $d$ -space obtained from Lebesgue measure with density

f(x)=\int_{[0,\infty)}(y^2+\|x\|^2)^{-1}\,d\rho(y).

Then the condition

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

is equivalent to the following disjunction:

d>2 \quad\lor\quad \left(d=1\ \land\ \int_{[0,1]}y^{-1}\,d\rho(y)<+\infty\right) \quad\lor\quad \left(d=2\ \land\ \int_{[0,1]}\ell(y)\,d\rho(y)<+\infty\right),

where $\ell(0)=+\infty$ and $\ell(y)=\max\{\log(1/y),0\}$ for $y>0$ . Moreover, if the displayed condition on $\mu$ holds and $d=1$ or $d=2$ , then $\rho(\{0\})=0$ . Both restricted integrals include the endpoints $0$ and $1$ ; all nonnegative integrals and inverses use extended nonnegative arithmetic, in particular $0^{-1}=+\infty$ . The exponent $N$ may be zero, and the hypotheses allow $\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