# `OS1_Regularity.lean` — Informal Summary

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

## Overview

Proves OS-1 (Regularity) for the Gaussian Free Field: the generating functional satisfies
the exponential bound $\lVert Z[f] \rVert \leq \exp\!\bigl(\tfrac{1}{2m^2}\int\lVert f\rVert^2\bigr)$
with $p = 2$ and $c = 1/(2m^2)$. The argument proceeds via: (1) $\lVert Z[f] \rVert =
\exp(-\tfrac{1}{2}\mathrm{Re}\langle f, Cf\rangle_\mathbb{C})$, (2) positive semidefiniteness
of $C$ bounds this by $\exp(\tfrac{1}{2}C(f_{\mathrm{im}}, f_{\mathrm{im}}))$, (3) a
momentum-space Parseval estimate gives $C(g,g) \leq \lVert g \rVert_{L^2}^2 / m^2$.
Local integrability of the two-point function $S_2(x) \sim \lvert x\rvert^{-2}$ follows
from the decay bound established for the free covariance kernel.

## Status

**Main result**: Fully proven

None — file is sorry-free.

**Length**: 582 lines, 1 definition + 12 theorem(s)/lemma(s)

---

## Preliminaries

### [`fourier_plancherel_schwartz`](../../OSforGFF/OS/OS1_Regularity.lean#L58) — Theorem

**Statement**: The Fourier transform preserves the $L^2$ norm on Schwartz functions: for any complex test function $g$,
$$\int_{\mathbb{R}^4} \lVert \hat{g}(k) \rVert^2\, dk = \int_{\mathbb{R}^4} \lVert g(x) \rVert^2\, dx.$$

**Proof uses**: `SchwartzMap.integral_norm_sq_fourier`

---

### [`SchwingerTwoPointFunction_GFF`](../../OSforGFF/OS/OS1_Regularity.lean#L82) — Definition

**Lean signature**
```lean
noncomputable def SchwingerTwoPointFunction_GFF (m : ℝ) [Fact (0 < m)] (x : SpaceTime) : ℝ
```

**Informal**: The two-point Schwinger function of the GFF at $x$, defined concretely as the free covariance kernel $C_m(x)$ evaluated at $x$.

---

### [`schwingerTwoPoint_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L86) — Theorem

**Statement**: The GFF two-point function equals the free covariance kernel by definition:
$S_2^{\mathrm{GFF}}(x) = C_m(x)$.

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

---

### [`schwingerTwoPointFunction_eq_GFF`](../../OSforGFF/OS/OS1_Regularity.lean#L98) — Theorem

**Statement**: The abstract limit-based Schwinger two-point function agrees with the
concrete GFF kernel: $S_2^{\mathrm{abs}}(x) = S_2^{\mathrm{GFF}}(x)$ for $x \neq 0$.

