# `OS0_Analyticity.lean` — Informal Summary

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

## Overview

Proves OS-0 (Analyticity) for the Gaussian Free Field: the generating functional
$Z[\sum_i z_i J_i] = \int \exp(i \langle \omega, \sum_i z_i J_i \rangle)\, d\mu(\omega)$
is analytic in the complex parameters $z_1, \ldots, z_n$. The strategy derives the
closed-form $Z[f] = \exp(-\tfrac{1}{2} C_\mathbb{C}(f,f))$ via one-parameter analytic
continuation (the identity theorem), then expands
$C_\mathbb{C}(\sum_i z_i J_i, \sum_j z_j J_j)$ as a finite quadratic polynomial in $z$
and composes with $\exp$ to obtain analyticity. The key technical input is Fernique's
theorem (exponential-square integrability of Gaussian pairings) combined with
parameter-dependent holomorphy of integrals.

## Status

**Main result**: Fully proven
**Sorry count**: 0
**Length**: 849 lines, 0 definition(s) + 21 theorem(s)/lemma(s) (4 private)

---

## OS0 for the Gaussian Free Field

### [`distributionPairingℂ_real_continuous`](../../OSforGFF/OS/OS0_Analyticity.lean#L83) — Theorem

**Statement**: For any complex test function $f$, the map $\omega \mapsto \langle \omega, f \rangle_\mathbb{C}$ is continuous on field configurations.

