# `Density.lean` -- Informal Summary

> **Source**: [`GaussianField/Density.lean`](../../GaussianField/Density.lean)
> **Generated**: 2026-03-03 11:30
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Proves that the lattice Gaussian measure (constructed via pushforward of noise) has density $\rho(\varphi) = \exp(-\tfrac{1}{2}\langle\varphi, Q\varphi\rangle)$ with respect to Lebesgue measure, up to normalization. The "density bridge" connects the abstract Gaussian field construction with the explicit density formula needed for the FKG inequality proof. The proof matches characteristic functions: both the pushforward measure and the normalized density measure have the same Fourier transform (computed via diagonalization in the mass eigenbasis), hence are equal by `Measure.ext_of_charFunDual`.

## Status

**Main result**: Fully proven

None -- file is sorry-free.

**Length**: 1053 lines, 14 definition(s) + 22 theorem(s)/lemma(s)

---

## Textbook Finite-Dimensional Gaussian

### [`quadraticGaussianDensity`](../../GaussianField/Density.lean#L57) -- Definition

**Lean signature**
```lean
def quadraticGaussianDensity
    (Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) (φ : ι → ℝ) : ℝ
```
**Informal**: The unnormalized Gaussian density $\rho(\varphi) = \exp\bigl(-\tfrac{1}{2}\sum_x \varphi(x)\,(Q\varphi)(x)\bigr)$.

---

### [`quadraticGaussianMeasure`](../../GaussianField/Density.lean#L62) -- Definition

**Lean signature**
```lean
def quadraticGaussianMeasure
    (Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) : Measure (ι → ℝ)
```
**Informal**: The unnormalized quadratic Gaussian measure $d\mu = \rho(\varphi)\,d\varphi$ on $\mathbb{R}^\iota$.

---

### [`normalizedQuadraticGaussianMeasure`](../../GaussianField/Density.lean#L67) -- Definition

**Lean signature**
```lean
def normalizedQuadraticGaussianMeasure
    (Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) : Measure (ι → ℝ)
```
**Informal**: The normalized quadratic Gaussian measure $(1/Z)\,\rho(\varphi)\,d\varphi$.

---

### [`integral_cexp_neg_half_sum_mul_sq_add_linear`](../../GaussianField/Density.lean#L72) -- Theorem

**Statement**: The finite-dimensional diagonal Gaussian Fourier integral evaluates to a product of 1D Gaussian transforms: for $\lambda_i > 0$,
$$\int \exp\Bigl(-\tfrac{1}{2}\sum_i \lambda_i v_i^2 + i\sum_i c_i v_i\Bigr)\,dv = \prod_i \sqrt{2\pi/\lambda_i}\,\exp\bigl(-\tfrac{1}{2}c_i^2/\lambda_i\bigr).$$

**Proof uses**: `GaussianFourier.integral_cexp_neg_sum_mul_add`, `PiLp.volume_preserving_toLp`

---

## Evaluation map

### [`evalMap`](../../GaussianField/Density.lean#L125) -- Definition

**Lean signature**
```lean
def evalMap :
    Configuration (FinLatticeField d N) → FinLatticeField d N
```
**Informal**: The evaluation map $\omega \mapsto (\omega(\delta_x))_{x \in \Lambda}$ extracting the field configuration from a continuous linear functional.

---

### [`measurable_evalMap`](../../GaussianField/Density.lean#L130) -- Theorem

**Statement**: The evaluation map `evalMap d N` is measurable.

**Proof uses**: [`configuration_eval_measurable`](../../GaussianField/Properties.lean)

---

### [`field_basis_decomposition_density`](../../GaussianField/Density.lean#L140) -- Theorem

**Statement**: Every field configuration decomposes as $\varphi = \sum_x \varphi(x)\,\delta_x$.

**Proof uses**: *(direct tactic proof)*

---

### [`config_apply_eq_sum_delta`](../../GaussianField/Density.lean#L147) -- Theorem

**Statement**: The pairing $\omega(f)$ equals $\sum_x f(x)\,\omega(\delta_x)$.

