integral_exp_modeMeasure
plain-language theorem explainer
The moment-generating function of the one-mode lattice Gaussian equals exp(v_N t²/2), with v_N the inverse discrete Hessian eigenvalue for Fourier mode k. Anyone checking the C10 cylinder-measure preflight or single-mode Gaussian statistics would cite this. The proof is a short application of Mathlib's centered Gaussian MGF identity after unfolding the mode measure.
Claim. For $k,N\in\mathbb{N}$ and $t\in\mathbb{R}$, $\int \exp(t x)\,d\mu_{k,N}(x)=\exp(v_{k,N} t^2/2)$, where $\mu_{k,N}$ is the centered Gaussian probability measure of variance $v_{k,N}=\lambda_N(k)^{-1}$ and $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ is the discrete Hessian eigenvalue of mode $k$ on the $N$-site unit circle.
background
This module is a one-mode toy preflight for panel bet C10 (a Gaussian cylinder-measure limit over a frozen quadratic energy). Scope is deliberately narrow: a single Fourier mode $k$ on the $N$-site discretization of the unit circle. It is not a path-sum or field-theoretic measure, carries no campaign flag weight, and is separate from the Test G lane.
The lattice Hessian eigenvalue is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$, with continuum counterpart $(2\pi k)^2$. The Boltzmann weight of the frozen quadratic $\tfrac12\lambda x^2$ is the centered real Gaussian of variance $v_N(k):=\lambda_N(k)^{-1}$, packaged as a nonnegative real and as the Mathlib measure gaussianReal with mean zero (the mode measure).
The identity here is the standard MGF formula for that concrete centered Gaussian, stated so later targets in the same file (characteristic function, second moment) can quote a named theorem rather than re-open Mathlib.
proof idea
Unfold the mode measure to the underlying centered gaussianReal. Invoke Mathlib's mgf_id_gaussianReal at mean $0$ and variance equal to the mode variance; congrFun evaluates the resulting function equality at the real parameter $t$. A short simp clears the mean contributions (zero_mul, zero_add) and the identity map, leaving $\exp(v t^2/2)$.
why it matters
This is TARGET 1 of the one-mode cylinder preflight: the exact moment-generating identity for the normalized mode Gaussian $\mu_N$. It belongs to the QG full-theory campaign, Phase 2b SLACK lane M, as honest Mathlib-level groundwork toward a Gaussian cylinder-measure limit over the frozen quadratic energy.
Sibling targets in the same module (characteristic function $\mathrm{charFun},\mu_N,t=\exp(-v_N t^2/2)$, and the second moment) sit on the same Gaussian package. Continuum spectral control justifying $v_N\to(2\pi k)^{-2}$ lives upstream in the discrete sine eigenvalue expansion of SpectralConvergence. No campaign flag is flipped; the file's honesty header forbids treating this as support for C10 as settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.