**Proof uses**: `WeakDual.eval_continuous`,
[`distributionPairingℂ_real`](../../OSforGFF/Spacetime/Basic.lean#L250),
[`complex_testfunction_decompose`](../../OSforGFF/Spacetime/Basic.lean#L207)

---

### [`distributionPairingℂ_real_measurable`](../../OSforGFF/OS/OS0_Analyticity.lean#L99) — Lemma

**Statement**: For any complex test function $f$, the map $\omega \mapsto \langle \omega, f \rangle_\mathbb{C}$ is measurable on field configurations.

**Proof uses**: `WeakDual.eval_measurable`,
[`distributionPairingℂ_real`](../../OSforGFF/Spacetime/Basic.lean#L250),
[`complex_testfunction_decompose`](../../OSforGFF/Spacetime/Basic.lean#L207)

---

### [`gff_integrand_measurable`](../../OSforGFF/OS/OS0_Analyticity.lean#L106) — Theorem

**Statement**: For each $z \in \mathbb{C}^n$, the GFF integrand $\omega \mapsto \exp(i \langle \omega, \sum_i z_i J_i \rangle)$ is almost-everywhere strongly measurable with respect to $\mu_{\mathrm{GFF}}$.

**Proof uses**: [`distributionPairingℂ_real_measurable`](../../OSforGFF/OS/OS0_Analyticity.lean#L99)

---

### [`gff_integrand_analytic`](../../OSforGFF/OS/OS0_Analyticity.lean#L120) — Theorem

**Statement**: For each fixed field configuration $\omega$, the map $z \mapsto \exp(i \langle \omega, \sum_i z_i J_i \rangle)$ is analytic at every point $z_0 \in \mathbb{C}^n$.

**Proof uses**: `AnalyticAt.cexp`, `ContinuousLinearMap.analyticAt`,
[`pairing_linear_combo`](../../OSforGFF/Spacetime/ComplexTestFunction.lean#L132),
`Finset.analyticAt_fun_sum`

---

### [`norm_exp_I_distributionPairingℂ_real`](../../OSforGFF/OS/OS0_Analyticity.lean#L194) — Lemma

**Statement**: For any complex test function $f$ with imaginary part $f_{\mathrm{im}}$,
$$\lVert \exp(i \langle \omega, f \rangle_\mathbb{C}) \rVert = \exp(-\omega(f_{\mathrm{im}})).$$

**Proof uses**: `Complex.norm_exp`,
[`distributionPairingℂ_real`](../../OSforGFF/Spacetime/Basic.lean#L250),
[`complex_testfunction_decompose`](../../OSforGFF/Spacetime/Basic.lean#L207)

---

### [`gff_exp_neg_pairing_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L212) — Lemma

**Statement**: For any real test function $f$, the function $\omega \mapsto \exp(-\omega(f))$ is integrable under $\mu_{\mathrm{GFF}}$.

**Proof uses**: [`gaussianFreeField_pairing_expSq_integrable`](../../OSforGFF/Measure/Construct.lean#L398),
[`distributionPairingCLM`](../../OSforGFF/Spacetime/Basic.lean#L123)

---

### [`gff_exp_abs_pairing_memLp`](../../OSforGFF/OS/OS0_Analyticity.lean#L253) — Lemma

**Statement**: For any real test function $f$ and any $p \neq \infty$, the function $\omega \mapsto \exp(\lvert \omega(f) \rvert)$ belongs to $L^p(\mu_{\mathrm{GFF}})$.

**Proof uses**: [`gaussianFreeField_pairing_expSq_integrable`](../../OSforGFF/Measure/Construct.lean#L398),
`eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top`, `ENNReal.ofReal_rpow_of_nonneg`

---

### [`gff_exp_abs_pairing_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L386) — Lemma

**Statement**: For any real test function $f$, the function $\omega \mapsto \exp(\lvert \omega(f) \rvert)$ is integrable under $\mu_{\mathrm{GFF}}$. ($L^1$ special case of `gff_exp_abs_pairing_memLp`.)

**Proof uses**: [`gff_exp_abs_pairing_memLp`](../../OSforGFF/OS/OS0_Analyticity.lean#L253),
`memLp_one_iff_integrable`

---

### [`gff_exp_abs_sum_memLp`](../../OSforGFF/OS/OS0_Analyticity.lean#L394) — Lemma

**Statement**: For a finite family of real test functions $g_1, \ldots, g_k$, the product $\omega \mapsto \exp(\sum_i \lvert \omega(g_i) \rvert)$ belongs to $L^2(\mu_{\mathrm{GFF}})$. Uses generalized Holder: each factor is in $L^{2k}$, and a product of $k$ such factors is in $L^2$.

**Proof uses**: [`gff_exp_abs_pairing_memLp`](../../OSforGFF/OS/OS0_Analyticity.lean#L253),
`MemLp.prod'`

---

### [`gff_integrand_norm_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L447) — Lemma

**Statement**: For any complex test function $f$, the norm $\omega \mapsto \lVert \exp(i \langle \omega, f \rangle_\mathbb{C}) \rVert$ is integrable under $\mu_{\mathrm{GFF}}$.

**Proof uses**: [`norm_exp_I_distributionPairingℂ_real`](../../OSforGFF/OS/OS0_Analyticity.lean#L194),
[`gff_exp_neg_pairing_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L212)

---

### [`gff_integrand_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L461) — Theorem

**Statement**: For each $z \in \mathbb{C}^n$, the GFF integrand $\omega \mapsto \exp(i \langle \omega, \sum_i z_i J_i \rangle)$ is integrable under $\mu_{\mathrm{GFF}}$.

**Proof uses**: [`gff_integrand_norm_integrable`](../../OSforGFF/OS/OS0_Analyticity.lean#L447),
[`gff_integrand_measurable`](../../OSforGFF/OS/OS0_Analyticity.lean#L106),
`integrable_norm_iff`

---

## Complex Characteristic Functional

### [`gff_cf_slice_entire`](../../OSforGFF/OS/OS0_Analyticity.lean#L492) — Lemma

**Statement**: For fixed real test functions $f_{\mathrm{re}}, f_{\mathrm{im}}$, the one-parameter family $t \mapsto Z[\mathrm{toComplex}\, f_{\mathrm{re}} + t \cdot \mathrm{toComplex}\, f_{\mathrm{im}}]$ is entire (analytic on all of $\mathbb{C}$). Proved via Fernique integrability and parameter-dependent holomorphy (`hasFDerivAt_integral_of_dominated_of_fderiv_le`).

**Proof uses**: [`gaussianFreeField_pairing_expSq_integrable`](../../OSforGFF/Measure/Construct.lean#L398),
[`pairing_linear_combo`](../../OSforGFF/Spacetime/ComplexTestFunction.lean#L132),
[`distributionPairingℂ_real_toComplex`](../../OSforGFF/Spacetime/ComplexTestFunction.lean#L284),
[`GJGeneratingFunctionalℂ`](../../OSforGFF/Spacetime/Basic.lean#L257),
`hasFDerivAt_integral_of_dominated_of_fderiv_le`

---

### [`gff_complex_CF_covariance`](../../OSforGFF/OS/OS0_Analyticity.lean#L660) — Theorem

**Statement**: The complex characteristic functional of the GFF equals
$$Z[f] = \mathbb{E}[\exp(i\langle\omega,f\rangle_\mathbb{C})] = \exp\!\bigl(-\tfrac{1}{2}\, C_\mathbb{C}(f,f)\bigr)$$
for any complex test function $f$. Proved by one-parameter analytic continuation: decompose $f = f_{\mathrm{re}} + i\, f_{\mathrm{im}}$, show the generating functional and the Gaussian formula agree on $\mathbb{R}$ (from `gff_real_characteristic`), and extend to $\mathbb{C}$ via the identity theorem.

**Proof uses**: [`gff_cf_slice_entire`](../../OSforGFF/OS/OS0_Analyticity.lean#L492),
[`gff_real_characteristic`](../../OSforGFF/Measure/Construct.lean#L149),
[`GJGeneratingFunctionalℂ_toComplex`](../../OSforGFF/Spacetime/ComplexTestFunction.lean#L291),
[`complex_testfunction_decompose_recompose`](../../OSforGFF/Spacetime/Basic.lean#L235),
[`freeCovarianceFormR_add_left`](../../OSforGFF/Covariance/RealForm.lean#L488),
[`freeCovarianceFormR_symm`](../../OSforGFF/Covariance/RealForm.lean#L476),
[`freeCovarianceℂ_bilinear_add_left`](../../OSforGFF/Covariance/Position.lean#L495),
[`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50),
`AnalyticOnNhd.eq_of_frequently_eq`

---

## Bilinear Expansion for Finite Sums

### [`freeCovarianceℂ_bilinear_sum_expansion`](../../OSforGFF/OS/OS0_Analyticity.lean#L791) — Theorem

**Statement**: The complexified covariance expands over finite sums as
$$C_\mathbb{C}\!\Bigl(\sum_i z_i J_i,\; \sum_j z_j J_j\Bigr) = \sum_i \sum_j z_i\, z_j\, C_\mathbb{C}(J_i, J_j).$$

**Proof uses**: [`freeCovarianceℂ_bilinear_add_left`](../../OSforGFF/Covariance/Position.lean#L495),
[`freeCovarianceℂ_bilinear_smul_left`](../../OSforGFF/Covariance/Position.lean#L505),
[`freeCovarianceℂ_bilinear_add_right`](../../OSforGFF/Covariance/Position.lean#L567),
[`freeCovarianceℂ_bilinear_smul_right`](../../OSforGFF/Covariance/Position.lean#L556)

---

### [`gff_generating_eq_exp_quadratic`](../../OSforGFF/OS/OS0_Analyticity.lean#L802) — Theorem

**Statement**: The generating functional for a finite linear combination equals
$$Z\!\Bigl[\sum_i z_i J_i\Bigr] = \exp\!\Bigl(-\tfrac{1}{2}\sum_{i,j} z_i\, z_j\, C_\mathbb{C}(J_i, J_j)\Bigr).$$

**Proof uses**: [`gff_complex_CF_covariance`](../../OSforGFF/OS/OS0_Analyticity.lean#L660),
[`freeCovarianceℂ_bilinear_sum_expansion`](../../OSforGFF/OS/OS0_Analyticity.lean#L791)

---

## Analyticity of exp(finite quadratic form)

### [`analyticOn_finite_quadratic`](../../OSforGFF/OS/OS0_Analyticity.lean#L815) — Theorem

**Statement**: A finite quadratic form $z \mapsto \sum_{i,j} A_{ij}\, z_i\, z_j$ is analytic on all of $\mathbb{C}^n$ (it is a polynomial).

**Proof uses**: `ContinuousLinearMap.proj`, `Finset.analyticOn_sum`, `AnalyticOn.mul`

---

### [`gaussianFreeField_satisfies_OS0`](../../OSforGFF/OS/OS0_Analyticity.lean#L832) — Theorem

**Statement**: The Gaussian Free Field measure $\mu_{\mathrm{GFF}}$ satisfies the OS-0 Analyticity axiom: $z \mapsto Z[\sum_i z_i J_i]$ is analytic on $\mathbb{C}^n$ for every $n$ and every $n$-tuple of complex test functions $J_i$.

**Proof uses**: [`gff_generating_eq_exp_quadratic`](../../OSforGFF/OS/OS0_Analyticity.lean#L802),
[`analyticOn_finite_quadratic`](../../OSforGFF/OS/OS0_Analyticity.lean#L815),
[`freeCovarianceℂ_bilinear`](../../OSforGFF/Covariance/Parseval.lean#L923),
[`OS0_Analyticity`](../../OSforGFF/OS/Axioms.lean#L73)

---

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