The convolution module property

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.convolution_module

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$ .

Let $\sigma\in\mathcal C$ . Suppose a regular positive Borel measure $\tau$ belongs to $\mathcal C_b$ : for each integer $p\ge1$ there are an integer $q\ge1$ and $C>0$ , both independent of $v\in\mathbb R^n$ , with

\int(1+|u+v|^2)^{-q}\,d\tau(u)\le C(1+|v|^2)^{-p}\qquad(\forall v\in\mathbb R^n).

Then $\sigma\star\tau\in\mathcal C$ , where convolution is the pushforward of the product measure under addition. This is the module inclusion $\mathcal C\star\mathcal C_b\subset\mathcal C$ in every positive dimension.

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 11.1, PDF pp.25--26: C is a convolution module over C_b.
In (11.1) both q and C are uniform in v; the proof's missing q is restored. -/
theorem convolution_module (n : ℕ) (hn : 0 < n)
    (σ τ : Measure (SpectralDomain n)) (hσ : InC σ) (hτ : InCb τ) :
    InC (measureConvolution σ τ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 25, Theorem 11.1: the convolution module property

Read-back

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

For every positive integer $n$ , put $X=\mathbb R^{\operatorname{Fin}n}$ , and let $\sigma,\tau$ be measures on $X$ . Assume that $\sigma$ is regular and that $\int_X(1+\|u\|^2)^{-r}\,d\sigma(u)<\infty$ for some natural number $r$ , with $r=0$ allowed. Assume also that $\tau$ is regular and that, for every natural number $p\ge1$ , there exist a natural number $q\ge1$ and a real number $C>0$ such that, for every $v\in X$ ,

\int_X^{\!\!-}(1+\|u+v\|^2)^{-q}\,d\tau(u) \le C(1+\|v\|^2)^{-p},

where the nonnegative expression on the right is viewed as an extended nonnegative real number. Define $\sigma*\tau$ as the pushforward of $\sigma\otimes\tau$ under $(u,v)\mapsto u+v$ . Then $\sigma*\tau$ is regular, and there exists a natural number $s$ , possibly zero, such that

\int_X^{\!\!-}(1+\|u\|^2)^{-s}\,d(\sigma*\tau)(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