The spectral measure class is not closed under self-convolution

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.convolution_nonclosure

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

prove2quantum

On $\mathbb R$ , let $\lambda$ be ordinary Lebesgue measure. For positive measures, define $\sigma\star\tau$ as the pushforward of $\sigma\times\tau$ under addition, allowing extended masses. Let $\mathcal C$ be the regular positive Borel measures with $\int(1+u^2)^{-p}\,d\sigma(u)<\infty$ for some nonnegative integer $p$ . Then

\lambda\in\mathcal C,\qquad\lambda\star\lambda\notin\mathcal C.

Thus $\mathcal C$ is not stable under self-convolution. The extended convolution measure exists; it is not locally finite and has infinite weighted mass, rather than being nonexistent as claimed in the source's stronger rhetoric.

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

/-- §11, PDF p.25: Lebesgue measure belongs to C, but its self-convolution does not.
The pushforward still exists as an extended measure, contrary to the source's
stronger “not a well defined Borel measure” rhetoric. -/
theorem convolution_nonclosure :
    InC (volume : Measure (SpectralDomain 1)) ∧
      ¬ InC (measureConvolution (volume : Measure (SpectralDomain 1)) volume) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 25, §11, unnumbered: C is not closed under self-convolution

Read-back

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

Let $X=\mathbb R^{\operatorname{Fin}1}$ with its Euclidean structure, let $\lambda$ be Euclidean volume on $X$ , and define $\lambda*\lambda$ to be the pushforward of the product measure $\lambda\otimes\lambda$ under $(u,v)\mapsto u+v$ . Then $\lambda$ is regular and there exists a natural number $p$ , possibly zero, such that

\int_X(1+\|u\|^2)^{-p}\,d\lambda(u)<\infty.

At the same time, it is false that $\lambda*\lambda$ is regular and has such a finite weighted integral for some natural number: equivalently, either $\lambda*\lambda$ is not regular or

\forall p\in\mathbb N,\qquad \int_X^{\!\!-}(1+\|u\|^2)^{-p}\,d(\lambda*\lambda)(u)=+\infty.

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