gaussian-field

A Lean 4 / Mathlib library for constructing centered Gaussian probability measures on duals of nuclear Fréchet spaces.

Given a nuclear Fréchet space and a continuous linear map (CLM) to a separable real Hilbert space (finite- or infinite-dimensional), the library constructs a probability measure on the weak dual satisfying the characteristic functional identity:

The covariance is .

Motivation

This construction is the standard path to Gaussian measures in quantum field theory, stochastic PDEs, and infinite-dimensional probability. The library is application-agnostic — it works for any nuclear Fréchet space and any CLM into any separable Hilbert space.

Example: Gaussian Free Field

For the free scalar field in dimensions, take:

• (Schwartz space, a nuclear Fréchet space)
• (inverse half-Laplacian on Schwartz space)

The resulting measure is the Gaussian free field with mass , and the covariance is:

Gel'fand Triple Structure

The construction realizes a rigged Hilbert space (Gel'fand triple):

where is the Cameron-Martin space — the completion of under the inner product (formalized as cameronMartinInner T). The support theorem (support_of_hilbertSchmidt) characterizes where the measure lives: if is Hilbert-Schmidt (IsHilbertSchmidt T), then is supported on configurations with finite basis norm ().

This triple is the functional-analytic core of:

• Constructive QFT: the Osterwalder-Schrader and Wightman frameworks, where is the Euclidean path integral measure
• Stochastic PDEs: where provides the law of Gaussian driving noise
• Infinite-dimensional probability: where generalizes finite-dimensional Gaussian distributions

API

Input

The user provides:

• A nuclear Fréchet space E with [DyninMityaginSpace E] instance
• A separable real Hilbert space H (with standard Mathlib instances)
• A CLM T : E →L[ℝ] H

Output

Definition / Theorem	Type	Description
measure T	Measure (Configuration E)	The Gaussian measure (with IsProbabilityMeasure instance)
covariance T f g	ℝ
charFun T f	integral identity
pairing_is_gaussian	measure equality	Pushforward by is
measure_centered	integral = 0
second_moment_eq_covariance	integral identity
cross_moment_eq_covariance	integral identity
pairing_integrable	Integrable	is integrable
pairing_memLp	MemLp	for all finite (Fernique-type)
pairing_product_integrable	Integrable	is integrable
measure_isGaussian	IsGaussian (measure T)	Mathlib's IsGaussian typeclass instance
gaussian_ibp_general	integral identity
wick_recursive	integral identity	Recursive Wick formula for -point functions
wick_bound	norm bound
odd_moment_vanish	integral = 0	Odd moments vanish: when is odd
cameronMartinInner T f g	ℝ	Cameron-Martin inner product
cameronMartinNormSq T f	ℝ	Cameron-Martin norm squared
IsHilbertSchmidt T	Prop	(Hilbert-Schmidt condition)
support_of_hilbertSchmidt	∀ᵐ	HS a.e. finite basis norm
weighted_support	∀ᵐ	Weighted-HS a.e. finite weighted basis norm
expected_norm_sq_eq_hs	integral identity	$\mathbb{E}[\sum_n
gaussian_measure_unique_of_covariance	measure equality	Two centered Gaussian probability measures with the same covariance are equal (conditional on the Cramér-Wold axiom cramerWold)

Design notes

The API takes only T as an explicit argument — no proof of infinite-dimensionality is required. When H is finite-dimensional, the construction embeds H isometrically into and builds the measure there, yielding a degenerate (finite-rank) Gaussian. This allows testing with toy cases like .

Configuration E is defined as WeakDual ℝ E — the space of continuous linear functionals on with the weak-* topology. Elements are "configurations" or "generalized functions" that pair with test functions: .

End-to-end workflow: from spaces to measures

See docs/workflow.md for the full three-layer workflow (test function spaces, covariance operators, measure construction) with Lean code examples for Schwartz space, circles, lattices, tensor products, heat kernels, and the lattice-continuum limit.

Module structure

The project has three libraries, with imports flowing left to right: Nuclear <- SchwartzNuclear <- GaussianField.

1. Nuclear Space Infrastructure

The DyninMityaginSpace typeclass and the canonical model RapidDecaySeq (the Kothe sequence space ), shared by both SchwartzNuclear/ and GaussianField/.

File	Lines	Contents
DyninMityagin.lean	76	DyninMityaginSpace typeclass (Dynin-Mityagin), expansion_H lemma
NuclearSpace.lean	487	NuclearSpace typeclass (Pietsch), Hahn-Banach for seminorms, hasSum_basis (strong Schauder convergence), DM -> Pietsch
NuclearTensorProduct.lean	1,125	RapidDecaySeq, NuclearTensorProduct, pure, universal property (lift, lift_pure)

Two definitions of nuclearity

The library contains two characterizations of nuclear spaces:

1. Dynin-Mityagin (DyninMityaginSpace in DyninMityagin.lean) — A nuclear Fréchet space with a countable Schauder basis admitting polynomial growth of seminorms and super-polynomial decay of coefficients. This is the operational definition used by the Gaussian measure construction. See docs/dynin-mityagin-typeclass.md for the full typeclass definition, design decisions, how to provide an instance for a new space, which spaces are nuclear, and target instances.

2. Pietsch (NuclearSpace in NuclearSpace.lean) — For every continuous seminorm , there exists a dominating seminorm such that the canonical map is nuclear (expressible as with and ). This is the standard textbook definition (Pietsch, Grothendieck).

The Dynin-Mityagin characterization is strictly stronger: it additionally requires the existence of a Schauder basis. The implication DyninMityaginSpace.toNuclearSpace (DM -> Pietsch) is proved in NuclearSpace.lean. The converse holds for nuclear Fréchet spaces that already possess a Schauder basis (the Dynin-Mityagin theorem), but is not formalized since our applications (Schwartz spaces) obtain the DM structure directly from the Hermite basis.

Tensor products of nuclear spaces

NuclearTensorProduct E₁ E₂ is the completed nuclear tensor product of two DyninMityaginSpace spaces. It carries a DyninMityaginSpace instance (hence is itself nuclear) and satisfies the universal property: every seminorm-bounded bilinear map factors uniquely through the canonical embedding.

Structural results:

Definition / Theorem	Type	Description
NuclearTensorProduct.assoc	(E₁ ⊗̂ E₂) ⊗̂ E₃ ≃L[ℝ] E₁ ⊗̂ (E₂ ⊗̂ E₃)	Associativity
lift B	E₁ ⊗̂ E₂ →L[ℝ] G	Universal property: factors bilinear maps through pure
lift_pure	lift B (pure e₁ e₂) = B e₁ e₂	Factoring identity

Schwartz space isomorphisms (in SchwartzNuclear/SchwartzTensorProduct.lean):

Definition / Theorem	Type	Description
schwartzPeelOff d	S(ℝ^{d+2}) ≃L S(ℝ^{d+1}) ⊗̂ S(ℝ)	Peel off one dimension
schwartzTensorEquiv m n	S(ℝ^{m+1}) ⊗̂ S(ℝ^{n+1}) ≃L S(ℝ^{m+n+2})	General tensor-product isomorphism
schwartzPeelOff_pure	canonicity	Inverse sends f ⊗ g to pointwise product

These isomorphisms identify the tensor product of Schwartz spaces on lower-dimensional Euclidean spaces with Schwartz space on the product space — the Schwartz kernel theorem.

For the concrete construction (Cantor pairing, pure, lift, reindexing), see docs/tensor-products.md. For the roadmap to connect to Mathlib's abstract TensorProduct, see docs/abstract-tensor-product-plan.md.

2. Schwartz Space Nuclearity

Proves DyninMityaginSpace (SchwartzMap D ℝ) for any finite-dimensional via the Hermite function expansion and the Dynin-Mityagin isomorphism .

The Hermite-polynomial side of this development also provides the Wick polynomial algebra used downstream by the Gaussian field construction:

• wickMonomial n c x — the Wick-ordered monomial defined by the three-term recursion (x · :x^{n+1}:_c - (n+1)·c · :x^n:_c = :x^{n+2}:_c).
• wick_eq_hermiteR — Wick monomials are scaled probabilist's Hermite polynomials.
• wickMonomial_homogeneity — :γx^n:_{γ²c} = γ^n · :x^n:_c (rescaling).
• wickMonomial_add_add — bivariate Wick addition (binomial form): for two independent variables with their own variances, :x+y^n:_{c₁+c₂} = ∑_k C(n,k) · :x^k:_{c₁} · :y^{n-k}:_{c₂}.
• wickMonomial_pow_sum_expansion — multivariate Wick multinomial expansion over a Fintype index set: :∑γⱼξⱼ^k:_{∑γⱼ²} = ∑_{|α|=k} (k!/∏α!) · (∏γⱼ^{αⱼ}) · ∏ⱼ :ξⱼ^{αⱼ}:_1. This is the textbook polynomial identity (Janson §3.4, Glimm-Jaffe §6.1) that underlies the eigenbasis expansion of site Wick monomials in the lattice GFF. Proof: bivariate addition by Nat.twoStepInduction + Pascal + choose-absorption, then iteration over the index set via Finset.induction_on + homogeneity. No external axioms beyond [propext, Classical.choice, Quot.sound].

File	Lines	Contents
HermiteFunctions.lean	1,853	1D Hermite functions, orthonormality, completeness
SchwartzHermiteExpansion.lean	1,446	1D Schwartz-Hermite expansion, coefficient decay
Basis1D.lean	157	1D DyninMityaginSpace fields assembly
ParametricCalculus.lean	316	Differentiation under the integral sign
SchwartzSlicing.lean	1,134	Multi-d slicing and partial Hermite coefficients
HermiteTensorProduct.lean	2,742	Multi-d isomorphism SchwartzMap D ℝ ≃L[ℝ] RapidDecaySeq
HermiteNuclear.lean	63	DyninMityaginSpace instance from the isomorphism
SchwartzTensorProduct.lean	427	Tensor product associativity, schwartzPeelOff, schwartzTensorEquiv
HermiteWick.lean	963	Wick monomial recursion, scaled Hermite identification, bivariate Wick addition, multivariate Wick multinomial expansion
WickOrthogonality.lean	365	Stein's lemma (Gaussian IBP), 1D Wick mean-zero (wickMonomial_mean_zero)

2b. Circle Analysis

Proves DyninMityaginSpace (SmoothMap_Circle L ℝ) (sorry-free) for smooth L-periodic functions on the circle via the real Fourier basis and the isomorphism SmoothMap_Circle L ℝ ≃L[ℝ] RapidDecaySeq. Also provides the circle Laplacian as a CLM, proves its eigenvalue equation on the Fourier basis, and defines the heat semigroup spectrally.

File	Lines	Contents
SmoothCircle/Basic.lean	845	Type, seminorms, Fourier basis, orthogonality, coefficients
SmoothCircle/Nuclear.lean	824	IBP decay, CLE, Fourier completeness, DyninMityaginSpace instance
SmoothCircle/Eigenvalues.lean	50	HasLaplacianEigenvalues instance: eigenvalues
SmoothCircle/Laplacian.lean	226	circleLaplacian CLM , eigenvalue equation on Fourier basis
SmoothCircle/HeatSemigroup.lean	195	circleHeatSemigroup , spectral action, semigroup properties
SmoothCircle/Restriction.lean	139	circleRestriction CLM: sample at lattice points with normalization
Test.lean	358	End-to-end tests: Gaussian measures on S(ℝ), S(ℝᵈ), C∞(S¹), cylinder, torus, QFT covariance

Circle Laplacian and heat semigroup:

• derivSCCLM L — the derivative as a CLM on SmoothMap_Circle L ℝ
• circleLaplacian L — defined as
• circleLaplacian_fourierBasis — eigenvalue equation:
• circleHeatSemigroup L ht — defined spectrally via conjugation through the Fourier equivalence
• circleHeatSemigroup_fourierBasis — spectral action:
• circleHeatSemigroup_zero — identity:

This enables Gaussian fields on the torus T¹ = ℝ/Lℤ and (via tensor products) on cylinders S¹×ℝ and higher tori Tᵈ. The test file verifies the full pipeline for SmoothMap_Circle L ℝ, the cylinder NuclearTensorProduct (SmoothMap_Circle L ℝ) (SchwartzMap ℝ ℝ), and the torus NuclearTensorProduct (SmoothMap_Circle L₁ ℝ) (SmoothMap_Circle L₂ ℝ). See concrete instances for the mathematical details.

Design note: SmoothMap_Circle L ℝ represents smooth L-periodic functions as {f : ℝ → ℝ | Periodic f L ∧ ContDiff ℝ ⊤ f}, avoiding manifold machinery. The codomain parameter ℝ is currently a phantom type (the construction only works for real-valued functions), but is included for forward compatibility with vector-valued generalizations. Mathlib's AddCircle L (= ) has rich Fourier analysis but currently lacks ChartedSpace/SmoothManifoldWithCorners instances, so ContMDiffMap (AddCircle L) F cannot yet be defined. Once Mathlib gains manifold structure on AddCircle, the type could be refactored to ContMDiffMap (AddCircle L) F with a genuine codomain parameter.

2c. Heat Kernel Toolkit

Spectral multiplier CLMs and QFT eigenvalue/singular value definitions for constructing covariance operators on product spaces.

File	Lines	Contents
HeatKernel/Axioms.lean	264	spectralCLM, qftEigenvalue, qftSingularValue, boundedness
HeatKernel/Bilinear.lean	410	Heat kernel bilinear form K_t, Green's function G_mass, L² convergence, positivity
HeatKernel/PositionKernel.lean	2,183	Position-space heat kernels: Mehler kernel, circle heat kernel (off main build path; future proof target)

spectralCLM σ hσ : E →L[ℝ] ℓ² maps f ↦ (σ_m · coeff_m(f))_m for any bounded multiplier sequence σ. This is the key tool for constructing covariance operators: the GFF covariance on S¹_L × ℝ uses spectralCLM with σ_m = λ_m^{-1/2} where λ_m = (2πn/L)² + (2k+1) + m².

2d. Lattice Field Theory

Lattice site types, discrete Laplacian, lattice Gaussian measures, and the FKG inequality. Used by pphi2 for the Glimm-Jaffe/Nelson construction.

FinLatticeSites d N is defined as Fin d → ZMod N, using Mathlib's canonical quotient ring ZMod N for the discrete torus (ℤ/Nℤ)^d. This enables embedding into the continuous torus (ℝ/pℤ)^d via ZMod.toAddCircle, multi-scale refinement via ZMod.castHom, and interoperability with AddCircle-based lattice frameworks (Tanimoto).

File	Contents
Lattice/Sites.lean	FinLatticeSites d N := Fin d → ZMod N, InfLatticeSites d, latticeNorm, neighbors
Lattice/TorusEmbedding.lean	ContinuousTorus d p, siteToTorus : FinLatticeSites d N →+ ContinuousTorus d p (with Yoh Tanimoto)
Lattice/FiniteField.lean	FinLatticeField d N, DyninMityaginSpace and HasPointEval instances
Lattice/RapidDecayLattice.lean	RapidDecayLattice d (rapidly decaying functions on ℤ^d), seminorms, topology
Lattice/Laplacian.lean	finiteLaplacian, infiniteLaplacian, massOperator, eigenvalue formulas
Lattice/SpectralCovariance.lean	Mass operator spectral decomposition, spectralLatticeCovariance CLM, gaussianDensity
Lattice/HeatKernel.lean	Heat kernel K_t = exp(-t·(-Δ)), semigroup, symmetry, commutation
Lattice/Symmetry.lean	Translation/reflection operators, Toeplitz property, Laplacian/heat kernel commutation
Lattice/Covariance.lean	latticeCovariance via spectral theorem, latticeGaussianMeasure
GaussianField/Density.lean	Density bridge: Gaussian measure ↔ Gaussian density
Lattice/AsymCovariance.lean	Heterogeneous (Nt ≠ Ns) isotropic lattice AsymLatticeField Nt Ns := (ZMod Nt × ZMod Ns) → ℝ: massOperatorAsym, latticeCovarianceAsymGJ (GJ cell-area normalisation), asym spectral/DFT data
Lattice/AsymFiniteField.lean	DyninMityaginSpace (AsymLatticeField Nt Ns) instance (asym analogue of FiniteField.lean; delta basis, point-eval coefficients)
GaussianField/DensityAsym.lean	Asym density bridge: evalMapAsym (weak-dual ↔ coordinate equiv) and latticeGaussianFieldLawAsym_eq_normalizedQuadraticGaussianMeasure — the free asym GFF, in coordinates, is the Lebesgue-density Gaussian with precision a²·massOperatorAsym (heterogeneous analogue of Density.lean)
Lattice/FKG.lean	FKG inequality for lattice Gaussian and convexly-perturbed measures
Lattice/CirculantDFT.lean	DFT eigenbasis, spectral expansion, 1D heat kernel convergence
Lattice/HeatKernelConvergence1d.lean	Eigenvalue/DFT coefficient convergence, Riemann sum convergence
Lattice/Convergence.lean	Green's function convergence (lattice → continuum)

2e. Point Evaluation and API

File	Lines	Contents
Nuclear/PointEval.lean	66	HasPointEval typeclass + instances
GaussianFieldAPI.lean	90	Re-export file for downstream QFT projects

HasPointEval E M abstracts pointwise evaluation across test function spaces. GaussianFieldAPI.lean collects the public API (Configuration, measure, charFun, moments, spectralCLM) for downstream consumers.

2f. Cylinder (Osterwalder-Schrader Axioms) — WIP

Work in progress. This module has axioms and sorries. It is NOT part of the default build target (lake build builds only the axiom-free core). Build with lake build Cylinder or lake build All.

Test function space and symmetry infrastructure for the cylinder , the natural geometry for the Osterwalder-Schrader axioms. The spatial direction is compact (circle of circumference ) while the temporal direction is the full real line, giving a clean positive-time half-space with no wraparound issues.

File	Lines	Contents
Cylinder/Basic.lean	75	CylinderTestFunction L , Configuration axioms
Cylinder/Symmetry.lean	320	Reflection, translation (Schwartz-level and cylinder-level), configuration-level actions, 1D positive-time Schwartz submodule, eval CLM, closedness
Cylinder/PositiveTime.lean	231	cylinderPositiveTimeSubmodule, cylinderNegativeTimeSubmodule, Θ maps P+ into N−, disjointness of Θf from P+, spatial translation preserves P+
Cylinder/GreenFunction.lean	240	cylinderMassOperator via spectralCLM, cylinderGreen , bilinearity, symmetry, positivity, invariance

Key definitions:

• CylinderTestFunction L — nuclear tensor product , inherits DyninMityaginSpace
• cylinderTimeReflection L — where
• cylinderPositiveTimeSubmodule L — closure of span of with
• cylinderMassOperator L mass hmass — via spectralCLM with QFT singular values
• cylinderGreen L mass hmass — Green's function

Proved results:

Theorem	Statement
cylinderTimeReflection_pos_to_neg	maps P+ into N−
cylinderPositiveTime_disjoint_reflected	for nonzero
cylinderPositiveTime_spatialTranslation_closed	Spatial translation preserves P+
cylinderGreen_bilinear
cylinderGreen_symm
cylinderGreen_nonneg
cylinderGreen_continuous_diag	is continuous

3. Gaussian Field Construction

Given [DyninMityaginSpace E] and T : E →L[ℝ] H, constructs the centered Gaussian probability measure on .

File	Lines	Contents
SpectralTheorem.lean	468	Compact self-adjoint spectral theorem
NuclearSVD.lean	640	SVD for nuclear operators
NuclearFactorization.lean	190	Source-indexed nuclear representation
TargetFactorization.lean	324	Target-indexed factorization with ONB
Construction.lean	715	Main construction + characteristic functional
Properties.lean	193	Gaussianity, moments, integrability
IsGaussian.lean	160	Mathlib IsGaussian instance for measure T
Wick.lean	1,067	Wick's theorem: Gaussian IBP, recursive Wick formula, moment bounds
Support.lean	274	Hilbert-Schmidt condition, Cameron-Martin defs, support theorem
Hypercontractive.lean	441	Gaussian moments, Gross log-Sobolev inequality
HypercontractiveNat.lean	329	Nelson's hypercontractive estimate for even integer p via double-factorial combinatorics
Symmetry.lean	250	Measure-level symmetries: covariance-preserving CLM action ⇒ measure invariance. Includes measure_neg_invariant and the lattice instance latticeGaussianFieldLaw_isNegInvariant.
StandardGaussianBridge.lean	513	Lattice GFF as pushforward of the standard multivariate Gaussian: orthogonalised coordinates ξ_k(ω) = ω(e_k) · √(a^d λ_k) are i.i.d. N(0,1) (gffOrthonormalCoord_normal/_independent), pushforward equality Π_k gaussianReal 0 1 (gffOrthonormalProj_pushforward_eq_stdGaussian), characteristic-functional form (gffOrthonormalProj_charFun)
WickMultivariate.lean	593	Multivariate Wick monomials in the orthogonalised GFF coordinates: gffMultiWickMonomial_eq_hermite_product, gffMultiWickMonomial_orthogonality (∫ :ξ^α: · :ξ^β: dμ_GFF = δ_{αβ} · ∏ α_j!), and the eigenbasis expansion siteWickMonomial_eigenbasis_expansion of the site Wick monomial :φ(x)^k:_{c_a(x)}

Dependency graph

Nuclear/
  DyninMityagin → NuclearTensorProduct → PointEval
       ↓                ↓
SchwartzNuclear/   SmoothCircle/                       GaussianField/
  ...              Basic → Nuclear → Eigenvalues    NuclearFactorization
                          ↓    ↓          ↓
                   Restriction  Laplacian → HeatSemigroup
  HermiteNuclear        ↓                     ↓
       ↓           Test (uses GF)   SpectralTheorem → NuclearSVD → TargetFactorization
  SchwartzTensorProduct                                                ↓
       ↓                                                               ↓
       └──────────────→ GaussianField.lean ←─────────────────── Construction
                              ↓                                        ↓
                       HeatKernel/                                 Properties
                     Axioms, PositionKernel                          ↓     ↓
                              ↓                                IsGaussian  Wick
                       GaussianFieldAPI.lean (re-exports for downstream)

Cylinder/ (OS axiom infrastructure)
  Basic ← Symmetry ← PositiveTime
                   ← GreenFunction
  (imports SmoothCircle/Nuclear, SchwartzNuclear, Nuclear/TensorProductFunctorAxioms)

Downstream projects

This library provides the concrete functional analysis infrastructure for:

• pphi2 — Formal construction of the P(Φ)₂ interacting Euclidean QFT via the Glimm-Jaffe/Nelson lattice approach. Uses the Lattice module (lattice Gaussian measure, FKG inequality, discrete Laplacian) and the core Gaussian field API.

• OSreconstruction — Osterwalder-Schrader reconstruction theorem and Wightman axioms. gaussian-field's extension branch proves two axioms used in Wightman/WightmanAxioms.lean:

  • schwartz_nuclear_extension — the Schwartz kernel theorem (proved in GeneralResults/NuclearExtensionComplex.lean)
  • exists_continuousMultilinear_ofSeparatelyContinuous — Banach-Steinhaus for separately continuous multilinear maps (proved in GeneralResults/SeparatelyContMultilinear.lean)

• QFTFramework — Abstract QFT axiomatics (SpacetimeData, QFTData, OSTheory). gaussian-field's types fill QFTFramework's abstract slots.

• GFF — Bridges gaussian-field and QFTFramework to formalize the Gaussian free field on cylinders (S¹_L × ℝ), tori (T²), and flat ℝ^d, with Osterwalder-Schrader axiom verification.

• OSforGFF — OS axiom verification for the Gaussian free field. Imports gaussian-field's main branch for DyninMityaginSpace (SchwartzMap D ℝ) (Schwartz space nuclearity via Hermite expansion) and the Gaussian measure construction.

Proof status

The core results are fully proved with no custom axioms:

• DyninMityaginSpace (SchwartzMap D ℝ) — sorry-free (~8,100 lines via Hermite expansion)
• DyninMityaginSpace (SmoothMap_Circle L ℝ) — sorry-free (~1,670 lines via Fourier basis)
• DyninMityaginSpace.toNuclearSpace — sorry-free (Dynin-Mityagin implies Pietsch)
• GaussianField.measure, charFun, moments — sorry-free
• gaussian_ibp_general, wick_recursive, wick_bound, odd_moment_vanish — sorry-free

The hypercontractive and log-Sobolev development is fully theorem-backed (GaussianField/HypercontractiveNat.lean, GaussianField/Hypercontractive.lean) with no remaining axioms or sorries in that path.

The lattice/FKG pipeline is theorem-backed end-to-end: continuous Ahlswede-Daykin (including ENNReal bridge and n-dimensional induction), lattice Gaussian FKG, perturbation/truncation lemmas, and the density bridge in GaussianField/Density.lean are proved. The heterogeneous (Nt ≠ Ns) density bridge GaussianField/DensityAsym.lean (latticeGaussianFieldLawAsym_eq_normalizedQuadraticGaussianMeasure) is likewise proved sorry-free and axiom-clean.

The standard-Gaussian bridge and multivariate Wick algebra are theorem-backed end-to-end (GaussianField/StandardGaussianBridge.lean, GaussianField/WickMultivariate.lean, SchwartzNuclear/HermiteWick.lean). All seven of the original bridge/Wick claims — orthogonalised-coordinate normality (gffOrthonormalCoord_normal), independence (_independent), pushforward to the standard pi-Gaussian (gffOrthonormalProj_pushforward_eq_stdGaussian), characteristic-functional form (gffOrthonormalProj_charFun), Wick-monomial / Hermite identification (gffMultiWickMonomial_eq_hermite_product), Wick orthogonality (gffMultiWickMonomial_orthogonality: ∫ :ξ^α: · :ξ^β: dμ_GFF = δ_{αβ} · ∏ α_j!), and the eigenbasis expansion of the site Wick monomial (siteWickMonomial_eigenbasis_expansion) — are now proved theorems with no custom axioms. The bivariate and multivariate Wick multinomial identities (wickMonomial_add_add, wickMonomial_pow_sum_expansion) are proved generically over an arbitrary Fintype index set in SchwartzNuclear/HermiteWick.lean and could be upstreamed to Mathlib.

The 1D lattice-continuum convergence pipeline is fully proved: DFT eigenbasis construction, spectral expansion of the heat kernel, eigenvalue convergence, DFT coefficient convergence via Riemann sums, and the full heat kernel bilinear form convergence theorem (lattice_heatKernel_tendsto_continuum_1d in Lattice/CirculantDFT.lean).

Green's function invariance (reflection, translation) on pure tensors and the bilinear extension are proved in HeatKernel/GreenInvariance.lean. Fourier translation/reflection axioms in SmoothCircle/FourierTranslation.lean are fully proved.

Default build target (lake build): 0 axioms, 0 sorries.

This includes: Nuclear/, SchwartzNuclear/, SmoothCircle/, GaussianField/, Lattice/, HeatKernel/, Torus/, GeneralResults/.

WIP modules (not in default build, build with lake build Cylinder or lake build All):

Module	Axioms	Sorries	Notes
Cylinder/	3	0	OS axiom infrastructure, proof plan
SchwartzFourier/	1	0	Hörmander multiplier theorem (general, Mathlib-ready)

Former axioms have been proved or moved to future/ as documentation:

• future/gaussian_field_axioms.lean — measure uniqueness, converse support, support Hilbert space
• future/configuration_torus.lean — Polish/Borel instances for Configuration(Torus)
• future/mehler_kernel.lean — Mehler's formula eigenfunction expansion

Further documentation

• DyninMityaginSpace typeclass — typeclass definition, design decisions, how to construct instances, which spaces are nuclear
• Workflow — end-to-end three-layer workflow with Lean code examples
• Nuclear space infrastructure — the NuclearSpace and DyninMityaginSpace typeclasses, RapidDecaySeq, and why nuclearity is needed
• Schwartz nuclearity proof — the 7,700-line proof that Schwartz space is nuclear
• Gaussian field construction — the 2,960-line measure construction
• Wick's theorem — Gaussian IBP, recursive Wick formula, moment bounds, and OS1' growth estimate
• Concrete instances — DyninMityaginSpace instances for , finite lattices, periodic lattices, and generic tensor products, with Lean sketches
• Operator construction — building covariance operators on product spaces via the heat kernel , Mathlib support, and the factorization theorem
• Lattice-continuum limit — convergence of lattice Gaussian measures to continuum measures via characteristic functionals
• Generalization plan — architecture of the DyninMityaginSpace typeclass, design decisions, and roadmap for future instances
• Tensor products — concrete construction of NuclearTensorProduct via RapidDecaySeq and Cantor pairing, pure/lift API, reindexing, and Schwartz tensor product isomorphisms
• Abstract tensor product plan — roadmap for building completed projective tensor products on Mathlib's TensorProduct, proving isomorphism with RapidDecaySeq, and the nuclear coincidence theorem

4. Schwartz Nuclear Extension Theorem (extension branch)

Proves the Schwartz kernel theorem: every continuous ℂ-multilinear functional on extends uniquely to a continuous ℂ-linear functional on , agreeing on product tensors. This replaces the schwartz_nuclear_extension axiom in OSreconstruction.

0 sorrys. 0 axioms. Fully proved in ~2,500 lines across 4 files.

File	Lines	Contents
GeneralResults/SchwartzProducts.lean	632	Product of Schwartz functions is Schwartz (schwartzProductTensor_schwartz), product Hermite density (productHermite_schwartz_dense), product-aware CLE (productRapidDecayEquiv)
GeneralResults/NuclearExtensionComplex.lean	1,357	Complex product tensor, complexification, schwartz_nuclear_extension theorem
SchwartzNuclear/NuclearExtension.lean	445	DyninMityaginSpace extension theorem (exists_unique_clm_of_polyBounded), multilinear basis bounds
SchwartzNuclear/TsumBound.lean	41	Tsum bound helper

Key results:

Theorem	Description
schwartz_nuclear_extension	, agreeing with on product tensors
exists_unique_clm_of_polyBounded	DyninMityaginSpace: CLM from polynomially-bounded basis values
multilinear_on_basis_bound	$
schwartzProductTensor_schwartz	Product of Schwartz functions is Schwartz
productHermite_schwartz_dense	Product Hermite functions span a dense subspace of
productBasisIndices_polyGrowth	Per-factor basis indices grow polynomially in the flat index

Proof architecture:

• Uniqueness: Product Hermite density (productHermite_schwartz_dense) via product-aware CLE, then complexification
• Existence: Restrict to real inputs → extract Re/Im parts → multilinear_on_basis_bound gives polynomial growth → exists_unique_clm_of_polyBounded constructs → complexify → prove agreement by induction on free arguments using DyninMityaginSpace.expansion in each slot

Future work

• New instances: is fully proved; remaining targets: for compact , half-spaces (see concrete instances)
• Vector-valued generalization: Generalize SmoothMap_Circle L ℝ and SchwartzMap D ℝ to vector-valued codomains (the F parameter in SmoothMap_Circle is a placeholder for this), with nuclearity via ; long-term, refactor to ContMDiffMap (AddCircle L) F once Mathlib gains manifold structure on AddCircle
• Abstract tensor product: Build completed projective tensor products on Mathlib's algebraic TensorProduct, prove isomorphism with RapidDecaySeq for DM spaces, and the nuclear coincidence theorem (see abstract tensor product plan)
• Besov regularity: The support theorem (support_of_hilbertSchmidt) shows a.s. finite basis norm when is HS. The next step is showing -a.s. for appropriate Besov indices
• -algebra coincidence: For separable nuclear Fréchet spaces, the cylindrical and Borel -algebras on the dual coincide (see future/configuration_torus.lean)

Building

lake update
lake build
lake build Test  # end-to-end tests: Gaussian measures on S(ℝ), S(ℝᵈ), C∞(S¹), cylinder, torus

Requires Lean 4 v4.28.0 and Mathlib (fetched automatically by Lake).

Authors

Michael R. Douglas, with contributions from Yoh Tanimoto (torus embedding framework)

License

Apache 2.0

References

• I.M. Gel'fand and N.Ya. Vilenkin, Generalized Functions, Vol. 4 (1964)
• B. Simon, The P(φ)₂ Euclidean (Quantum) Field Theory (1974)
• J. Glimm and A. Jaffe, Quantum Physics: A Functional Integral Point of View (1987)
• S. Thangavelu, Lectures on Hermite and Laguerre Expansions (1993)
• A. Dynin, B. Mityagin, "Criterion for nuclearity in terms of approximative dimension" (1960)