**Proof uses**: [`freeCovarianceKernel_continuousOn`](../../OSforGFF/Covariance/Momentum.lean#L1963),
[`schwinger_eq_covariance`](../../OSforGFF/Schwinger/Defs.lean#L82),
[`GFFIsGaussian.schwinger_eq_covariance_real`](../../OSforGFF/Measure/IsGaussian.lean#L372),
[`schwingerTwoPointFunction_eq_kernel`](../../OSforGFF/Schwinger/TwoPoint.lean#L167)

---

### [`schwingerTwoPointFunction_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L135) — Theorem

**Statement**: The abstract Schwinger two-point function equals the free covariance kernel
$S_2(x) = C_m(x)$ for $x \neq 0$.

**Proof uses**: [`schwingerTwoPointFunction_eq_GFF`](../../OSforGFF/OS/OS1_Regularity.lean#L98),
[`schwingerTwoPoint_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L86)

---

### [`schwinger_two_point_decay_bound_GFF`](../../OSforGFF/OS/OS1_Regularity.lean#L144) — Theorem

**Statement**: There exists $C > 0$ such that for all $x, y \in \mathbb{R}^4$,
$\lvert S_2^{\mathrm{GFF}}(x - y) \rvert \leq C \lVert x - y \rVert^{-2}$.

**Proof uses**: [`freeCovarianceKernel_decay_bound`](../../OSforGFF/Covariance/Momentum.lean#L1723),
[`schwingerTwoPoint_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L86)

---

### [`schwinger_two_point_decay_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L161) — Theorem

**Statement**: The abstract Schwinger two-point function satisfies the same polynomial
decay bound: there exists $C > 0$ such that
$\lVert S_2(x - y) \rVert \leq C \lVert x - y \rVert^{-2}$ for all $x, y$.

**Proof uses**: [`schwinger_two_point_decay_bound_GFF`](../../OSforGFF/OS/OS1_Regularity.lean#L144),
[`schwingerTwoPointFunction_zero`](../../OSforGFF/Schwinger/TwoPoint.lean#L114),
[`schwingerTwoPointFunction_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L135)

---

### [`schwingerTwoPoint_measurable`](../../OSforGFF/OS/OS1_Regularity.lean#L188) — Theorem

**Statement**: The abstract Schwinger two-point function is almost-everywhere strongly
measurable with respect to Lebesgue measure on $\mathbb{R}^4$.

**Proof uses**: [`freeCovarianceKernel_integrable`](../../OSforGFF/Covariance/Momentum.lean#L1690),
[`schwingerTwoPointFunction_eq_freeCovarianceKernel`](../../OSforGFF/OS/OS1_Regularity.lean#L135)

---

## GFF Exponential Bound

### [`gff_generating_norm_eq`](../../OSforGFF/OS/OS1_Regularity.lean#L218) — Lemma

**Statement**: The norm of the GFF generating functional equals
$$\lVert Z[f] \rVert = \exp\!\bigl(-\tfrac{1}{2} \mathrm{Re} C_\mathbb{C}(f,f)\bigr).$$

**Proof uses**: [`gff_complex_generating`](../../OSforGFF/Measure/IsGaussian.lean#L523),
[`gff_two_point_equals_covarianceℂ_free`](../../OSforGFF/Measure/IsGaussian.lean#L463),
`Complex.norm_exp`

---

### [`gff_generating_bound_by_imaginary`](../../OSforGFF/OS/OS1_Regularity.lean#L228) — Lemma

**Statement**: The norm of the generating functional is bounded above by
$$\lVert Z[f] \rVert \leq \exp\!\bigl(\tfrac{1}{2} C_\mathbb{C}(if_{\mathrm{im}}, if_{\mathrm{im}})\bigr),$$
using the real-part decomposition $\mathrm{Re} C_\mathbb{C}(f,f) = C(f_{\mathrm{re}}, f_{\mathrm{re}}) - C(f_{\mathrm{im}}, f_{\mathrm{im}})$ and positivity of $C$.

**Proof uses**: [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50),
[`freeCovarianceℂ_bilinear_symm`](../../OSforGFF/Covariance/Position.lean#L528),
[`freeCovarianceℂ_positive`](../../OSforGFF/Covariance/Position.lean#L601),
[`complex_testfunction_decompose_recompose`](../../OSforGFF/Spacetime/Basic.lean#L206)

---

### [`covariance_imaginary_L2_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L313) — Lemma

**Statement**: The real covariance of the imaginary part is bounded by $(1/m^2)$ times the
$L^2$ norm squared of $f$:
$$C_\mathbb{C}(f_{\mathrm{im}}, f_{\mathrm{im}}) \leq \frac{1}{m^2} \int \lVert f(x) \rVert^2\, dx.$$

**Proof uses**: [`parseval_covariance_schwartz_bessel`](../../OSforGFF/Covariance/Position.lean#L628),
[`freeCovarianceℂ_eq_bilinear_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L195),
[`fourier_plancherel_schwartz`](../../OSforGFF/OS/OS1_Regularity.lean#L58),
[`real_integral_mono_of_le`](../../OSforGFF/Covariance/Momentum.lean#L95),
[`integral_const_mul_eq`](../../OSforGFF/Covariance/Momentum.lean#L86)

---

### [`gff_generating_L2_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L467) — Lemma

**Statement**: The GFF generating functional satisfies
$$\lVert Z[f] \rVert \leq \exp\!\Bigl(\frac{1}{2m^2} \int \lVert f(x) \rVert^2\, dx\Bigr).$$

**Proof uses**: [`gff_generating_norm_eq`](../../OSforGFF/OS/OS1_Regularity.lean#L218),
[`gff_generating_bound_by_imaginary`](../../OSforGFF/OS/OS1_Regularity.lean#L228),
[`covariance_imaginary_L2_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L313)

---

## Two-Point Function Local Integrability

### [`gff_two_point_locally_integrable`](../../OSforGFF/OS/OS1_Regularity.lean#L488) — Lemma

**Statement**: The two-point Schwinger function of the GFF is locally integrable on $\mathbb{R}^4$,
i.e., $S_2 \in L^1_{\mathrm{loc}}(\mathbb{R}^4)$.

**Proof uses**: [`schwinger_two_point_decay_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L161),
[`locallyIntegrable_of_rpow_decay_real`](../../OSforGFF/General/FunctionalAnalysis.lean#L464),
[`schwingerTwoPoint_measurable`](../../OSforGFF/OS/OS1_Regularity.lean#L188)

---

## OS1 Verification for the GFF

### [`gaussianFreeField_satisfies_OS1_revised`](../../OSforGFF/OS/OS1_Regularity.lean#L527) — Theorem

**Statement**: The Gaussian Free Field measure $\mu_{\mathrm{GFF}}$ satisfies OS-1 Regularity
with $p = 2$ and $c = 1/(2m^2)$: for every complex test function $f$,
$$\lVert Z[f] \rVert \leq \exp\!\Bigl(\frac{1}{2m^2}\Bigl(\int \lVert f\rVert\, dx + \int \lVert f\rVert^2\, dx\Bigr)\Bigr),$$
and $S_2$ is locally integrable.

**Proof uses**: [`gff_generating_L2_bound`](../../OSforGFF/OS/OS1_Regularity.lean#L467),
[`gff_two_point_locally_integrable`](../../OSforGFF/OS/OS1_Regularity.lean#L488)

---

*This file has **1** definition and **12** theorems/lemmas (0 with sorry).*