**Proof uses**: [`field_basis_decomposition_density`](../../GaussianField/Density.lean#L140)

---

### [`config_apply_eq_sum_evalMap`](../../GaussianField/Density.lean#L154) -- Theorem

**Statement**: The pairing $\omega(f)$ equals $\sum_x f(x)\,(\mathrm{eval}\,\omega)(x)$.

**Proof uses**: [`config_apply_eq_sum_delta`](../../GaussianField/Density.lean#L147)

---

### [`gaussianDensity_measurable`](../../GaussianField/Density.lean#L159) -- Theorem

**Statement**: The Gaussian density function `gaussianDensity d N a mass` is measurable.

**Proof uses**: *(direct tactic proof)*

---

### [`gaussianDensityWeight`](../../GaussianField/Density.lean#L167) -- Definition

**Lean signature**
```lean
def gaussianDensityWeight (a mass : ℝ) : FinLatticeField d N → ENNReal
```
**Informal**: The Gaussian density lifted to `ENNReal` for use with `withDensity`.

---

### [`gaussianDensityMeasure`](../../GaussianField/Density.lean#L170) -- Definition

**Lean signature**
```lean
def gaussianDensityMeasure (a mass : ℝ) : Measure (FinLatticeField d N)
```
**Informal**: The unnormalized Gaussian density measure $\rho(\varphi)\,d\varphi$ on the lattice field space.

---

### [`gaussianDensityNormConst`](../../GaussianField/Density.lean#L173) -- Definition

**Lean signature**
```lean
noncomputable def gaussianDensityNormConst (a mass : ℝ) : ENNReal
```
**Informal**: The partition function $Z = \int \rho(\varphi)\,d\varphi$.

---

### [`normalizedGaussianDensityMeasure`](../../GaussianField/Density.lean#L176) -- Definition

**Lean signature**
```lean
def normalizedGaussianDensityMeasure (a mass : ℝ) :
    Measure (FinLatticeField d N)
```
**Informal**: The normalized Gaussian density measure $(1/Z)\,\rho(\varphi)\,d\varphi$.

---

### [`latticeGaussianFieldLaw`](../../GaussianField/Density.lean#L181) -- Definition

**Lean signature**
```lean
def latticeGaussianFieldLaw (a mass : ℝ) (ha : 0 < a) (hmass : 0 < mass) :
    Measure (FinLatticeField d N)
```
**Informal**: The finite-dimensional field law: the pushforward of the lattice Gaussian measure by the evaluation map.

---

### [`sitePairing_eq_massEigenbasis_sum`](../../GaussianField/Density.lean#L193) -- Theorem

**Statement**: The site pairing $\sum_x f(x)\,\varphi(x)$ equals the eigenbasis expansion $\sum_k \langle e_k, f\rangle\,\langle e_k, \varphi\rangle$.

**Proof uses**: [`massEigenbasis_sum_mul_sum_eq_site_inner`](../../Lattice/SpectralCovariance.lean)

---

### [`gaussianDensity_eq_exp_massEigenbasis`](../../GaussianField/Density.lean#L205) -- Theorem

**Statement**: The Gaussian density in spectral form: $\rho(\varphi) = \exp\bigl(-\tfrac{1}{2}\sum_k \lambda_k \langle e_k, \varphi\rangle^2\bigr)$.

**Proof uses**: [`gaussianDensity_eq_exp_spectral`](../../Lattice/SpectralCovariance.lean)

---

### [`integral_massEigenbasis_cexp`](../../GaussianField/Density.lean#L216) -- Theorem

**Statement**: The Gaussian Fourier integral in mass-eigenbasis coordinates evaluates to $\prod_k \sqrt{2\pi/\lambda_k}\,\exp(-\tfrac{1}{2}c_k^2/\lambda_k)$.

**Proof uses**: [`integral_cexp_neg_half_sum_mul_sq_add_linear`](../../GaussianField/Density.lean#L72), [`massEigenbasis_quadratic_sum_reprSymm_ofLp`](../../Lattice/SpectralCovariance.lean), [`massEigenbasis_linear_sum_reprSymm_ofLp`](../../Lattice/SpectralCovariance.lean), `OrthonormalBasis.repr.symm.measurePreserving`

---

### [`latticeGaussianFieldLaw_pairing_is_gaussian`](../../GaussianField/Density.lean#L315) -- Theorem

**Statement**: The pushforward of the field law by the site pairing $\sum_x f(x)\,\varphi(x)$ is a 1D Gaussian $N(0, \lVert Tf \rVert^2)$.

**Proof uses**: [`pairing_is_gaussian`](../../GaussianField/Properties.lean), [`config_apply_eq_sum_evalMap`](../../GaussianField/Density.lean#L154)

---

### [`latticeGaussianFieldLaw_fourier`](../../GaussianField/Density.lean#L352) -- Theorem

**Statement**: The characteristic function of the field law equals $\exp(-\tfrac{1}{2}\lVert Tf \rVert^2)$ in site coordinates.

**Proof uses**: [`charFun`](../../GaussianField/Construction.lean), [`config_apply_eq_sum_evalMap`](../../GaussianField/Density.lean#L154)

---

### [`normalizedGaussianDensityMeasure_linearFourier`](../../GaussianField/Density.lean#L412) -- Theorem

**Statement**: The characteristic function of the normalized density measure equals $\exp(-\tfrac{1}{2}\lVert Tf \rVert^2)$, matching the field law.

**Proof uses**: [`integral_massEigenbasis_cexp`](../../GaussianField/Density.lean#L216), [`gaussianDensity_eq_exp_massEigenbasis`](../../GaussianField/Density.lean#L205), [`sitePairing_eq_massEigenbasis_sum`](../../GaussianField/Density.lean#L193), [`spectralLatticeCovariance_norm_sq`](../../Lattice/SpectralCovariance.lean)

---

### [`strongDualToField`](../../GaussianField/Density.lean#L705) -- Definition

**Lean signature**
```lean
def strongDualToField
    (L : StrongDual ℝ (FinLatticeField d N)) : FinLatticeField d N
```
**Informal**: The site-coordinate representative of a dual functional: $f(x) = L(\delta_x)$.

---

### [`normalizedGaussianDensityMeasure_charFunDual_eq_latticeGaussianFieldLaw`](../../GaussianField/Density.lean#L742) -- Theorem

**Statement**: The characteristic functions (as maps on the strong dual) of the normalized density measure and the field law are equal.

**Proof uses**: [`normalizedGaussianDensityMeasure_linearFourier`](../../GaussianField/Density.lean#L412), [`latticeGaussianFieldLaw_fourier`](../../GaussianField/Density.lean#L352)

---

### [`latticeGaussianFieldLaw_eq_normalizedGaussianDensityMeasure`](../../GaussianField/Density.lean#L784) -- Theorem

**Statement**: The lattice Gaussian field law equals the normalized Gaussian density measure. This is the master measure-equality theorem.

**Proof uses**: `Measure.ext_of_charFunDual`, [`normalizedGaussianDensityMeasure_charFunDual_eq_latticeGaussianFieldLaw`](../../GaussianField/Density.lean#L742), [`normalizedGaussianDensityMeasure_isFinite`](../../GaussianField/Density.lean#L768)

---

## Density bridge

### [`latticeGaussianFieldLaw_density_integral`](../../GaussianField/Density.lean#L904) -- Theorem

**Statement**: Expectations under the field law equal normalized weighted Lebesgue integrals:
$$\int F(\varphi)\,d\mu_{\mathrm{law}} = \frac{\int F(\varphi)\,\rho(\varphi)\,d\varphi}{\int \rho(\varphi)\,d\varphi}.$$

**Proof uses**: [`latticeGaussianFieldLaw_eq_normalizedGaussianDensityMeasure`](../../GaussianField/Density.lean#L784), [`gaussianDensityNormConst_eq_ofReal_integral`](../../GaussianField/Density.lean#L882), `integral_withDensity_eq_integral_toReal_smul`

---

### [`latticeGaussianMeasure_density_integral`](../../GaussianField/Density.lean#L1028) -- Theorem

**Statement**: **Density bridge**: expectations under `latticeGaussianMeasure` equal normalized weighted Lebesgue integrals with the Gaussian density.

**Proof uses**: [`latticeGaussianFieldLaw_density_integral`](../../GaussianField/Density.lean#L904)

---

### [`integrable_mul_gaussianDensity`](../../GaussianField/Density.lean#L974) -- Theorem

**Statement**: **Integrability transfer**: if $F$ is integrable under the lattice Gaussian measure, then $F \cdot \rho$ is Lebesgue-integrable.

**Proof uses**: [`integrable_mul_gaussianDensity_of_fieldLaw`](../../GaussianField/Density.lean#L947), `integrable_map_measure`

---

*This file has **14** definitions and **22** theorems/lemmas (0 with sorry).*