Closability is equivalent to absolute continuity

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.closable_iff_absolute_continuity

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

prove2quantum

Let $n\ge1$ , let $\mathcal S=\mathcal S(\mathbb R^n;\mathbb C)$ have its full Schwartz Fréchet topology, and write $\widehat\psi(u)=\int_{\mathbb R^n}e^{-iu\cdot x}\psi(x)\,dx$ . Let $\mathcal C$ consist of the regular positive Borel measures $\sigma$ for which $\int(1+|u|^2)^{-p}\,d\sigma(u)<\infty$ for some nonnegative integer $p$ .

For $\sigma\in\mathcal C$ , put $q_\sigma(\psi)=\int|\widehat\psi|^2\,d\sigma$ . Closability is taken in the ambient space $L^2(dx)$ : whenever $s_k\in\mathcal S$ tends to zero in $L^2(dx)$ and $q_\sigma(s_k-s_l)\to0$ as both indices tend to infinity, one has $q_\sigma(s_k)\to0$ . Then

q_\sigma\text{ is closable in }L^2(dx)\quad\Longleftrightarrow\quad\sigma\ll dx.

This keeps both implications, without assuming the existence of the source proof's auxiliary operator or kernel.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P38

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P38

open MeasureTheory Filter

open scoped Topology ComplexConjugate ENNReal

/-- Theorem 4.2, PDF pp.11--13: both directions of closability in the ambient
Lebesgue L2 space. The unfinished converse proof is not a premise. -/
theorem closable_iff_absolute_continuity (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) :
    Closable (spectralQ σ) ↔ σ ≪ (volume : Measure (SpectralDomain n)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 12, Theorem 4.2: closability iff absolute continuity

Read-back

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

For every positive integer $n$ , let $X=\mathbb R^{\operatorname{Fin}n}$ be Euclidean space, and let $\sigma$ be a regular measure on $X$ satisfying $\int_X(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , with $p=0$ allowed. For each complex-valued Schwartz function $\psi$ , define

\widehat\psi(u)=\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx, \qquad q(\psi)=\operatorname{toReal}\!\left(\int_X^{\!\!-}|\widehat\psi(u)|^2\,d\sigma(u)\right),

where the integral inside $\operatorname{toReal}$ is extended nonnegative, and $\operatorname{toReal}(+\infty)=0$ . For a function $g$ , let $[g]_{du}$ denote its $L^2$ class for Euclidean volume when it belongs to $L^2$ , and zero otherwise. Then $\sigma$ is absolutely continuous with respect to Euclidean volume if and only if the following sequence property holds: for every sequence $(s_k)_{k\in\mathbb N}$ of complex-valued Schwartz functions, if $\|[s_k]_{du}\|\to0$ and

\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall k,l\ge N,\qquad q(s_k-s_l)<\varepsilon,

then $q(s_k)\to0$ . Absolute continuity here means that every measurable set of volume zero has $\sigma$ -measure zero.

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