# `Properties.lean` — Informal Summary

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

## Overview

Derives downstream consequences of the characteristic functional identity from `Construction.lean`. The key intermediate result shows that the pushforward of the Gaussian measure by evaluation at $f$ is the 1D Gaussian $N(0, \lVert T(f) \rVert^2)$. From this, all moment identities and $L^p$ integrability results follow, including centeredness, the second-moment/covariance identity, and the cross-moment polarization formula.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

**Length**: 193 lines, 0 definition(s) + 7 theorem(s)/lemma(s)

---

### [`pairing_is_gaussian`](../../GaussianField/Properties.lean#L50) --- Theorem

**Statement**: The pushforward of the Gaussian measure by the evaluation map $\omega \mapsto \omega(f)$ is the 1D Gaussian $N(0, \langle T(f), T(f) \rangle_H)$. Proved by matching characteristic functions via Levy's uniqueness theorem.

**Proof uses**: [`charFun`](../../GaussianField/Construction.lean#L687), [`configuration_eval_measurable`](../../GaussianField/Construction.lean#L85), `Measure.ext_of_charFun`, `charFun_gaussianReal`

---

### [`pairing_memLp`](../../GaussianField/Properties.lean#L86) --- Theorem

**Statement**: For all finite $p$, the evaluation $\omega \mapsto \omega(f)$ is in $L^p$ (Fernique-type bound).

**Proof uses**: [`pairing_is_gaussian`](../../GaussianField/Properties.lean#L50), `memLp_id_gaussianReal`, `memLp_map_measure_iff`

---

### [`pairing_integrable`](../../GaussianField/Properties.lean#L97) --- Theorem

**Statement**: The evaluation $\omega \mapsto \omega(f)$ is integrable.

**Proof uses**: [`pairing_memLp`](../../GaussianField/Properties.lean#L86), `memLp_one_iff_integrable`

---

### [`measure_centered`](../../GaussianField/Properties.lean#L104) --- Theorem

**Statement**: The measure is centered: $\mathbb{E}[\omega(f)] = 0$ for all test functions $f$.

**Proof uses**: [`pairing_is_gaussian`](../../GaussianField/Properties.lean#L50), `integral_id_gaussianReal`, `integral_map`

---

### [`second_moment_eq_covariance`](../../GaussianField/Properties.lean#L117) --- Theorem

**Statement**: The second moment equals the covariance: $\mathbb{E}[\omega(f)^2] = \langle T(f), T(f) \rangle_H$.

**Proof uses**: [`pairing_is_gaussian`](../../GaussianField/Properties.lean#L50), [`measure_centered`](../../GaussianField/Properties.lean#L104), `variance_of_integral_eq_zero`, `variance_map`, `variance_fun_id_gaussianReal`

---

### [`pairing_product_integrable`](../../GaussianField/Properties.lean#L139) --- Theorem

**Statement**: Products of pairings $\omega(f) \cdot \omega(g)$ are integrable (by Cauchy--Schwarz in $L^2$).

**Proof uses**: [`pairing_memLp`](../../GaussianField/Properties.lean#L86), `MemLp.integrable_mul`

---

### [`cross_moment_eq_covariance`](../../GaussianField/Properties.lean#L153) --- Theorem

**Statement**: The cross moment equals the inner product: $\mathbb{E}[\omega(f) \cdot \omega(g)] = \langle T(f), T(g) \rangle_H$. Proved by polarization from the second-moment identity: $\langle Tf, Tg \rangle = \tfrac{1}{4}(\lVert T(f+g) \rVert^2 - \lVert T(f-g) \rVert^2)$.

**Proof uses**: [`second_moment_eq_covariance`](../../GaussianField/Properties.lean#L117), [`pairing_product_integrable`](../../GaussianField/Properties.lean#L139), [`pairing_memLp`](../../GaussianField/Properties.lean#L86)

---

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