# `GaussianFreeField.lean` — Informal Summary

> **Source**: [`OSforGFF/Measure/GaussianFreeField.lean`](../../OSforGFF/Measure/GaussianFreeField.lean)
> **Generated**: 2026-03-03 00:00
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

This file assembles the Gaussian Free Field and proves two Osterwalder-Schrader (OS) axioms
for general Gaussian measures. OS0 (analyticity) is proved via an alternative route: the
generating functional $Z[\sum_i z_i J_i] = \exp(-\tfrac{1}{2}\sum_{ij} z_i z_j S_2(J_i, J_j))$
is entire because it is the exponential of a polynomial in the $z_i$. OS2 (Euclidean invariance)
follows immediately from invariance of the covariance under Euclidean transformations. Both
proofs work for any Gaussian measure satisfying the appropriate covariance assumptions, not
just the free GFF. The primary OS0 proof used by the Master theorem is in `OS.OS0_Analyticity`;
the proof here is an independent alternative.

## Status

**Main result**: Fully proven (0 sorries).

None — file is sorry-free.

**Length**: 274 lines, 4 definition(s) + 3 theorem(s)/lemma(s)

---

## OS0_alt Namespace

### [`bilin_sum_sum`](../../OSforGFF/Measure/GaussianFreeField.lean#L58) — Lemma

**Statement**: For a complex bilinear form $B$ on $E$, finite index set of vectors
$(J_i)_{i < n}$, and scalars $(z_i)_{i < n}$,
$$B\!\Bigl(\sum_i z_i J_i,\, \sum_j z_j J_j\Bigr) = \sum_i \sum_j z_i z_j\, B(J_i, J_j).$$

**Proof uses**: `Finset.sum_comm`, `Finset.mul_sum`

---

### [`CovarianceContinuous`](../../OSforGFF/Measure/GaussianFreeField.lean#L75) — Definition

**Lean signature**
```lean
def CovarianceContinuous (dμ_config : ProbabilityMeasure FieldConfiguration) : Prop
```

**Informal**: The condition that the complex covariance $J \mapsto S_2(\mu, z \cdot J, K)$ is continuous in $z \in \mathbb{C}$ for all fixed test functions $J$ and $K$.

---

## OS0: Analyticity for Gaussian Measures (OLD PROOF - in OS0_alt namespace)

### [`GJcov_bilin`](../../OSforGFF/Measure/GaussianFreeField.lean#L90) — Definition

**Lean signature**
```lean
def GJcov_bilin (dμ_config : ProbabilityMeasure FieldConfiguration)
  (h_bilinear : CovarianceBilinear dμ_config) : LinearMap.BilinMap ℂ TestFunctionℂ ℂ
```

**Informal**: Packages the Schwinger two-point function $S_2(\mu, \cdot, \cdot)$ as a
`LinearMap.BilinMap`, using the `CovarianceBilinear` hypothesis to verify the linearity
axioms in both arguments.

---

### [`gaussian_satisfies_OS0`](../../OSforGFF/Measure/GaussianFreeField.lean#L107) — Theorem

**Statement**: Any Gaussian measure $\mu$ (satisfying `isGaussianGJ`) with bilinear
covariance satisfies OS0 analyticity: for every $n$ and test functions $(J_i)_{i < n}$,
the map $z \mapsto Z_\mathbb{C}[\sum_i z_i J_i]$ is analytic on all of $\mathbb{C}^n$.

**Proof uses**: [`GJcov_bilin`](../../OSforGFF/Measure/GaussianFreeField.lean#L90),
[`bilin_sum_sum`](../../OSforGFF/Measure/GaussianFreeField.lean#L58),
`AnalyticOn.cexp`, `Finset.analyticOnNhd_sum`, `ContinuousLinearMap.proj`

---

## OS2: Euclidean Invariance for Translation-Invariant Gaussian Measures

### [`CovarianceEuclideanInvariant`](../../OSforGFF/Measure/GaussianFreeField.lean#L201) — Definition

**Lean signature**
```lean
def CovarianceEuclideanInvariant (dμ_config : ProbabilityMeasure FieldConfiguration) : Prop
```

**Informal**: The real two-point Schwinger function $S_2(\mu, \cdot, \cdot)$ is invariant under
the Euclidean group action: $S_2(\mu, g \cdot f, g \cdot h) = S_2(\mu, f, h)$ for all
$g \in E(4)$ and real test functions $f, h$.

---

### [`CovarianceEuclideanInvariantℂ`](../../OSforGFF/Measure/GaussianFreeField.lean#L207) — Definition

**Lean signature**
```lean
def CovarianceEuclideanInvariantℂ (dμ_config : ProbabilityMeasure FieldConfiguration) : Prop
```

**Informal**: The complex two-point Schwinger function $S_2^\mathbb{C}(\mu, \cdot, \cdot)$ is
invariant under the Euclidean group action on complex test functions: $S_2^\mathbb{C}(\mu, g \cdot f, g \cdot h) = S_2^\mathbb{C}(\mu, f, h)$ for all $g \in E(4)$ and complex test functions $f, h$.

---

### [`gaussian_satisfies_OS2`](../../OSforGFF/Measure/GaussianFreeField.lean#L212) — Theorem

**Statement**: Any Gaussian measure $\mu$ (satisfying `isGaussianGJ`) whose complex covariance
is Euclidean-invariant satisfies OS2 (Euclidean invariance of the generating functional):
$Z_\mathbb{C}[g \cdot f] = Z_\mathbb{C}[f]$ for all $g \in E(4)$ and complex test functions $f$.

**Proof uses**: [`CovarianceEuclideanInvariantℂ`](../../OSforGFF/Measure/GaussianFreeField.lean#L207),
[`isGaussianGJ`](../../OSforGFF/Measure/Construct.lean#L90)

---

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