Dirac comb factorization and corrected periodization

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.dirac_comb_factorization

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

prove2quantum

Let $\mathcal S=\mathcal S(\mathbb R;\mathbb C)$ have its full Fréchet topology, put $\widehat\psi(u)=\int e^{-iux}\psi(x)\,dx$ , and let $\sigma=\sum_{m\in\mathbb Z}\delta_m$ . Fix a complex Hilbert isometric isomorphism $W:\ell^2(\mathbb Z)\to L^2(\mathbb R,dx)$ . The Fourier samples are square summable, $Q\psi=W((\widehat\psi(m))_m)$ is continuous complex-linear, and

\|Q\psi\|_2^2=\sum_{m\in\mathbb Z}|\widehat\psi(m)|^2=\int|\widehat\psi|^2\,d\sigma.

The adjoint product is continuous into the distribution anti-dual and satisfies, for all $\psi,\varphi\in\mathcal S$ ,

\langle Q^*Q\psi,\varphi\rangle=2\pi\int_{\mathbb R}\left(\sum_{m\in\mathbb Z}\psi(x+2\pi m)\right)\overline{\varphi(x)}\,dx.

The series converges absolutely at every $x$ , and the displayed integral is integrable. The factor $2\pi$ corrects (12.2) under the paper's stated Fourier convention; it is a disclosed source correction.

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

/-- Proposition 12.1, PDF pp.26--27. SOURCE CORRECTION: under the paper's
unnormalized Fourier convention, (12.2) must read Q*Q=2π times periodization.
The printed W must be isometric, as (12.1) and its proof require. All continuity
is Schwartz Fréchet continuity; no Lebesgue-L2 boundedness is asserted.
The anti-dual formulation is the distributional equality, not pointwise evaluation. -/
theorem dirac_comb_factorization
    (W : SequenceL2 ≃ₗᵢ[ℂ] L2 (volume : Measure (SpectralDomain 1))) :
    ∃ Q : ComplexTest 1 →L[ℂ] L2 (volume : Measure (SpectralDomain 1)),
      ∃ A : ComplexTest 1 →L[ℂ] AntiDual 1,
        (∀ ψ, Q ψ = W (l2Class Measure.count (combSamples ψ))) ∧
        (∀ ψ, MemLp (combSamples ψ) 2 Measure.count ∧
          fourierEnergy diracComb ψ = ENNReal.ofReal (‖Q ψ‖ ^ 2) ∧
          ∀ x, Summable (fun m : ℤ => ψ (x + point1 (2 * Real.pi * (m : ℝ))))) ∧
        (∀ ψ, A ψ = adjointProduct Q ψ ∧ ∀ φ : ComplexTest 1,
          Integrable (fun x => periodization ψ x * conj (φ x)) volume ∧
          A ψ φ = (2 * Real.pi : ℂ) *
            ∫ x, periodization ψ x * conj (φ x)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 26, Proposition 12.1: Dirac comb factorization and periodization

Read-back

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

Let $X=\mathbb R^{\operatorname{Fin}1}$ with Euclidean volume $dx$ , write $\iota(a)\in X$ for the vector whose sole coordinate is $a\in\mathbb R$ , and let $\mathcal S_{\mathbb C}(X)$ be the complex-valued Schwartz space. For every surjective complex-linear isometry $W:\ell^2(\mathbb Z;\mathbb C)\to L^2(X,dx;\mathbb C)$ , where $\ell^2$ uses counting measure, there exist continuous complex-linear maps

Q:\mathcal S_{\mathbb C}(X)\to L^2(X,dx;\mathbb C), \qquad A:\mathcal S_{\mathbb C}(X)\to\mathcal S_{\mathbb C}(X)^\times,

where $\mathcal S_{\mathbb C}(X)^\times$ is the space of continuous conjugate-linear functionals, with the following properties. Define

\widehat\psi(u)=\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx,\qquad b_\psi(m)=\widehat\psi(\iota(m)),\qquad \sigma_{\mathrm{comb}}=\sum_{m\in\mathbb Z}\delta_{\iota(m)}, \qquad P_\psi(x)=\sum_{m\in\mathbb Z}\psi\bigl(x+\iota(2\pi m)\bigr).

For every $\psi\in\mathcal S_{\mathbb C}(X)$ , $Q\psi=W([b_\psi])$ , where $[b_\psi]$ is its counting-measure $L^2$ class if it belongs to $L^2$ , and zero otherwise; in fact, $b_\psi$ belongs to $L^2$ , and

\int_X^{\!\!-}|\widehat\psi(u)|^2\,d\sigma_{\mathrm{comb}}(u) =\operatorname{ofReal}(\|Q\psi\|^2).

For every such $\psi$ and every $x\in X$ , the series defining $P_\psi(x)$ is summable. Finally, for every $\psi$ , $A\psi$ is the functional $\phi\mapsto\langle Q\phi,Q\psi\rangle_{\mathbb C}$ , and for every $\phi\in\mathcal S_{\mathbb C}(X)$ , the function $x\mapsto P_\psi(x)\overline{\phi(x)}$ is integrable with respect to volume and

(A\psi)(\phi)=2\pi\int_X P_\psi(x)\,\overline{\phi(x)}\,dx.

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