# Concrete `DyninMityaginSpace` Instances ## Overview This document specifies concrete `DyninMityaginSpace` instances for spaces arising in QFT and stochastic analysis, and the generic tensor product construction that composes them. Each instance is parameterized by geometric data (circumference, lattice spacing, etc.). The current library provides one instance: `SchwartzMap D F` via Hermite basis axioms. The instances below extend this to circles, lattices, and their products. --- ## 1. The circle $S^1_L$ of circumference $L$ ### Mathematical setup Fix circumference $L > 0$. The test function space is $$E = C^\infty(S^1_L) = C^\infty(\mathbb{R}/L\mathbb{Z})$$ with the Fréchet topology generated by the Sobolev seminorms $$p_k(f) = \left(\sum_{n \in \mathbb{Z}} (1 + |n|)^{2k} |\hat{f}_n|^2\right)^{1/2}$$ where $\hat{f}_n = \frac{1}{L} \int_0^L f(x) e^{-2\pi i n x / L} dx$ are the Fourier coefficients. The dual space $E' = \mathcal{D}'(S^1_L)$ consists of periodic distributions. ### Basis and coefficients - **Basis:** Fourier modes, reindexed to $\mathbb{N}$ via a bijection $\sigma : \mathbb{N} \to \mathbb{Z}$ (e.g., $0, 1, -1, 2, -2, \ldots$): $$\psi_m(x) = \frac{1}{\sqrt{L}} e^{2\pi i \sigma(m) x / L}$$ (For a real-valued formulation, use $\cos$ and $\sin$ modes instead.) - **Coefficients:** $c_m(f) = \sqrt{L}\, \hat{f}_{\sigma(m)}$ ### Growth and decay - **Growth:** $p_k(\psi_m) = (1 + |\sigma(m)|)^k \le (1 + m)^k$ (polynomial, with $C = 1$, $s = k$) - **Decay:** $|c_m(f)| \cdot (1 + m)^k \le C \cdot p_{k+1}(f)$ (super-polynomial, controlled by one higher Sobolev norm) ### Lean sketch ```lean /-- Smooth periodic functions on the circle of circumference L. Uses Mathlib's AddCircle L = ℝ/Lℤ as the domain. -/ structure SmoothMap_Circle (L : ℝ) (F : Type*) [hL : Fact (0 < L)] := -- Placeholder: Mathlib does not yet have C^∞(AddCircle L) as a Fréchet space. -- Would be defined as smooth maps AddCircle L → ℝ with Fréchet topology. sorry variable (L : ℝ) [hL : Fact (0 < L)] /-- Fourier modes on S^1_L, reindexed by ℕ. -/ axiom fourierBasis (L : ℝ) [Fact (0 < L)] : ℕ → SmoothMap_Circle L ℝ /-- Fourier coefficient CLMs. -/ axiom fourierCoeff (L : ℝ) [Fact (0 < L)] : ℕ → (SmoothMap_Circle L ℝ →L[ℝ] ℝ) /-- Sobolev seminorms on S^1_L, indexed by ℕ. -/ axiom sobolevSeminorm (L : ℝ) [Fact (0 < L)] : ℕ → Seminorm ℝ (SmoothMap_Circle L ℝ) axiom smoothCircle_withSeminorms (L : ℝ) [Fact (0 < L)] : WithSeminorms (sobolevSeminorm L) axiom fourier_expansion (L : ℝ) [Fact (0 < L)] (φ : SmoothMap_Circle L ℝ →L[ℝ] ℝ) (f : SmoothMap_Circle L ℝ) : φ f = ∑' m, (fourierCoeff L m f) * φ (fourierBasis L m) axiom fourier_seminorm_growth (L : ℝ) [Fact (0 < L)] (k : ℕ) : ∃ C > 0, ∃ (s : ℕ), ∀ m : ℕ, sobolevSeminorm L k (fourierBasis L m) ≤ C * (1 + (m : ℝ)) ^ s axiom fourier_coefficient_decay (L : ℝ) [Fact (0 < L)] (k : ℕ) : ∃ C > 0, ∃ (q : ℕ), ∀ (f : SmoothMap_Circle L ℝ) (m : ℕ), |fourierCoeff L m f| * (1 + (m : ℝ)) ^ k ≤ C * sobolevSeminorm L q f instance smoothCircle_dyninMityaginSpace : DyninMityaginSpace (SmoothMap_Circle L ℝ) where ι := ℕ p := sobolevSeminorm L h_with := smoothCircle_withSeminorms L basis := fourierBasis L coeff := fourierCoeff L expansion := fourier_expansion L basis_growth := fourier_seminorm_growth L coeff_decay := fourier_coefficient_decay L ``` ### Usage ```lean -- Gaussian free field on S^1 of circumference L variable (L : ℝ) [Fact (0 < L)] (m : ℝ) variable (T : SmoothMap_Circle L ℝ →L[ℝ] H) -- e.g., (-d²/dx² + m²)^{-1/2} #check GaussianField.measure T -- Measure (Configuration (SmoothMap_Circle L ℝ)) ``` The circumference $L$ propagates through the construction: it determines the Fourier mode spacing $2\pi/L$, the eigenvalues $(2\pi n/L)^2$, and ultimately the covariance kernel. --- ## 2. Finite lattice in $\mathbb{R}$ with spacing $a$ ### Mathematical setup Fix lattice spacing $a > 0$ and number of sites $N$. The lattice is $$\Lambda_{a,N} = \{0, a, 2a, \ldots, (N-1)a\}$$ The test function space is $E = \Lambda_{a,N} \to \mathbb{R} \cong \mathbb{R}^N$, finite-dimensional and trivially nuclear. The dual space $E' \cong \mathbb{R}^N$ (self-dual). A "lattice distribution" is just a vector of values at the lattice sites. ### Basis and coefficients - **Basis:** standard basis vectors $e_k \in \mathbb{R}^N$, $e_k(ja) = \delta_{jk}$ - **Coefficients:** $c_k(f) = f(ka)$ (evaluation at site $k$) ### Growth and decay Trivial: all sums are finite (at most $N$ nonzero terms), so growth and decay conditions are automatically satisfied. Any bound works because we can take $C$ large enough to dominate the finite maximum. ### Lean sketch ```lean /-- Finite lattice with N sites and spacing a. The spacing a is a parameter of the operators, not the DyninMityaginSpace instance — the underlying vector space is just Fin N → ℝ regardless of a. -/ abbrev FiniteLattice (N : ℕ) := Fin N → ℝ variable (N : ℕ) [NeZero N] instance finiteLattice_dyninMityaginSpace : DyninMityaginSpace (FiniteLattice N) where ι := Unit p := fun _ => sorry -- sup norm or ℓ² norm; any single norm suffices h_with := sorry -- finite-dimensional topology = norm topology basis := fun m => if h : m < N then Pi.single ⟨m, h⟩ 1 else 0 coeff := fun m => if h : m < N then -- evaluation at site m ContinuousLinearMap.proj ⟨m, h⟩ else 0 expansion := by -- finite sum, straightforward intro φ f; simp; sorry basis_growth := by -- trivial: finitely many basis elements intro _; exact ⟨1, one_pos, 0, fun m => by simp; sorry⟩ coeff_decay := by -- trivial: finitely many nonzero coefficients intro k; exact ⟨1, one_pos, (), fun f m => by simp; sorry⟩ ``` ### Usage The lattice spacing $a$ enters through the operators, not the space: ```lean variable (a : ℝ) [Fact (0 < a)] (N : ℕ) [NeZero N] /-- Discrete Laplacian with spacing a and Dirichlet BC. -/ def discreteLaplacian (a : ℝ) (N : ℕ) : FiniteLattice N →L[ℝ] FiniteLattice N := sorry -- (Δf)(k) = (f(k+1) - 2f(k) + f(k-1)) / a² /-- Covariance operator for the lattice GFF. -/ def latticeGFF_T (a : ℝ) (N : ℕ) (mass : ℝ) : FiniteLattice N →L[ℝ] FiniteLattice N := sorry -- (-Δ_a + m²)^{-1/2} -- The lattice Gaussian measure #check GaussianField.measure (latticeGFF_T a N mass) -- : Measure (Configuration (FiniteLattice N)) ``` ### Design note The `DyninMityaginSpace` instance for `Fin N → ℝ` does not depend on $a$ — all finite-dimensional spaces of the same dimension are isomorphic as nuclear spaces. The spacing $a$ determines the CLM $T$ and therefore the specific Gaussian measure (its covariance structure), not the topology of the test function space. --- ## 2b. Infinite lattice $\mathbb{Z}^d$: rapidly decaying sequences ### Why $\ell^2(\mathbb{Z}^d)$ doesn't work A theorem of Grothendieck: an infinite-dimensional Banach space is never nuclear. Since $\ell^2(\mathbb{Z}^d)$ is an infinite-dimensional Hilbert space, it cannot carry a `DyninMityaginSpace` instance. The same applies to any fixed Sobolev space $\ell^2_s(\mathbb{Z}^d)$. Nuclearity requires the topology to be strictly weaker than any single norm. It needs a *family* of seminorms with specific decay properties between them. ### The nuclear alternative: $s(\mathbb{Z}^d)$ The discrete analogue of Schwartz space is the space of **rapidly decaying sequences**: $$s(\mathbb{Z}^d) = \left\{ f : \mathbb{Z}^d \to \mathbb{R} \;\middle|\; \forall k \in \mathbb{N},\, \sum_{n \in \mathbb{Z}^d} |f(n)|^2 (1+|n|)^{2k} < \infty \right\}$$ This is a nuclear Fréchet space, topologized by the weighted $\ell^2$ seminorms: $$p_k(f) = \left(\sum_{n \in \mathbb{Z}^d} |f(n)|^2 (1+|n|)^{2k}\right)^{1/2}$$ Its dual $s'(\mathbb{Z}^d)$ consists of sequences of at most polynomial growth — the discrete tempered distributions. The Gel'fand triple is: $$s(\mathbb{Z}^d) \subset \ell^2(\mathbb{Z}^d) \subset s'(\mathbb{Z}^d)$$ ### Basis and coefficients This is the simplest infinite-dimensional instance because the basis and coefficients are trivial: - **Basis:** standard delta functions $e_n$, reindexed via a bijection $\sigma : \mathbb{N} \to \mathbb{Z}^d$ - **Coefficients:** point evaluations $c_n(f) = f(n)$ - **Growth:** $p_k(e_n) = (1 + |n|)^k$ — polynomial - **Decay:** $|f(n)| \cdot (1+|n|)^k \le p_k(f)$ — immediate from the seminorm definition (Cauchy-Schwarz on a single term) No axioms needed. All proofs are elementary. ### Lean sketch ```lean /-- Rapidly decaying sequences on ℤ^d — the discrete Schwartz space. -/ structure RapidDecaySeq (d : ℕ) where val : (Fin d → ℤ) → ℝ rapid : ∀ k : ℕ, Summable fun n => |val n| ^ 2 * (1 + ‖(n : Fin d → ℤ)‖) ^ (2 * k) -- Reindex ℤ^d to ℕ via some computable bijection def enumZd (d : ℕ) : ℕ ≃ (Fin d → ℤ) := sorry instance rapidDecaySeq_dyninMityaginSpace : DyninMityaginSpace (RapidDecaySeq d) where ι := ℕ -- weight parameter k p := fun k => sorry -- p_k(f) = (Σ |f(n)|² (1+|n|)^{2k})^{1/2} h_with := sorry -- topology = seminorm topology basis := fun m => let n := (enumZd d) m ⟨fun n' => if n' = n then 1 else 0, sorry⟩ coeff := fun m => let n := (enumZd d) m sorry -- CLM: f ↦ f.val n expansion := by sorry -- f = Σ_n f(n) · e_n (straightforward) basis_growth := by -- p_k(e_n) = (1+|n|)^k intro k; exact ⟨1, one_pos, k, fun m => by sorry⟩ coeff_decay := by -- |f(n)| · (1+|n|)^k ≤ p_k(f) (Cauchy-Schwarz) intro k; exact ⟨1, one_pos, k, fun f m => by sorry⟩ ``` ### Relation to finite lattices For lattice QFT, the standard approach is: 1. Work on a **finite** lattice $(\mathbb{Z}/N\mathbb{Z})^d$ — trivially nuclear, all computations are linear algebra 2. Take the **infinite-volume limit** $N \to \infty$ — the limiting space is $s(\mathbb{Z}^d)$ (or $C^\infty$ on a torus in the periodic case) The finite lattice instance (Section 2) handles step 1. Step 2 is a convergence statement analogous to the lattice-continuum limit in [lattice-continuum-limit.md](lattice-continuum-limit.md). --- ## 3. Finite lattice on $S^1_L$ with spacing $a = L/N$ ### Mathematical setup Fix circumference $L > 0$ and number of sites $N$, giving lattice spacing $a = L/N$. The lattice is $$\Lambda_{L,N} = \{0, L/N, 2L/N, \ldots, (N-1)L/N\} \subset S^1_L$$ with **periodic boundary conditions**: site $N$ is identified with site $0$. The test function space is $E = \Lambda_{L,N} \to \mathbb{R} \cong \mathbb{R}^N$, identical as a vector space to the interval lattice but with different operators reflecting the periodicity. ### Basis and coefficients Two natural choices: **Standard basis** (same as interval lattice): - $e_k(j) = \delta_{jk}$, $c_k(f) = f(kL/N)$ **Discrete Fourier basis** (respects periodicity): - $\psi_n(j) = \frac{1}{\sqrt{N}} e^{2\pi i n j / N}$, $n = 0, \ldots, N-1$ - $c_n(f) = \frac{1}{\sqrt{N}} \sum_j f(j) e^{-2\pi i n j / N}$ (DFT) Either works for the `DyninMityaginSpace` instance (finite-dimensional, so the choice is immaterial for nuclearity). The DFT basis diagonalizes the discrete Laplacian, which is useful for explicit covariance computations. ### Lean sketch ```lean /-- Finite periodic lattice: N sites on a circle of circumference L. As a vector space, identical to FiniteLattice N. The periodicity enters through the operators. -/ abbrev PeriodicLattice (N : ℕ) := Fin N → ℝ -- DyninMityaginSpace instance is identical to FiniteLattice instance periodicLattice_dyninMityaginSpace : DyninMityaginSpace (PeriodicLattice N) := finiteLattice_dyninMityaginSpace N /-- Discrete periodic Laplacian on N sites with spacing L/N. (Δf)(k) = N²/L² · (f(k+1 mod N) - 2f(k) + f(k-1 mod N)) -/ def discretePeriodicLaplacian (L : ℝ) (N : ℕ) : PeriodicLattice N →L[ℝ] PeriodicLattice N := sorry /-- Lattice GFF on the periodic lattice (discrete circle). -/ def periodicLatticeGFF_T (L : ℝ) (N : ℕ) (mass : ℝ) : PeriodicLattice N →L[ℝ] PeriodicLattice N := sorry -- (-Δ_{L,N} + m²)^{-1/2} -- The lattice Gaussian measure on the discrete circle variable (L : ℝ) [Fact (0 < L)] (N : ℕ) [NeZero N] (mass : ℝ) #check GaussianField.measure (periodicLatticeGFF_T L N mass) ``` ### Continuum limit As $N \to \infty$ (equivalently $a = L/N \to 0$), the lattice GFF on $\Lambda_{L,N}$ should converge to the continuum GFF on $S^1_L$. The restriction map $r_N : C^\infty(S^1_L) \to (\text{Fin } N \to \mathbb{R})$ samples a smooth function at the $N$ lattice points: $$r_N(f)(k) = \sqrt{L/N} \cdot f(kL/N)$$ (The $\sqrt{L/N}$ factor ensures the correct scaling of the $L^2$ inner product: $\sum_k |r_N(f)(k)|^2 \cdot 1 \approx \int_0^L |f(x)|^2 dx$.) The convergence theorem (see [lattice-continuum-limit.md](lattice-continuum-limit.md)) reduces to: $$\|T_N(r_N f)\|^2 \to \|T(f)\|^2 \qquad \forall f \in C^\infty(S^1_L)$$ which is a standard approximation result for the discrete Laplacian. --- ## 4. Generic tensor product `NuclearTensorProduct` ### Mathematical setup Given nuclear Fréchet spaces $E_1$ and $E_2$ with Schauder bases $\{\psi_i\}$ and $\{\varphi_j\}$, the completed projective tensor product $E_1 \hat{\otimes} E_2$ is again a nuclear Fréchet space with: - **Basis:** $\{\psi_i \otimes \varphi_j\}_{(i,j) \in \mathbb{N}^2}$ - **Seminorms:** product seminorms $r_{(\alpha,\beta)} = p_\alpha \otimes q_\beta$ - **Coefficients:** $c_{(i,j)}(f_1 \otimes f_2) = c^1_i(f_1) \cdot c^2_j(f_2)$ ### The Cantor pairing The typeclass requires basis indexed by $\mathbb{N}$, so we use Mathlib's `Nat.pair : ℕ → ℕ → ℕ` (the Cantor pairing function) and its inverse `Nat.unpair : ℕ → ℕ × ℕ`. Key property for growth bounds: if $\text{unpair}(m) = (i, j)$ then $i \le m$ and $j \le m$, so $(1+i)(1+j) \le (1+m)^2$. ### Growth and decay for the product **Growth.** Suppose $p_\alpha(\psi_i) \le C_1 (1+i)^{s_1}$ and $q_\beta(\varphi_j) \le C_2 (1+j)^{s_2}$. Then for $m$ with $\text{unpair}(m) = (i,j)$: $$r_{(\alpha,\beta)}(\psi_i \otimes \varphi_j) = p_\alpha(\psi_i) \cdot q_\beta(\varphi_j) \le C_1 C_2 (1+i)^{s_1} (1+j)^{s_2} \le C_1 C_2 (1+m)^{s_1 + s_2}$$ Still polynomial. **Decay.** Suppose $|c^1_i(f_1)| (1+i)^k \le C_1 p_{\alpha}(f_1)$ and $|c^2_j(f_2)| (1+j)^k \le C_2 q_{\beta}(f_2)$. Then for $f = f_1 \otimes f_2$: $$|c_{(i,j)}(f)| (1+m)^k \le |c^1_i(f_1)| \cdot |c^2_j(f_2)| \cdot (1+m)^k$$ Since $m \ge \max(i,j)$, we can split $(1+m)^k \le (1+i)^k (1+j)^k$ (up to a constant from the Cantor pairing), giving: $$\le C_1 C_2 \cdot p_\alpha(f_1) \cdot q_\beta(f_2) = C_1 C_2 \cdot r_{(\alpha,\beta)}(f)$$ Still super-polynomial decay controlled by a product seminorm. ### Lean sketch ```lean namespace GaussianField /-- Cantor pairing utilities. -/ private def pair : ℕ × ℕ → ℕ := fun ⟨i, j⟩ => Nat.pair i j private def unpair : ℕ → ℕ × ℕ := Nat.unpair /-- The nuclear Fréchet tensor product of two nuclear Fréchet spaces. Defined concretely as a subspace of functions ℕ × ℕ → ℝ with appropriate decay, carrying the product Fréchet topology. Mathematically: E₁ ⊗̂_π E₂ (completed projective tensor product). By nuclearity, this equals the completed injective tensor product E₁ ⊗̂_ε E₂ as well. -/ structure NuclearTensorProduct (E₁ : Type*) [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [DyninMityaginSpace E₁] (E₂ : Type*) [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₂] where /-- The sequence of coefficients in the product basis. -/ coeff_seq : ℕ × ℕ → ℝ /-- Rapid decay in the product seminorms. -/ rapid_decay : ∀ (α : DyninMityaginSpace.ι (E := E₁)) (β : DyninMityaginSpace.ι (E := E₂)) (k : ℕ), Summable fun ⟨i, j⟩ => |coeff_seq (i, j)| * DyninMityaginSpace.p α (DyninMityaginSpace.basis i) * DyninMityaginSpace.p β (DyninMityaginSpace.basis j) * (1 + (i : ℝ))^k * (1 + (j : ℝ))^k -- Instances: AddCommGroup, Module ℝ, TopologicalSpace, etc. -- (Inherited from the Köthe sequence space structure.) instance [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : AddCommGroup (NuclearTensorProduct E₁ E₂) := sorry instance [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : Module ℝ (NuclearTensorProduct E₁ E₂) := sorry instance [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : TopologicalSpace (NuclearTensorProduct E₁ E₂) := sorry instance [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : IsTopologicalAddGroup (NuclearTensorProduct E₁ E₂) := sorry instance [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : ContinuousSMul ℝ (NuclearTensorProduct E₁ E₂) := sorry /-- The tensor product of two nuclear Fréchet spaces is nuclear. Basis: ψ_i ⊗ φ_j via Cantor pairing. Seminorms: products of factor seminorms. Growth/decay: products of factor bounds. -/ instance nuclearTensorProduct_dyninMityaginSpace [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : DyninMityaginSpace (NuclearTensorProduct E₁ E₂) where ι := DyninMityaginSpace.ι (E := E₁) × DyninMityaginSpace.ι (E := E₂) p := fun ⟨α, β⟩ => sorry -- product seminorm: r_{α,β}(f) = ... h_with := sorry -- product topology = product seminorm topology basis := fun m => let (i, j) := Nat.unpair m sorry -- ψ_i ⊗ φ_j as element of NuclearTensorProduct coeff := fun m => let (i, j) := Nat.unpair m sorry -- c^1_i ⊗ c^2_j as a CLM expansion := by -- Factor the scalar CLF through the two factors -- and apply expansion in each factor sorry basis_growth := by -- Product of factor growth bounds: -- r_{α,β}(ψ_i ⊗ φ_j) = p_α(ψ_i) · q_β(φ_j) -- ≤ C₁(1+i)^s₁ · C₂(1+j)^s₂ ≤ C₁C₂(1+m)^{s₁+s₂} sorry coeff_decay := by -- Product of factor decay bounds: -- |c_{i,j}(f)|(1+m)^k ≤ C₁C₂ · r_{α,β}(f) sorry /-- Pure tensor: the canonical bilinear map E₁ × E₂ → E₁ ⊗̂ E₂. -/ def NuclearTensorProduct.pure [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (f₁ : E₁) (f₂ : E₂) : NuclearTensorProduct E₁ E₂ where coeff_seq := fun ⟨i, j⟩ => DyninMityaginSpace.coeff i f₁ * DyninMityaginSpace.coeff j f₂ rapid_decay := sorry end GaussianField ``` ### Usage: measures on product spaces ```lean -- Gaussian measure on distributions on the cylinder S¹_L × ℝ variable (L : ℝ) [Fact (0 < L)] abbrev Cylinder (L : ℝ) [Fact (0 < L)] := NuclearTensorProduct (SmoothMap_Circle L ℝ) (SchwartzMap (EuclideanSpace ℝ (Fin 1)) ℝ) variable (T : Cylinder L →L[ℝ] H) #check GaussianField.measure T -- : Measure (Configuration (Cylinder L)) -- Gaussian measure on distributions on the torus T²_{L₁,L₂} variable (L₁ L₂ : ℝ) [Fact (0 < L₁)] [Fact (0 < L₂)] abbrev Torus2 (L₁ L₂ : ℝ) [Fact (0 < L₁)] [Fact (0 < L₂)] := NuclearTensorProduct (SmoothMap_Circle L ℝ₁) (SmoothMap_Circle L ℝ₂) variable (T₂ : Torus2 L₁ L₂ →L[ℝ] H) #check GaussianField.measure T₂ -- : Measure (Configuration (Torus2 L₁ L₂)) ``` ### Lattice tensor products Tensor products of finite lattices are again finite lattices: ```lean -- Lattice on S¹_L × S¹_L (2D periodic lattice) -- PeriodicLattice N₁ ⊗ PeriodicLattice N₂ ≅ Fin (N₁ * N₂) → ℝ -- But can also just use: abbrev Lattice2D (N₁ N₂ : ℕ) := Fin N₁ × Fin N₂ → ℝ instance : DyninMityaginSpace (Lattice2D N₁ N₂) := sorry -- finite-dim -- Lattice GFF on 2D periodic lattice def lattice2D_GFF (L₁ L₂ : ℝ) (N₁ N₂ : ℕ) (mass : ℝ) : Lattice2D N₁ N₂ →L[ℝ] Lattice2D N₁ N₂ := sorry -- (-Δ₁ - Δ₂ + m²)^{-1/2} with spacings L₁/N₁, L₂/N₂ ``` --- ## 5. Continuum limits for product spaces ### Circle: $\Lambda_{L,N} \to S^1_L$ ```lean /-- Restriction: sample a smooth function on S¹_L at N equally spaced points. -/ def circleRestriction (L : ℝ) [Fact (0 < L)] (N : ℕ) [NeZero N] : SmoothMap_Circle L ℝ →L[ℝ] PeriodicLattice N := sorry -- r_N(f)(k) = √(L/N) · f(kL/N) /-- Convergence of lattice GFF to continuum GFF on S¹_L. -/ theorem circle_continuum_limit (L : ℝ) [Fact (0 < L)] (mass : ℝ) (T : SmoothMap_Circle L ℝ →L[ℝ] H) -- continuum operator (T_N : ∀ N : ℕ, PeriodicLattice N →L[ℝ] H_N) -- lattice operators (h_conv : ∀ f : SmoothMap_Circle L ℝ, Filter.Tendsto (fun N => ‖T_N N (circleRestriction L N f)‖ ^ 2) Filter.atTop (nhds (‖T f‖ ^ 2))) : sorry -- weak convergence of pushed-forward lattice measures to μ := sorry ``` ### Torus: $\Lambda_{L_1,N_1} \times \Lambda_{L_2,N_2} \to T^2_{L_1,L_2}$ The restriction map factors as a tensor product: $$r_{N_1,N_2} = r_{N_1} \otimes r_{N_2} : C^\infty(S^1_{L_1}) \hat{\otimes} C^\infty(S^1_{L_2}) \to (\text{Fin } N_1 \to \mathbb{R}) \otimes (\text{Fin } N_2 \to \mathbb{R})$$ The quadratic form convergence likewise factors: $$\|T_{N_1,N_2}(r_{N_1,N_2} f)\|^2 \to \|T(f)\|^2$$ For product operators ($T = T_1 \otimes T_2$), this reduces to convergence in each factor separately. --- ## Which spaces are nuclear? Not every function space is nuclear. A theorem of Grothendieck: an infinite-dimensional Banach (or Hilbert) space is never nuclear. | Space | Nuclear? | Reason | |---|---|---| | $C^\infty(S^1_L)$ | **Yes** | Projective limit of Sobolev spaces | | $\mathcal{S}(\mathbb{R}^d)$ | **Yes** | Projective limit of weighted Sobolev spaces | | $s(\mathbb{Z}^d)$ (rapidly decaying) | **Yes** | Projective limit of weighted $\ell^2$ | | $\mathbb{R}^N$ (finite lattice) | **Yes** | Finite-dimensional | | $H^k(S^1_L)$ for fixed $k$ | **No** | Infinite-dimensional Hilbert space | | $\ell^2(\mathbb{Z}^d)$ | **No** | Infinite-dimensional Hilbert space | | $L^2(\mathbb{R}^d)$ | **No** | Infinite-dimensional Hilbert space | The pattern: $C^\infty = \bigcap_k H^k$ is nuclear (intersection of all Sobolev levels), but any individual $H^k$ is not. Similarly $s(\mathbb{Z}^d) = \bigcap_k \ell^2_k(\mathbb{Z}^d)$ is nuclear, but any individual $\ell^2_k$ is not. The Gaussian measure lives on the dual — distributions $\mathcal{D}' = \bigcup_k H^{-k}$ or polynomially growing sequences $s' = \bigcup_k \ell^2_{-k}$. ## Summary table | Space | `E` in Lean | `ι` | Basis | Axioms needed | |---|---|---|---|---| | $\mathcal{S}(\mathbb{R}^d)$ | `SchwartzMap D F` | `ℕ × ℕ` | Hermite | 5 (current) | | $C^\infty(S^1_L)$ | `SmoothMap_Circle L ℝ` | `ℕ` | Fourier | 0 (fully proved) | | $s(\mathbb{Z}^d)$ | `RapidDecaySeq d` | `ℕ` | Standard $e_n$ | 0 (elementary) | | Finite lattice | `FiniteLattice N` | `Unit` | Standard | 0 (trivial) | | Periodic lattice on $S^1_L$ | `PeriodicLattice N` | `Unit` | Standard/DFT | 0 (trivial) | | $E_1 \hat{\otimes} E_2$ | `NuclearTensorProduct E₁ E₂` | `ι₁ × ι₂` | Product | From factors | | $T^2_{L_1,L_2}$ | `Torus2 L₁ L₂` | `ℕ × ℕ` | Fourier² | From circle | | Cylinder $S^1_L \times \mathbb{R}$ | `Cylinder L` | `ℕ × (ℕ × ℕ)` | Fourier × Hermite | From factors |